@MASTERSTHESIS\{IMM2012-06355,
    author       = "A. A. Olsen",
    title        = "Extended AnB for Web Services",
    year         = "2012",
    school       = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk",
    address      = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    note         = "Supervised by Associate Professor Sebastian Alexander M{\"{o}}dersheim, samo@imm.dtu.dk, {DTU} Informatics",
    url          = "http://www.imm.dtu.dk/English.aspx",
    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 differently 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."
}