Process algebraic modeling of authentication protocols for analysis of parallel multi-session executions

Document Type: ORIGINAL RESEARCH PAPER

Author

Abstract

Many security protocols have the aim of authenticating one agent acting as initiator to another agent acting as responder and vice versa. Sometimes, the authentication fails because of executing several parallel sessions of a protocol, and because an agent may play both the initiator and responder role in parallel sessions. We take advantage of the notion of transition systems to specify authentication for parallel multiple session's execution. To model the authentication, two main notions called 1. agent's scope and 2. agent's recognizability are introduced, which consider the difference of ability of agents due to their different roles in the protocol and different access to keys and secrets. To formalize above notions, a process algebra provided by some primitives for manipulating cryptographic messages is used. We formalize some security protocols and examine our definition of authentication for them. We just discuss the symmetric key case.

Keywords


[1] Michael Burrows, Martín Abadi, and Roger Needham. A Logic of Authentication. Proceedings of the Royal Society of London. Series A, Mathematical and Physical Sciences (1934-1990), 426(1871):233-271, 1989.

[2] Martín Abadi and Mark R. Tuttle. A Semantics for a Logic of Authentication (Extended Abstract). In Proceedings of the ACM Symposium of Principles of Distributed Computing, pages 201-216. ACM Press, 1991.

[3] Paul van Oorschot. Extending Cryptographic Logics of Belief to Key Agreement Protocols. In Proceedings of the 1st ACM conference on Computer and Communications Security (CCS '93), pages 232-243, New York, NY, USA, 1993. ACM.

[4] Paul F. Syverson and Paul C. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In Proceedings of IEEE Computer Society Symposium on Research in Security and Privacy (CSFW94), pages 14-28, 1994.

[5] Li Gong, Roger Needham, and Raphael Yahalom. Reasoning about Belief in Cryptographic Protocols. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 234-248. IEEE Computer Society, 1990.

[6] Yan Zhang and Vijay Varadharajan. A Logic for Modeling the Dynamics of Beliefs in Cryptographic Protocols. In Proceedings of the 24th Australaian Conference on Computer Science, pages 215-222. IEEE Computer Society Washington, DC, USA, 2001.

[7] Gavin Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1055, pages 147-166. Springer, 1996.

[8] A. William Roscoe. Modeling and Verifying Key- Exchange Protocols using CSP and FDR. In Proceedings of the 8th IEEE Computer Security Foundations Workshop, pages 98-107, 1995.

[9] Peter Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe, and Bill Roscoe. The Modeling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2001.

[10] F. Javier Thayer F_abrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand Spaces: Why is a Security Protocol Correct? In Proceedings of the IEEE Symposium on Security and Privacy, pages 160-171, 1998.

[11] F. Javier Thayer F_abrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security, 7(2-3):191-230, 1999.

[12] Wan Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2000.

[13] Wan Fokkink. Modeling Distributed Systems. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2007.

[14] Gavin Lowe. A Hierarchy of Authentication Speci_cations. In Proceedings of 10th IEEE Computer Security Foundations Workshop, volume 15. IEEE, 1997.

[15] Gavin Lowe. A Family of Attacks upon Authentication Protocols. Technical Report 1997/5, Department of Mathematics and Computer Science, University of Leicester, England, 1997.

[16] Rasool Ramezanian. Authentication in Parallel Multiple- Sessions Execution of Protocols. In Proceedings of the 4th Iranian Society of Cryptology Conference, 2007.

[17] C.A. Middelburg and Michel A. Reniers. Introduction to Process Theory, 2004. Technische Universiteit Eindhoven.

[18] Stefan Blom, Jan Friso Groote, Sjouke Mauw, and Alexander Serebrenik. Analysing the BKE-security Protocol with ϻCRL. Electronic Notes in Theoretical Computer Science, 139(1):49-90, 2005.

[19] Cas J. F. Cremers, Sjouke Mauw, and Erik P. de Vink. A Syntactic Criterion for Injectivity of Authentication Protocols. Electronic Notes in Theoretical Computer Science, 135(1):23-38, 2005. Proceedings of the Second Workshop on Automated Reasoning for Security Protocol analysis (ARSPA 2005).

[20] Cas J. F. Cremers, Sjouke Mauw, and Erik P. de Vink. Injective Synchronisation: An Extension of the Authentication Hierarchy. Theoretical Computer Science, 367(1-2):139-161, 2006. Automated Reasoning for Security Protocol Analysis, Automated Reasoning for Security Protocol Analysis.

[21] Mohammad Torabi Dashti. Keeping Fairness Alive: Design and Formal Verification of Fair Exchange Protocols. PhD thesis, Vrije Universitei, Amsterdam, 2008.

[22] Riccardo Focardi and Roberto Gorrieri. A Classi_cation of Security Properties for Process Algebras. Journal of Computer Security, 3:5-33, 1994.

[23] Jun Pang. Analysis of a Security Protocol in ϻCRL. In Proceedings of the 4th International Conference on Formal Engineering Methods (ICFEM): Formal Methods and Software Engineering, pages 396-400. Springer, 2002.

[24] Thomas Y.C. Woo and Simon S. Lam. A Semantic Model for Authentication Protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 178-194, 1993.

[25] Andrew D. Gordon and Alan Jeffrey. Authenticity by Typing for Security Protocols. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01), pages 145-159, Los Alamitos, CA, USA, 2001. IEEE Computer Society.

[26] Andrew D. Gordon and Alan Jeffrey. Typing Correspondence Assertions for Communication Protocols. Theoretical Computer Science, 300(1-3):379-409, 2003.

[27] Eduardo Bonelli, Adriana Compagnoni, and Elsa Gunter. Correspondence Assertions for Process Synchronization in Concurrent Communications. Journal of Functional Programming, 15(02):219-247, 2005.

[28] Annette M. Bleeker and Jan van Eijck. The Epistemics of Encryption. Technical report, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 2000.

[29] Francien Dechesne and Yanjing Wang. Dynamic Epistemic Verification of Security Protocols: Framework and Case Study. In Proceedings of the Workshop on Logic, Rationality and Interaction, pages 129-144, 2007.

[30] Jan van Eijck and Simona Orzan. Epistemic Veri_cation of Anonymity. Electronic Notes in Theoretical Computer Science, 168:159-174, 2007. Proceedings of the Second International Workshop on Views on Designing Complex Architectures (VODCA 2006).

[31] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic, volume 337 of Synthese Library. Springer, 2007.

[32] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge MA, August 1995.