Automated Proof of Authentication Protocols in a Logic of Events
by Mark Bickford
We developed a general purpose tactic (in the NuPrl theorem prover), and applied it to automatically prove that several protocols satisfy a strong authentication property. Several unexpected subtleties exposed in this development are addressed with new concepts (legal protocols, and a fresh signature criterion) and reasoning that makes use of a well-founded causal ordering on events.
This work shows that proofs in a logic like PCL can be automated, provides a new and possibly simpler axiomatization for a theory of authentication, and addresses some issues raised in a critique of PCL.
bibTex ref: Bic10