Sciweavers

Share
IFIP
2010
Springer

Efficient Decision Procedures for Message Deducibility and Static Equivalence

8 years 7 months ago
Efficient Decision Procedures for Message Deducibility and Static Equivalence
Abstract. 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. Key words: security protocols, equational theories, deducibility, static equivalence
Bruno Conchinha, David A. Basin, Carlos Caleiro
Added 18 May 2011
Updated 18 May 2011
Type Journal
Year 2010
Where IFIP
Authors Bruno Conchinha, David A. Basin, Carlos Caleiro
Comments (0)
books