dc.contributor.author Tonet, Adam dc.date.accessioned 2019-03-14T15:06:30Z dc.date.available 2019-03-14T15:06:30Z dc.identifier.uri http://hdl.handle.net/10464/14020 dc.description.abstract The spi calculus is a process algebra used to model cryptographic protocols. A process calculus is a means of modelling a system of concurrently interacting agents, and provides tools for the description of communications and synchronizations between those agents. The spi calculus is based on Robin Milner's pi calculus, which was itself based upon his Calculus of Communicating Systems (CCS). It was created by Martin Abadi and Andrew D. Gordon as an expansion of the pi calculus intended to focus on cryptographic protocols, and adds features such as the encryption and decryption of messages using keys. The Coq proof system is an interactive theorem prover that allows for the definition of types and functions, and provides means by which to prove properties about them. The spi calculus has been implemented in Coq and subsequently used to model and show an example proof of a property about a simple cryptographic protocol. This required the implementation of both the syntax and the semantics of the calculus, as well as the rules and axioms used to manipulate the syntax in proofs. We discuss the spi calculus in detail as defined by Abadi and Gordon, then the various challenges faced during the implementation of the calculus and our rationale for the decisions made in the process. en_US dc.language.iso eng en_US dc.publisher Brock University en_US dc.subject spi calculus en_US dc.subject coq en_US dc.subject cryptographic protocols en_US dc.subject software correctness en_US dc.title Modelling and Proving Cryptographic Protocols in the Spi Calculus using Coq en_US dc.type Electronic Thesis or Dissertation en_US dc.degree.name M.Sc. Computer Science en_US dc.degree.level Masters en_US dc.contributor.department Department of Computer Science en_US dc.degree.discipline Faculty of Mathematics and Science en_US
﻿