Automated Proof of Authentication Protocols in a Logic of Events
Using the language of event orderings and event classes,and using a type of atoms to represent nonces, keys, signatures,and ciphertexts, we give an axiomatization of a theory in which authentication protocols can be formally defined and strong authentication properties proven. This theory is inspired by PCL, the protocol composition logic defined by Datta, Derek, Mitchell, and Roy.
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 wellfounded 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.
by Mark Bickford