Technical reports
Proving properties of security protocols by induction
December 1996, 24 pages
DOI: 10.48456/tr-409
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-409.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-409},
number = {UCAM-CL-TR-409}
}