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

• Type: Journal
• Year: 2010
• Where: IFIP
• Authors: Bruno Conchinha, David A. Basin, Carlos Caleiro
• Keywords: Equational Theories, IFIP 2010, Polynomial-time Algorithms, Programming Languages, Static Equivalence