Show simple item record

dc.contributor.authorTonet, Adam
dc.date.accessioned2019-03-14T15:06:30Z
dc.date.available2019-03-14T15:06:30Z
dc.identifier.urihttp://hdl.handle.net/10464/14020
dc.description.abstractThe 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.isoengen_US
dc.publisherBrock Universityen_US
dc.subjectspi calculusen_US
dc.subjectcoqen_US
dc.subjectcryptographic protocolsen_US
dc.subjectsoftware correctnessen_US
dc.titleModelling and Proving Cryptographic Protocols in the Spi Calculus using Coqen_US
dc.typeElectronic Thesis or Dissertationen_US
dc.degree.nameM.Sc. Computer Scienceen_US
dc.degree.levelMastersen_US
dc.contributor.departmentDepartment of Computer Scienceen_US
dc.degree.disciplineFaculty of Mathematics and Scienceen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record