Access Restriction

Author Conchinha, Bruno ♦ Basin, David ♦ Caleiro, Carlos
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Static Equivalence ♦ Message Deducibility ♦ Efficient Decision Procedure ♦ Prefix Property ♦ Polynomial-time Algorithm ♦ Equational Theory ♦ Formal Security Protocol Analysis ♦ Symmetric Encryption Scheme ♦ Present Polynomial-time Algorithm ♦ Subterm Convergent Equational Theory ♦ Key Word ♦ Subterm Convergent Theory ♦ Symmetric Encryption ♦ Security Protocol ♦ Asymptotic Complexity ♦ Kerberos Protocol ♦ Prefix Theory ♦ Standard Notion
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.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study