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.

Security protocol specification and verification with AnBx

BUGLIESI, Michele;CALZAVARA, STEFANO;
2016

Abstract

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.
File in questo prodotto:
File Dimensione Formato  
jisa16.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 417.92 kB
Formato Adobe PDF
417.92 kB Adobe PDF   Visualizza/Apri
1-s2.0-S2214212616300564-main.pdf

accesso aperto

Tipologia: Versione dell'editore
Licenza: Accesso chiuso-personale
Dimensione 840.09 kB
Formato Adobe PDF
840.09 kB Adobe PDF Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10278/3685123
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 5
social impact