Abstract
Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been extremely error prone. Most of the protocols found in the literature contain redundancies or security flaws. A simple logic has allowed us to describe the beliefs of trustworthy parties involved in authentication protocols and the evolution of these beliefs as a consequence of communication. We have been able to explain a variety of authentication protocols formally, to discover subtleties and errors in them, and to suggest improvements. In this paper we present the logic and then give the results of our analysis of four published protocols, chosen either because of their practical importance or because they serve to illustrate our method.
- 1 BAUER, R. K., BERSON, T. A., AND FEIERTAG, R.J. A key distribution protocol using event markers. ACM Trans. Comput. Syst. 1, 3 (Aug. 1983), 249-255. Google Scholar
- 2 BURROWS, M., ABADI, M., AND NEEDHAM, R.M. Authentication: A practical study in belief and action. In Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning about Knowledge (Asilomar, Ca., Feb. 1988) M. Vardi, Ed. Morgan Kaufmann, Los Altos, Calif., 1988, pp. 325-342. Google Scholar
- 3 BURROWS, M., ABADI, M., AND NEEDHAM, R.M. A logic of authentication. Rep. 39, Digital Equipment Corporation Systems Research Center, Palo Alto, Calif., Feb. 1989.Google Scholar
- 4 CCITT. CCITT draft recommendation X.509. The directory-authentication framework, version 7. CCITT, Gloucester, Nov. 1987.Google Scholar
- 5 DEMILLO, R. A., LYNCH, N. A., AND MERRITT, M.J. Cryptographic protocols. In Proceedings o/the 14th ACM Symposium on the Theory of Computing (San Francisco, May 1982), ACM, New York, 1982, pp. 383-400. Google Scholar
- 6 DENNING, D. E., AND SACCO, G.M. Timestamps in key distribution protocols. Commun. A CM 24, 8 (Aug. 1981), 533-536. Google Scholar
- 7 DOLEV, D., AND YAO, A.C. On the security of public key protocols. IEEE Trans. Inf. Theory IT-29, 2 (Mar. 1983), 198-208.Google Scholar
- 8 HALPERN, J. Y., AND MOSES, Y. O. Knowledge and common knowledge in a distributed environment. In Proceedings of the 3rd A CM Conference on the Principles of Distributed Computing (Vancouver, British Columbia, Aug. 1984), ACM, New York, 1984, pp. 480-490. Google Scholar
- 9 HALPERN, J. Y., MOSES, Y. 0., AND TUTTLE, M. R. A knowledge-based analysis of zero knowledge (preliminary report). In Proceedings of the 20th ACM Symposium on Theory of Computing (Chicago, Ill., May 1988), ACM, New York, 1988, pp. 132-147. Google Scholar
- 10 HOARE, C. A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576-580. Google Scholar
- 11 MERRITT, M. J., AND WOLPER, P.L. States of knowledge in cryptographic protocols. Draft.Google Scholar
- 12 MILLEN, J. K., CLARK, S. C., AND FREEDMAN, S.B. The interrogator: Protocol security analysis. IEEE Trans. So{tw. Eng. SE-13, 2 (Feb. 1987), 274-288. Google Scholar
- 13 MILLER, S. P., NEUMAN, C., SCHILLER, J. I., AND SALTZER, J.H. Kerberos authentication and authorization system. In Project Athena Technical Plan, Sect. E.2.1. MIT, Cambridge, Mass., July 1987.Google Scholar
- 14 National Bureau of Standards. Data encryption standard. Fed. Inf. Process. Stand. Publ. 46. National Bureau of Standards, Washington, D.C., Jan. 1977.Google Scholar
- 15 NEEDHAM, R. M., AND SCHROEDER, M. D. Using encryption for authentication in large networks of computers. Commun. ACM 2I, 12 (Dec. 1978), 993-999. Google Scholar
- 16 OTWAV, D., AND REES, O. Efficient and timely mutual authentication. Oper. Syst. Rev. 21, 1 (Jan. 1987), 8-10. Google Scholar
- 17 RIVEST, R. L., SHAMIR, A., AND ADLEMAN, L. A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM 21, 2 (Feb. 1978), 120-126. Google Scholar
- 18 SATYANARAYANAN, M. Integrating security in a large distributed system. ACM Trans. Comput. Syst. 7, 3 (Aug. 1989), 247-280. Google Scholar
- 19 VOYDOCK, V. L., AND KENT, S.T. Security mechanisms in high-level network protocols. ACM Comput. Surv. 15, 2 (June 1983), 135-171. Google Scholar
Index Terms
- A logic of authentication
Recommendations
A logic of authentication
SOSP '89: Proceedings of the twelfth ACM symposium on Operating systems principlesAuthentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been extremely error prone. Most of the protocols found in ...
Authentication for paranoids: multi-party secret handshakes
ACNS'06: Proceedings of the 4th international conference on Applied Cryptography and Network SecurityIn a society increasingly concerned with the steady assault on electronic privacy, the need for privacy-preserving techniques is both natural and justified. This need extends to traditional security tools such as authentication and key distribution ...
A logic of authentication
Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been extremely error prone. Most of the protocols found in ...
Comments