A logic of authentication
- 1 February 1990
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computer Systems
- Vol. 8 (1) , 18-36
- https://doi.org/10.1145/77648.77649
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.Keywords
This publication has 10 references indexed in Scilit:
- Integrating security in a large distributed systemACM Transactions on Computer Systems, 1989
- The Interrogator: Protocol Secuity AnalysisIEEE Transactions on Software Engineering, 1987
- Efficient and timely mutual authenticationACM SIGOPS Operating Systems Review, 1987
- A key distribution protocol using event markersACM Transactions on Computer Systems, 1983
- Security Mechanisms in High-Level Network ProtocolsACM Computing Surveys, 1983
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Timestamps in key distribution protocolsCommunications of the ACM, 1981
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978
- A method for obtaining digital signatures and public-key cryptosystemsCommunications of the ACM, 1978
- An axiomatic basis for computer programmingCommunications of the ACM, 1969