@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
}