Automating and simplifying agreement and secrecy verification using PVS

Type of content
Theses / Dissertations
Publisher's DOI/URI
Thesis discipline
Computer Science
Degree name
Master of Science
Publisher
University of Canterbury. Computer Science
Journal Title
Journal ISSN
Volume Title
Language
Date
2001
Authors
Renaud, André
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.

Description
Citation
Keywords
Ngā upoko tukutuku/Māori subject headings
ANZSRC fields of research
Rights
Copyright André Renaud