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; procédure de décision; réécriture; ou-exclusif; exclusive-or; protocoles de sécurité

Domaines: Autre [cs.OH]

Yannick Chevalier. A Simple Constraint-solving Decision Procedure for Protocols with Exclusive or. 18th International Workshop on Unification - UNIF'2004, Jul 2004, Cork, Ireland, 15 p. ⟨inria-00099889⟩