Efficient Decision Procedures for Message Deducibility and Static Equivalence
The authors consider two standard notions in formal security protocol analysis: message deducibility and static equivalence under equational theories. They 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, their algorithms have a significantly better asymptotic complexity than existing approaches.