The Inductive Approach to Verifying Cryptographic Protocols

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 e#ort 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 tra#c. Three protocols are analyzed below: OtwayRees (which uses shared-key encryption), Needham-Schroeder (which uses public-key encryption), and a recursive protocol [9] (which is of variable length). One can prove that event ev always precedes event ev # or that property P holds provided X remains ...