Laurent Mazare
Satisfiability of Dolev-Yao Constraints (2004)
Satisfiability of Dolev-Yao Constraints (2004)
TR-2004-22.ps
Keywords: Security, Formal Verification, Dolev-Yao Constraints, Rewriting Systems, Opacity.
Abstract: The secrecy problem, under certain hypothesis, is equivalent to satisfiability of constraints involving Dolev-Yao's operator $vdash$. Making some restrictions over these constraints, their satisfiability has been proven to be NP-complete. However, to check opacity~cite{mazare04} 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.
