Constraint solving, exclusive or and the decision of confide ntiality for security protocols assuming a bounded number of sessions

We present decidability results for the verification of cryptographic protocols in the presence of equational the- ories corresponding toxor and Abelian groups. Since the perfect cryptography assumption is unrealistic for crypto - graphic primitives with visible algebraic properties suchas xor, we extend the conventional Dolev-Yao model by per- mitting the intruder to exploit these properties. We show that the reachability problem is NP-complete for the ex- tended intruder theories in the cases ofxor and Abelian groups. This result follows from a normal proof theorem. Then, we show how to lift this result in thexor case: we consider a symbolic constraint system expressing the reach - ability (e.g., secrecy) problem for a finite number of ses- sions. We prove that such constraint system is decidable, relying in particular on an extension of combination algo- rithms for unification procedures. As a corollary, this en- ables automatic symbolic verification of cryptographic pro - tocols employingxor for a fixed number of sessions.