Alice and Bob notation is a popular way to describe security protocols: it is intuitive, succinct, and yet expressive. Several formal specification languages are based on this notation, where the semantics is given by translation to a low-level language that describes transition systems. Besides the
theoretical aspect of the translation, it has immediate practical applications: it is straightforward to connect a large variety of verification tools by implementing for each tool a suitable output back-end of the translator. One of the most severe limitation of previous formal approaches using Alice and Bob notation is the lack of algebraic reasoning, which is required for instance for the correct interpretation of Diffie-Hellman based protocols. As a
consequence, most of the previous approaches can either not 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. Our semantics also allows for two models of decryption, explicit and implicit, which is relevant for the efficiency of verification tools.
By: Sebastian Moedersheim
Published in: RZ3709 in 2008
Questions about this service can be mailed to reports@us.ibm.com .
