Extended AnB for Web Services |
Allan Asp Olsen
|
| Abstract | Formal protocol analysis is an important tool for computer security. While there has been a lot of formal mathematical analysis of cryptology the usual security problems in practice are the results of poorly applied cryptology or security problems in the programs themselves. For example some protocols have
flaws that aren't found in several years after their publication. While one solution might be to just use well de fined protocols this is not always possible. E.g. Sometimes new protocols need to be invented. While security protocols have been analysed for many years by hand it is often easy to miss mistakes in the design of the protocol.
This has led to the development of several tools for formal analysis of protocols. This includes Casper, Common Authentication Protocol Specification Language (CAPSL)[1] and Open-Source Fixed-Point Model-Checker (OFMC)[4][5]. The purpose of this thesis is to extend on the Alice and Bob notation (AnB) which is used for specifying protocols, these can be analysed with OFMC or similar tools. Classic AnB lacks support for problems that require a more persistent storage than a single protocol run. One such protocol is ASW[3] which allows users to digitally sign a protocol in a fair way (ie. one participant of the negotiation cannot have a signed contract without the other part acquiring one). This may require a trusted third party in the case that they disagree and this trusted third party has to act di fferently depending on the messages received so far.
To accomplish it's task OFMC translates from AnB to Automated Validation of Internet Security Protocols and Applications Intermediate Format(AVISPA IF). To extend AnB into the language which we refer to as Web Service Alice and Bob notation (WS-AnB) it was necessary to de fine a formal description of the translation from these additions into AVISPA IF as well. |
| Type | Master's thesis [Academic thesis] |
| Year | 2012 |
| Publisher | Technical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk |
| Address | Asmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark |
| Series | IMM-M.Sc.-2012-63 |
| Note | |
| Electronic version(s) | [pdf] |
| Publication link | http://www.imm.dtu.dk/English.aspx |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |