Sciweavers

LICS
2003
IEEE

Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or

13 years 9 months ago
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 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 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 fo...
Hubert Comon-Lundh, Vitaly Shmatikov
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where LICS
Authors Hubert Comon-Lundh, Vitaly Shmatikov
Comments (0)