Proving properties of security protocols by induction

Informal justifications of security protocols involve arguing backwards that various events are impossible. Inductive definitions can make such arguments rigorous, The resulting proofs are complicated, bug can be generated reasonably quickly using the proof tool Isabelle/HOL. There is no restriction to finite-state systems and the approach is not based on belief logics. Protocols are inductively defined as sets of traces, traces, which may involve many interleaved protocol runs. 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. Several key distribution protocols have been studied including Needham-Schroeder, Yahalom and Otway-Rees. The method applies to both symmetric-key and public-key protocols. 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.