Algebraic Properties in Alice and Bob Notation (Extended Version, revised October 2008)

Alice and Bob notation is a popular way to describe security protocols: it is intuitive, succinct, and yet expressive. Several formal protocol specification languages are based on this notation. One of the most severe limitations of these languages is the lack of algebraic reasoning, which is required for instance for the correct interpretation of Diffie-Hellman based protocols. As a consequence, previous approaches either cannot handle such protocols at all or require manual annotation. We generalize previous approaches and give the first formal semantics for a language based on Alice and Bob notation that is defined over an arbitrary algebraic theory. In particular, it defines unambiguously how the protocol is supposed to be executed by honest agents, based on the considered algebraic properties of the operators.

The revised version is attached as PDF file. The first version of this report can be obtained from
A condensed version of this report has appeared in: Proc. 4th Int'l Conf. on Availability, Reliability and Security "ARES 2009" Fukuoka, Japan, (IEEE Computer Society, March 2009), 433-440

By: Sebastian Moedersheim

Published in: RZ3709 in 2008


This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.


Questions about this service can be mailed to .