Satisfiability of Dolev-Yao Constraints

The secrecy problem, under certain hypothesis, is equivalent to satisfiability of constraints involving Dolev-Yao's operator vertical bar. Making some restrictions over these constraints, their satisfiability has been proven to be NP-complete. However, to check opacity [11] 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.