Close menu


Sunderland Repository records the research produced by the University of Sunderland including practice-based research and theses.

Security Protocol Specification and Verification with AnBx

WarningThere is a more recent version of this item available.

Bugliesi, Michele, Calzavara, Stefano, Mödersheim, Sebastian and Modesti, Paolo (2016) Security Protocol Specification and Verification with AnBx. Journal of Information Security and Applications. ISSN 2214-2126 (In Press)

Item Type: Article


Designing distributed protocols is complex and requires actions at very different levels: from the design of an interaction flow supporting the desired application-specific guarantees, to the selection of the most appropriate network-level protection mechanisms.
To tame this complexity, we propose AnBx, a formal protocol specification language based on the popular Alice & Bob notation. AnBx offers channels as the main abstraction for communication, providing different authenticity and/or confidentiality guarantees for message transmission.
AnBx extends existing proposals in the literature with a novel notion of forwarding channels, enforcing specific security guarantees from the message originator to the final recipient along a number of intermediate forwarding agents. We give a formal semantics of AnBx in terms of a state transition system expressed in the AVISPA Intermediate Format. We devise an ideal channel model
and a possible cryptographic implementation, and we show that, under mild restrictions, the two representations coincide, thus making AnBx amenable to automated verification with different tools. We demonstrate the benefits of the declarative specification style distinctive of AnBx by revisiting the design of two existing e-payment protocols, iKP and SET.

jisa2016.pdf - Accepted Version

Download (455kB) | Preview

More Information

Depositing User: Paolo Modesti


Item ID: 6526
Identification Number:
ISSN: 2214-2126
Official URL:

Users with ORCIDS

Catalogue record

Date Deposited: 26 Jul 2016 13:09
Last Modified: 02 Jul 2019 09:11


Author: Michele Bugliesi
Author: Stefano Calzavara
Author: Sebastian Mödersheim
Author: Paolo Modesti

University Divisions

Faculty of Technology > School of Computer Science


Computing > Network Computing
Computing > Programming

Actions (login required)

View Item View Item

Available Versions of this Item