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.

Provided by: Springer Science+Business Media Topic: Security Date Added: Feb 2011 Format: PDF

Find By Topic