A Simple Constraint-solving Decision Procedure for Protocols with Exclusive or

Yannick Chevalier (1)

1 CASSIS - Combination of approaches to the security of infinite states systems

We present a procedure for deciding security of protocols employing the Exclusive or operator. This procedure relies on a direct combination of a constraint solver for security protocol with a unification algorithm for the exclusive-or theory. Hence compared to the previous ones it is much simpler and easily amenable to automation. The principle of the approach can be applied to other theories too.

Mots clés: security protocols; decision procedure; unification; rewriting; exclusive-or

Domaines: Autre [cs.OH]

Yannick Chevalier. A Simple Constraint-solving Decision Procedure for Protocols with Exclusive or. [Research Report] RR-5224, INRIA. 2004, pp.35. ⟨inria-00070771⟩