@article{DLL+08,
title = { Symbolic protocol analysis for monoidal equational theories },
author = {Delaune, St\'ephanie and Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
month = {feb},
year = {2008},
journal = {Information and Computation},
pages = {312-351},
publisher = {Elsevier Science Publishers},
volume = {206},
team = {DCS},
abstract = {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 relies on the correspondence between a monoidal theory~{\(E\)} and a semiring~{\(S{\{\_}}E\)} which we use to deal with the symbolic constraints. We~show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The~resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight.},
}
