This Article 
 Bibliographic References 
 Add to: 
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 / .
[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: Casper/index.html 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.
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.