Abstract

Questions of belief are essential in analysing protocols for the authentication of principals in distributed computing systems. In this paper we motivate, set out, and exemplify a logic specifically designed for this analysis: we show how various protocols differ subtly with respect to the required initial assumptions of the participants and their final beliefs. Our formalism has enabled us to isolate and express these differences with a precision that was not previously possible. It has drawn attention to features of protocols of which we and their authors were previously unaware, and allowed us to suggest improvements to the protocols. The reasoning about some protocols has been mechanically verified. This paper starts with an informal account of the problem, goes on to explain the formalism to be used, and gives examples of its application to protocols from the literature, both with shared-key cryptography and with public-key cryptography. Some of the examples are chosen because of their practical importance, whereas others serve to illustrate subtle points of the logic and to explain how we use it. We discuss extensions of the logic motivated by actual practice; for example, to account for the use of hash functions in signatures. The final sections contain a formal semantics of the logic and some conclusions.

Keywords

Formalism (music)Computer scienceTheoretical computer scienceCryptographyHash functionKey (lock)Cryptographic protocolAuthentication (law)Semantics (computer science)Public-key cryptographyComputer securityProgramming languageEncryption

Related Publications

Publication Info

Year
1989
Type
article
Volume
426
Issue
1871
Pages
233-271
Citations
627
Access
Closed

External Links

Social Impact

Altmetric

Social media, news, blog, policy document mentions

Citation Metrics

627
OpenAlex

Cite This

Michael T. Burrows, M. Abadi, Roger M. Needham (1989). A logic of authentication. Proceedings of the Royal Society of London A Mathematical and Physical Sciences , 426 (1871) , 233-271. https://doi.org/10.1098/rspa.1989.0125

Identifiers

DOI
10.1098/rspa.1989.0125