Intruder deductions, constraint solving and insecurity decision in presence of exclusive or

We present decidability results for the verification of cryptographic protocols in the presence of equational theories corresponding to xor and Abelian groups. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties such as xor, we exte...

Full description

Saved in:
Bibliographic Details
Main Authors: Comon-Lundh, H., Shmatikov, V.
Format: Conference Proceeding
Language:English
Subjects:
Algebra
Authentication
Computer science
Constraint theory
Context modeling
Cryptographic protocols
Cryptography
Equations
Logic
Polynomials
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present decidability results for the verification of cryptographic protocols in the presence of equational theories corresponding to xor and Abelian groups. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties such as xor, we extend the conventional Dolev-Yao model by permitting the intruder to exploit these properties. We show that the ground reachability problem in NP for the extended intruder theories in the cases of xor and Abelian groups. This result follows from a normal proof theorem. Then, we show how to lift this result in the xor case: we consider a symbolic constraint system expressing the reachability (e.g., secrecy) problem for a finite number of sessions. We prove that such a constraint system is decidable, relying in particular on an extension of combination algorithms for unification procedures. As a corollary, this enables automatic symbolic verification of cryptographic protocols employing xor for a fixed number of sessions.
ISSN:1043-6871
2575-5528
DOI:10.1109/LICS.2003.1210067