@TechReport{	  conchinha.ea:efficient:2010-b,
  abstract	= {We consider two standard notions in formal security
		  protocol analysis: message deducibility and static
		  equivalence under equational theories. We present
		  polynomial-time algorithms for deciding both problems under
		  subterm convergent equational theories and under a theory
		  representing symmetric encryption with the prefix property.
		  For subterm convergent theories, polynomial-time algorithms
		  for both problems are well-known. However, we achieve a
		  significantly better asymptotic complexity than existing
		  approaches. For the prefix theory, we are not aware of any
		  polynomial-time algorithms for static equivalence.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},
  institution	= {ETH Z\"urich},
  language	= {USenglish},
  pdf		= {papers/2010/FAST Technical Report.pdf},
  title		= {Efficient Decision Procedures for Message Deducibility and
		  Static Equivalence},
  url		= {http://www.inf.ethz.ch/research/disstechreps/techreports/show?serial=680&lang=en}
		  ,
  year		= 2010,
  user		= {brunoco}
}