@InProceedings{ basin.ea:algebraic:2005-b,
abstract = {Many security protocols fundamentally depend on the
algebraic properties of cryptographic operators. It is
however difficult to handle these properties when formally
analyzing protocols, since basic problems like the equality
of terms that represent cryptographic messages are
undecidable, even for relatively simple algebraic theories.
We present a framework for security protocol analysis that
can handle algebraic properties of cryptographic operators
in a uniform and modular way. Our framework is based on two
ideas: the use of modular rewriting to formalize a
generalized equational deduction problem for the Dolev-Yao
intruder, and the introduction of two parameters that
control the complexity of the equational unification
problems that arise during protocol analysis by bounding
the depth of message terms and the operations that the
intruder can perform when analyzing messages. We motivate
the different restrictions made in our model by
highlighting different ways in which undecidability arises
when incorporating algebraic properties of cryptographic
operators into formal protocol analysis.},
author = {David Basin and Sebastian M{\"o}dersheim and Luca
Vigan{\`o}},
booktitle = {LPAR 2005},
editor = {Geoff Sutcliffe and Andrei Voronkov},
isbn = {0302-9743},
language = {USenglish},
month = {December},
pages = {549--564},
publisher = {Springer-Verlag},
series = {LNAI},
title = {Algebraic Intruder Deductions},
volume = 3835,
year = 2005
}