Abstract
Three experimental methods have been developed to help apply formal methods to the security verification of cryptographic protocols of the sort used for key distribution and authentication. Two of these methods are based on Prolog programs, and one is based on a general-purpose specification and verification system. All three combine algebraic with state-transition approaches. For purposes of comparison, they were used to analyze the same example protocol with a known flaw.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abadi, M., and M. R. Tuttle, A Semantics for a Logic of Authentication, Proceedings of the 10th Annual ACM Symposium on Distributed Computing, ACM Press, New York, August 1991, pp. 201–206.
Bieber, P., A Logic of Communication in a Hostile Environment, Proceedings of the Computer Security Foundations Workshop III, IEEE Computer Society Press, New York, June 1990, pp. 14–22.
Boudet, A., Unification in a Combination of Equational Theories: an Efficient Algorithm, Proceedings of the 10th International Conference on Automated Deduction, Springer-Verlag, New York, 1990, pp. 292–307.
Burns, J., and C. J. Mitchell, A Security Scheme for Resource Sharing Over a Network, Comput. Security, Vol. 9, 1990, pp. 67–76.
Burrows, M., M. Abadi, and R. M. Needham, A Logic of Authentication, ACM Trans. Comput. Systems, Vol. 8, No. 1, February 1990, pp. 18–36.
Clocksin, W. F., and C. S. Mellish, Programming in Prolog, Springer-Verlag, New York, 1984.
Denning, D. E., and G. M. Sacco, Timestamps in Key Distribution Protocols, Comm. ACM, Vol. 24, No. 8, August 1981, pp. 533–536.
Dolev, D., and A. Yao, On the Security of Public-Key Protocols, IEEE Trans. Inform. Theory, Vol. 29, 1983, pp. 198–203.
Eckmann, S. T., and R. A. Kemmerer, INATEST: An Interactive Environment for Testing Formal Specifications, Third Workshop on Formal Verification, Pajaro Dunes, CA, February, 1985, ACM—Software Engrg Notes, Vol. 10, No. 4, August 1985, pp. 17–18.
Goldwasser, S., S. Micali, and C. Rackoff, The Knowledge Complexity of Interactive Proof Systems, Siam J. Comput., Vol. 18, No. 1, February 1989, pp. 186–208.
Holzmann, G., The Design and Validation of Computer Protocols, Prentice-Hall, Englewood Cliffs, NJ, 1991.
Kemmerer, R. A., Analyzing Encryption Protocols Using Formal Verification Techniques, IEEE J. Selected Areas Commun., Vol. 7, No. 4, May 1989, pp. 448–457.
Kemmerer, R. A., Integrating Formal Methods into the Development Process, IEEE Software, September 1990, pp. 37–50.
Kemmerer, R. A., Analyzing the Tatebayashi-Matsuzaki-Newman Protocol Using Inatest, UCSB Report No. TRCS91–05, Computer Science Department, University of California, Santa Barbara, CA, April 1991.
Longley, D., Expert Systems Applied to the Analysis of Key Management Schemes, Comput. Security, Vol. 6, 1987, pp. 54–67.
Massey, J. L., Cryptography and Provability, Proceedings of the Workshop on Mathematical Concepts of Dependable Systems, Mathematisches Forschunginstitut Oberwolfach, Oberwolfach, April 1990.
Meadows, C., A System for the Specification and Verification of Key Management Protocols, Proceedings of the 1991 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, New York, 1991, pp. 182–195.
Meadows, C., Applying Formal Methods to the Analysis of a Key Management Protocol, J. Comput. Security, Vol. 1, No. 1, 1992, pp. 5–53.
Merritt, M., and P. Wolper, States of Knowledge in Cryptographic Protocols, unpublished manuscript, 1985.
Millen, J. K., The Interrogator: A Tool for Cryptographic Protocol Security, Proceedings of the 1984 Symposium on Security and Privacy, IEEE Computer Society Press, New York, pp. 134–141.
Millen, J. K., S. C. Clark, and S. B. Freedman, The Interrogator: Protocol Security Analysis, IEEE Trans. Software Engrg., Vol. 13, No. 2, February 1987.
Moore, J. H., Protocol Failures in Cryptosystems, Proc. IEEE, Vol. 76, No. 5, May 1988, pp. 564–602.
Needham, R. M., and M. D. Schroeder, Using Encryption for Authentication in Large Networks of Computers, Comm. ACM, Vol. 21, No. 12, December 1978, pp. 993–999.
Rety, P., C. Kirchner, H. Kirchner, and P. Lescanne, NARROWER: A New Algorithm for Unification and Its Applications to Logic Programming, in Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 202, Jean-Pierre Jouannaud, ed., Springer-Verlag, Berlin, 1985, pp. 141–157.
Scheid, J., and S. Holtsberg, Ina Jo Specification Language Reference Manual, TM-6021, Unisys Corporation, Culver City, CA, May 1989.
Simmons, G. J., How To (Selectively) Broadcast a Secret, Proceedings of the 1985 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, New York, 1985, pp. 108–113.
Syverson, P. and Meadows, C., A Logical Language for Specifying Cryptographic Protocol Requirements, in Proceedings of the 1993 IEEE Computer Society Symposium on Security and Privacy, IEEE Computer Society Press, New York, 1993, pp. 165–177.
Tatebayashi, M., N. Matsuzaki, and D. B. Newman, Key Distribution Protocol for Digital Mobile Communication Systems, in Advances in Cryptology—CRYPTO '89, Lecture Notes in Computer Science, Vol. 435, G. Brassard, ed., Springer-Verlag, New York, 1991, pp. 324–333.
Toussaint, M.-J., Separating the Specification and Implementation Phases in Cryptology (Extended Abstract), Computer Security, ESORICS 92, Lecture Notes in Computer Science, Vol. 648, Springer-Verlag, Berlin, 1992, pp. 77–101.
Author information
Authors and Affiliations
Additional information
Communicated by Thomas Beth
Rights and permissions
About this article
Cite this article
Kemmerer, R., Meadows, C. & Millen, J. Three systems for cryptographic protocol analysis. J. Cryptology 7, 79–130 (1994). https://doi.org/10.1007/BF00197942
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF00197942