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 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.