@InProceedings{	  conchinha.ea:efficient:2010,
  abstract	= {Abstract. We consider two standard notions in formal
		  security protocol analysis: message deducibility and static
		  equivalence under equational theories. We present new
		  polynomial-time algorithms for deciding both notions under
		  subterm convergent equational theories and under a theory
		  representing symmetric encryption with the prefix property.
		  For these equational theories, polynomial-time algorithms
		  for the decision problems associated to both notions are
		  well-known (although this has not been proven for static
		  equivalence under the prefix theory). However, our
		  algorithms have a significantly better asymptotic
		  complexitythan existing approaches.As an application, we
		  use our algorithm for static equivalence to discover
		  off-line guessing attacks on the Kerberos protocol when
		  implemented using a symmetric encryption scheme for which
		  the prefix property holds.},
  author	= {Bruno Conchinha and David Basin and Carlos Caleiro},
  booktitle	= {Formal Aspects in Security and Trust (FAST '2010)},
  copyright	= {Springer},
  copyrighturl	= {http://www.springerlink.com/content/n3323gh2417k/#section=862333&page=1&locus=2}
		  ,
  editor	= {Pierpaolo Degano and Sandro Etalle and Joshua D. Guttman},
  filelabel	= {10.1007/978-3-642-19751-2{\_}3},
  language	= {USenglish},
  pages		= {34--49},
  pdf		= {papers/2010/Springer Fulltext.pdf},
  publisher	= {Springer Berlin / Heidelberg},
  series	= {LNCS},
  title		= {Efficient Decision Procedures for Message Deducibility and
		  Static Equivalence},
  url		= {http://dx.doi.org/10.1007/978-3-642-19751-2_3},
  volume	= 6561,
  year		= 2010,
  user		= {bgeiser}
}v