Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Symbolic protocol analysis for monoidal equational theories. Information and Computation, 206(2-4):312–351, Elsevier Science Publishers, February 2008.
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.
@article{DLLT-IC07,
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.},
author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and
Lugiez, Denis and Treinen, Ralf},
OPTDOI = {10.1016/j.ic.2007.07.005},
journal = {Information and Computation},
month = feb,
number = {2-4},
pages = {312-351},
publisher = {Elsevier Science Publishers},
title = {Symbolic protocol analysis for monoidal equational
theories},
volume = {206},
year = {2008},
nmonth = {2},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}