Efficient Decision Procedures for Message Deducibility and Static Equivalence

摘要

We consider two standard notions in formal security protocol analysis: message deducibility and static equivalence under equa-tional 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 complexity than 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.