@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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},
}