[ Changed 25th January 1997 ]
Security protocols can be formally specified in terms of traces, which may involve many interleaved 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.
The approach has been implemented using the proof assistant Isabelle/HOL. Several symmetric-key protocols have been analysed, 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 can be 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.