Technical reports

Mechanized proofs of security protocols:
Needham-Schroeder with public keys

Lawrence C. Paulson

January 1997, 20 pages

DOI: 10.48456/tr-413

Abstract

The inductive approach to verifying security protocols, previously applied to shared-key encryption, is here applied to the public key version of the Needham-Schroeder protocol. As before, mechanized proofs are performed using Isabelle/HOL. Both the original, flawed version and Lowe’s improved version are studied; the properties proved highlight the distinctions between the two versions. The results are compared with previous analyses of the same protocol. The analysis reported below required only 30 hours of the author’s time. The proof scripts execute in under three minutes.

Full text

PDF (0.1 MB)
PS (0.0 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-413,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Mechanized proofs of security protocols: Needham-Schroeder
         	   with public keys}},
  year = 	 1997,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-413.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-413},
  number = 	 {UCAM-CL-TR-413}
}