Symbolic protocol analysis for monoidal equational theories

We are interested in the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra. The main goal of this paper is to set up a general approach that works for a whole class of monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way (e.g. exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom). We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly rel...

• Type: Journal
• Year: 2008
• Where: IANDC
• Authors: Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen
• Keywords: Cryptographic Protocol, IANDC 2008, Protocol Analysis, Symbolic Constraints