Efficient decision procedures for message deducibility and static equivalence
Basin, David A.
Rights / licenseIn Copyright - Non-Commercial Use Permitted
We consider two standard notions in formal security protocol analysis: message deducibility and static equivalence under equational theories. We present new polynomial-time algorithms for deciding both notions under subterm convergent equational theories and under a theory representing symmetric encryption with the prex 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 prex theory). However, our algorithms have a signicantly better asymptotic complexity than existing approaches. 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 prex property holds Show more
External linksFull text via SFX
Journal / seriesTechnical report
PublisherETH, Department of Computer Science
SubjectEquational theories; Security protocols; Deducibility; Static equivalence
Organisational unit02150 - Departement Informatik / Department of Computer Science
NotesTechnical Reports D-INFK.
MoreShow all metadata