This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Using CSP to Detect Errors in the TMN Protocol
October 1997 (vol. 23 no. 10)
pp. 659-669

Abstract—In this paper we use FDR, a model checker for CSP, to detect errors in the TMN protocol [18]. We model the protocol and a very general intruder as CSP processes, and use the model checker to test whether the intruder can successfully attack the protocol. We consider three variants on the protocol, and discover a total of 10 different attacks leading to breaches of security.

[1] D. Coppersmith, M. Frankin, J. Patarin, and M.K. Reiter, "Low-Exponent RSA with Related Messages," U. Maurer, ed., Proc. Eurocrypt '96, Lecture Notes in Computer Science 1070. Springer-Verlag, 1996.
[2] S.T. Eckmann and R.A. Kemmerer, "Inatest: An Interactive Environment for Testing Formal Specifications, ACM—Software Eng. Notes, vol. 10, no. 4, 1985.
[3] "Formal Systems (Europe) Ltd." Failures-Divergence Refinement—FDR 2 User Manual, 1997. Available via URLwww.arl.wustl.edu/arl/refpapers/gopal/os.htmlhttp:/ /www.formal.demon.co.ukFDR2.html .
[4] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[5] R.A. Kemmerer, C. Meadows, and J. Millen, "Three Systems for Cryptographic Protocol Analysis," J. Cryptology, vol. 7, no. 2, 1994.
[6] 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.
[7] G. Lowe, "Casper: A Compiler for the Analysis of Security Protocols," Proc. 10th IEEE Computer Security Foundations Workshop, pp. 18-30, 1997. URL.
[8] G. Lowe, "A Hierarchy of Authentication Specifications," Proc. 10th IEEE Computer Security Foundations Workshop, 1997.
[9] J.K. Millen, S.C. Clark, and S.B. Freedman, "The Interrogator: Protocol Security Analysis," IEEE Trans. Software Eng., vol. 13, no. 2, 1987.
[10] C. Meadows, "The NRL Protocol Analyzer: An Overview. J. Logic Programming, vol. 26, no. 2, pp. 113-131, 1996.
[11] J.C. Mitchell, M. Mitchell, and U. Stern, "Automated Analysis of Cryptographic Protocols Using Murφ," IEEE Symp. Security and Privacy, 1997.
[12] A.W. Roscoe and M.H. Goldsmith, "The Perfect "Spy" for Model-Checking Cryptoprotocols," Proc. DIMACS Workshop Design and Formal Verification of Security Protocols, 1997. URL:http://www.mcs.le.ac.uk/~glowe/Security/ Casper/index.htmlhttp://dimacs.rutgers.edu/ Workshops/Security/program2program.html .
[13] A.W. Roscoe, "Model-Checking CSP," A Classical Mind, Essays in Honour of C.A.R. Hoare. Prentice Hall, 1994.
[14] A.W. Roscoe, "Intensional Specification of Security Protocols," Ninth IEEE Computer Security Foundations Workshop, pp. 28-38, 1996.
[15] A.W. Roscoe, Theory and Practice of Concurrency. Prentice-Hall, 1997.
[16] R.L. Rivest,A. Shamir, and L.A. Adleman,"A Method for Obtaining Digital Signatures and Public Key Cryptosystems," Comm. ACM, vol. 21, pp. 120-126, 1978.
[17] G.J. Simmons, "Cryptanalysis and Protocol Failures," Comm. ACM, vol. 37, no. 11, pp. 56-65, 1994.
[18] M. Tatebayashi, N. Matsuzaki, and D.B. Newman Jr., "Key Distribution Protocol for Digital Mobile Communication Systems," Advances in Cryptology: Proc. Crypto '89, Lecture Notes in Computer Science 435, pp. 324-333. Springer-Verlag, 1990.

Index Terms:
Security protocols, key establishment, CSP, FDR, model checking, cryptography, protocol failure.
Citation:
Gavin Lowe, Bill Roscoe, "Using CSP to Detect Errors in the TMN Protocol," IEEE Transactions on Software Engineering, vol. 23, no. 10, pp. 659-669, Oct. 1997, doi:10.1109/32.637148
Usage of this product signifies your acceptance of the Terms of Use.