Abstract:



Efficient Decision Procedures for Message Deducibility 
and Static Equivalence


Bruno Conchinha and David Basin and Carlos Caleiro



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.