skip to main content
article
Free Access

A logic of authentication

Published:01 February 1990Publication History
Skip Abstract Section

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.

References

  1. 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 ScholarGoogle Scholar
  2. 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 ScholarGoogle Scholar
  3. 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 ScholarGoogle Scholar
  4. 4 CCITT. CCITT draft recommendation X.509. The directory-authentication framework, version 7. CCITT, Gloucester, Nov. 1987.Google ScholarGoogle Scholar
  5. 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 ScholarGoogle Scholar
  6. 6 DENNING, D. E., AND SACCO, G.M. Timestamps in key distribution protocols. Commun. A CM 24, 8 (Aug. 1981), 533-536. Google ScholarGoogle Scholar
  7. 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 ScholarGoogle Scholar
  8. 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 ScholarGoogle Scholar
  9. 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 ScholarGoogle Scholar
  10. 10 HOARE, C. A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576-580. Google ScholarGoogle Scholar
  11. 11 MERRITT, M. J., AND WOLPER, P.L. States of knowledge in cryptographic protocols. Draft.Google ScholarGoogle Scholar
  12. 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 ScholarGoogle Scholar
  13. 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 ScholarGoogle Scholar
  14. 14 National Bureau of Standards. Data encryption standard. Fed. Inf. Process. Stand. Publ. 46. National Bureau of Standards, Washington, D.C., Jan. 1977.Google ScholarGoogle Scholar
  15. 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 ScholarGoogle Scholar
  16. 16 OTWAV, D., AND REES, O. Efficient and timely mutual authentication. Oper. Syst. Rev. 21, 1 (Jan. 1987), 8-10. Google ScholarGoogle Scholar
  17. 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 ScholarGoogle Scholar
  18. 18 SATYANARAYANAN, M. Integrating security in a large distributed system. ACM Trans. Comput. Syst. 7, 3 (Aug. 1989), 247-280. Google ScholarGoogle Scholar
  19. 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 ScholarGoogle Scholar

Index Terms

  1. A logic of authentication

              Recommendations

              Comments

              Login options

              Check if you have access through your login credentials or your institution to get full access on this article.

              Sign in

              Full Access

              • Published in

                cover image ACM Transactions on Computer Systems
                ACM Transactions on Computer Systems  Volume 8, Issue 1
                Feb. 1990
                82 pages
                ISSN:0734-2071
                EISSN:1557-7333
                DOI:10.1145/77648
                Issue’s Table of Contents

                Copyright © 1990 ACM

                Publisher

                Association for Computing Machinery

                New York, NY, United States

                Publication History

                • Published: 1 February 1990
                Published in tocs Volume 8, Issue 1

                Permissions

                Request permissions about this article.

                Request Permissions

                Check for updates

                Qualifiers

                • article

              PDF Format

              View or Download as a PDF file.

              PDF

              eReader

              View online with eReader.

              eReader