Logic in Computer Science (LICS 2003)

Paper: Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or (at LICS 2003)

Authors: H. Comon-Lundh V. Shmatikov

Abstract

We present decidability results for the verification of cryptographic protocols in the presence of equational theories corresponding to xorand 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 xorcase: 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 xorfor a fixed number of sessions.

BibTeX

  @InProceedings{ComonLundhShmatikov-IntruderDeductionsC,
    author = 	 {H. Comon-Lundh and V. Shmatikov},
    title = 	 {Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2003},
    year =	 2003,
    editor =	 {Phokion G. Kolaitis},
    month =	 {June}, 
    pages =      {271--},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }