Satisfiability of Dolev-Yao Constraints

The secrecy problem, under certain hypothesis, is equivalent to satisfiability of constraints involving Dolev-Yao's operator ⊢. Making some restrictions over these constraints, their satisfiability has been proven to be NP-complete. However, to check opacity [L. Mazaré. Using unification for opacity properties. In Proc. of the Workshop on Issues in the Theory of Security (WITS'04). To appear, 2004] or some modified versions of secrecy, there is a need to find similar results for a larger class of predicates. This paper starts to extend this decidability result to more general constraints allowing in particular inequalities and gives a simple decision procedure based on a rewriting system.