Automating and Simplifying Agreement and Secrecy Verification Using PVS
Andre Renaud
Department of Computer Science
University of Canterbury
Abstract
In this thesis we present a system for assisting with theorem proving of security protocols. The desirability of theorem proving is examined and a method of automating the encoding, and some sections of the proof, are demonstrated. We also discuss various aspects of two different classes of security properties: secrecy and agreement. We demonstrate how our system can be used via two case study protocols, NetBill and SET. The proof can be decomposed into various sub-lemmas, most of which can be proven automatically, and then used to simplify the proofs of the final theorems of interest.