An approach to the formal verification of the two-party cryptographic protocols

ABSTRACT

A general method, which can be used to verify the two-party cryptographic protocols, is present in this paper. Our approach makes use of running modes of the two-party cryptographic protocols to analyze the protocols. Based on this method, the verification of the protocols becomes independent of model checking tools. Finally, this approach is illustrated with an example on the Needham-Schroeder public-key protocol.

REFERENCES

• 1: Martín Abadi , Mark R. Tuttle, A semantics for a logic of authentication (extended abstract), Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.201-216, August 19-21, 1991, Montreal, Quebec, Canada [doi>10.1145/112600.112618]
• 2: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 3: [3] Z. Dang and R. A. Kemmerer. Using the ASTRAL Model Checker for Cryptographic Protocol Analysis. In Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. Available via URL: http://dimacs.rutgers.edu/Workshops/Security/program2/program.html.
• 4: [4] G. Denker, J. Meseguer and C. Talott. Protocol Specification and Analysis in Maude. In Proceedings of Workshop on Formal Methods and Security Protocols, June 1998. Available via URL: http://www.cs.bell-labs.com/who/nch/fmsp/index.html.
• 5: [5] Li Gong, Roger Needham, and Raphael Yahalom, Reasoning About Belief in Cryptographic Protocols. In Proceedings 1990 IEEE Computer Society Symposium on Research in Security and Privacy. IEEE Computer Society, 234-248, 1990.
• 6: [6] Volker Kessler and Gabriele Wedel. AUTLOG--An advanced logic of authentication. In Proceedings of the Computer Security Foundations Workshop VII. IEEE Computer Society Press, 90-99, 1994.
• 7: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 8: [8] G. Lowe, Towards a completeness result for model checking of security protocols. Technical Report 1998/6, Department of Mathematics and Computer Science, University of Leicester, 1998. Available from http://www.mcs.le.ac.uk/~glowe/Security/Papers/completeness.ps.gz.
• 9: Gavin Lowe , Bill Roscoe, Using CSP to Detect Errors in the TMN Protocol, IEEE Transactions on Software Engineering, v.23 n.10, p.659-669, October 1997 [doi>10.1109/32.637148]
• 10: [10] W. Marrero, E. Clarke, and S. Jha. A model checker for authentication protocols. In Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. Available via URL: http://dimacs.rutgers.edu/Workshops/Security/program2/program.html.
• 11: J. C. Mitchell , M. Mitchell , U. Stern, Automated analysis of cryptographic protocols using Mur/spl phi/, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, May 04-07, 1997
• 12: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 13: [13] SMV. Available via URL: http://www.cs.cmu.edu/~modelcheck/.
• 14: Paul F. Syverson , Paul C. Van Oorschot, On Unifying Some Cryptographic Protocol Logics, Proceedings of the 1994 IEEE Symposium on Security and Privacy, p.14, May 16-18, 1994
• 15: [15] Yuqing Zhang, Kai Chen, and Guozhen Xiao. Automated Analysis of Cryptographic Protocol Using SMV. In Proceedings of International Workshop on Cryptographic Techniques and E-Commerce (CrypTEC '99), July 1999.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS

  E. Data
  E.3 DATA ENCRYPTION
      Subjects: Public key cryptosystems

General Terms:
Design, Performance, Reliability, Security, Standardization, Theory, Verification