Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

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

Authors: Hubert Comon-Lundh Vitaly 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 = 	 {Hubert Comon-Lundh and Vitaly Shmatikov},
    title = 	 {Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {271--280},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski