Technical reports

Authentication: a practical study in belief and action

Michael Burrows, Martín Abadi, Roger Needham

June 1988, 19 pages

DOI: 10.48456/tr-138

Abstract

Questions of belief and action are essential in the analysis of 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 protocols differ subtly with respect to the required initial assumptions of the participants and their final beliefs. Our fomalism has enabled us to isolate and express these differences in a way that was not previously possible, and it has drawn attention to features of the protocols of which we were perviously unaware. The reasoning about particular 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 real protocols from the literature. The final sections deal with a formal semantics of the logic and conclusions.

Full text

PDF (1.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-138,
  author =	 {Burrows, Michael and Abadi, Mart{\'\i}n and Needham, Roger},
  title = 	 {{Authentication: a practical study in belief and action}},
  year = 	 1988,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-138.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-138},
  number = 	 {UCAM-CL-TR-138}
}