2010 | OriginalPaper | Buchkapitel
AnBx - Security Protocols Design and Verification
verfasst von : Michele Bugliesi, Paolo Modesti
Erschienen in: Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Designing distributed protocols is challenging, as it requires actions at very different levels: from the choice of network-level mechanisms to protect the exchange of sensitive data, to the definition of structured interaction patterns to convey application-specific guarantees. Current security infrastructures provide very limited support for the specification of such guarantees. As a consequence, the high-level security properties of a protocol typically must often be hard-coded explicitly, in terms of low-level cryptographic notions and devices which clutter the design and undermine its scalability and robustness.
To counter these problems, we propose an extended
Alice & Bob
notation for protocol narrations (
AnBx
) to be employed for a purely declarative modelling of distributed protocols. These abstractions provide a compact specification of the high-level security guarantees they convey, and help shield the design from the details of the underlying cryptographic infrastructure. We discuss an implementation of the abstractions based on a translation from the
AnBx
notation to the AnB language supported by the OFMC [1,2] verification tool. We show the practical effectiveness of our approach by revisiting the
iKP
e-payment protocols, and showing that the security goals achieved by our declarative specification outperform those offered by the original protocols.