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

Colloque avec actes et comité de lecture. internationale.International audienceWe 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