AnB-API: Extending AnB with APIs and persistent storage |
|
Abstract | In this thesis we introduce a security protocol modelling language, AnB-API, which is designed as an extension to another security protocol modelling language AnB. With AnB-API we extend the capabilities of AnB to support modelling of protocols that make use of an API based communications model and persistent storage. We formally describe the semantics of AnB-API and how it is compiled into AIF, a lower level language, and how that is translated into Horn Clauses that can be verified to give proof of security. We also give examples of protocol specifications written in AnB-API and explain how they utilise the new features of AnB-API. |
Type | Master's thesis [Academic thesis] |
Year | 2016 |
Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science |
Address | Richard Petersens Plads, Building 324, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk |
Series | DTU Compute M.Sc.-2016 |
Note | |
Electronic version(s) | [pdf] |
Publication link | http://www.compute.dtu.dk/English.aspx |
BibTeX data | [bibtex] |
IMM Group(s) | Computer Science & Engineering |