This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verifying Authentication Protocols in CSP
September 1998 (vol. 24 no. 9)
pp. 741-758

Abstract—This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder Public-Key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs.

[1] M. Abadi and A.D. Gordon, "A Calculus for Cryptographic Protocols: The spi Calculus," technical report, Univ. of Cambridge, 1996.
[2] M. Burrows, M. Abadi, and R. Needham, "A Logic of Authentication," Technical Report 39, SRC, Dec. 1989.
[3] J. Davies and S. Schneider, "Recursion Induction for Real-Time Processes," Formal Aspects of Computing, vol. 5, no. 6, 1993.
[4] W. Diffie, P.C. van Oorschot, and M.J. Weiner, “Authentication and Authenticated Key Exchanges,” Design, Codes and Cryptography, vol. 2, pp. 107-125, 1992.
[5] D. Dolev and A. C. Yao, "On the security of public key protocols," IEEE Trans. Information Theory, vol. 29, no. 2, Mar. 1983. Also appears in the 22nd FOCS, 1981.
[6] D. Gollmann, "What Do We Mean by Entity Authentication," IEEE Computer Society Symp. Research in Security and Privacy, 1996.
[7] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[8] International Organisation for Standardisation, Information Processing Systems—Open Systems Interconnection—Basic Reference Model—Part 2: Security Architecture, ISO 7498-2. 1989.
[9] R. Kemmerer, C. Meadows, and J. Millen, "Three Systems for Cryptographic Protocol Analysis," J. Cryptology, vol. 7, no. 2, 1994.
[10] G. Lowe, An Attack on the Needham-Schroeder Public-Key Protocol Information Processing Letters, 1995.
[11] G. Lowe, "Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proc. TACAS, Lecture Notes in Computer Science 1055, pp. 147-166. Springer-Verlag, 1996. Also in Software—Concepts and Tools, vol. 17, pp. 93-102, 1996.
[12] G. Lowe, "A Hierarchy of Authentication Specifications," Proc. 10th IEEE Computer Security Foundations Workshop, 1997.
[13] C. Meadows, "Applying Formal Methods to the Analysis of a Key Management Protocol," J. Computer Security, vol. 1, no. 1, 1992.
[14] J. Millen, "The Interrogator Model," IEEE Computer Society Symp. Research in Security and Privacy, 1995.
[15] R. Milner, J. Parrow, and D. Walker, “A Calculus of Mobile Processes,” Information and Computation, vol. 100, pp. 1-77, 1992.
[16] R.M. Needham and M.D. Schroeder, "Using Encryption for Authentication in Large Networks of Computers," Comm. ACM, vol. 21, no. 12, pp. 993-999, Dec. 1978
[17] S. Owre, N. Shankar, and J. Rushby, "The PVS Specification Language," technical report, Computer Science Laboratory, SRI Int'l, 1993.
[18] L.C. Paulson, "Proving Properties of Security Protocols by Induction," technical report, Univ. of Cambridge, UK, 1996.
[19] A.W. Roscoe, "Modelling and Verifying Key-Excfhange Protocols Using CSP and FDR," Proc. Computer Security Foundations Workshop, no. 8, 1995.
[20] A.W. Roscoe, "Intensional Specification of Security Protocols," Ninth IEEE Computer Security Foundations Workshop, pp. 28-38, 1996.
[21] A.W. Roscoe, Theory and Practice of Concurrency. Prentice-Hall, 1997.
[22] S. Schneider, “Security Properties and CSP,” Proc. IEEE Symp. Security and Privacy, 1996.
[23] P. Syverson and C. Meadows, "A Formal Language for Cryptographic Protocol Requirements," Designs, Code,s and Cryptography, no. 7, 1996.
[24] T. Woo and S. Lam, "A Semantic Model for Authentication Protocols," Proc. IEEE Computer Society Symp. Research in Security and Privacy, 1993.

Index Terms:
Authentication, security protocols, formal methods, CSP, verification, Needham-Schroeder protocol.
Citation:
Steve Schneider, "Verifying Authentication Protocols in CSP," IEEE Transactions on Software Engineering, vol. 24, no. 9, pp. 741-758, Sept. 1998, doi:10.1109/32.713329
Usage of this product signifies your acceptance of the Terms of Use.