  Informal arguments that cryptographic protocols are secure can be made
rigorous using inductive definitions. The approach is based on ordinary
predicate calculus and copes with infinite-state systems. Proofs are generated
using Isabelle/HOL. The human effort required to analyze a protocol can be as
little as a week or two, yielding a proof script that takes a few minutes to
run.
  Protocols are inductively defined as sets of traces. A trace is a list of
communication events, perhaps comprising many interleaved protocol runs.
Protocol descriptions incorporate attacks and accidental losses. The model spy
knows some private keys and can forge messages using components decrypted from
previous traffic. Three protocols are analyzed below: Otway-Rees (which uses
shared-key encryption), Needham-Schroeder (which uses public-key encryption),
and a recursive protocol by Bull and Otway (which is of variable length).
  One can prove that event $ev$ always precedes event $ev'$ or that property
$P$ holds provided $X$ remains secret. Properties can be proved from the
viewpoint of the various principals: say, if $A$ receives a final message from
$B$ then the session key it conveys is good.
