Abstract:


Efficient Decision Procedures for Message 
Deducibility and Static Equivalence


Bruno Conchinha and David Basin and Carlos Caleiro



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.