Computer Laboratory

Technical reports

Proving properties of security protocols by induction

Lawrence C. Paulson

December 1996, 24 pages

Abstract

Security protocols are formally specified in terms of traces, which may involve many interleaved protocol runs. Traces are defined inductively. Protocol descriptions model accidental key losses as well as attacks. The model spy can send spoof messages made up of components decrypted from previous traffic.

Correctness properties are verified using the proof tool Isabelle/HOL. Several symmetric-key protocols have been studied, including Needham-Schroeder, Yahalom and Otway-Rees. A new attack has been discovered in a variant of Otway-Rees (already broken by Mao and Boyd). Assertions concerning secrecy and authenticity have been proved.

The approach rests on a common theory of messages, with three operators. The operator “parts” denotes the components of a set of messages. The operator “analz” denotes those parts that can be decrypted with known keys. The operator “synth” denotes those messages that can be expressed in terms of given components. The three operators enjoy many algebraic laws that are invaluable in proofs.

Full text

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

BibTeX record

@TechReport{UCAM-CL-TR-409,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Proving properties of security protocols by induction}},
  year = 	 1996,
  month = 	 dec,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-409.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-409}
}