Verimag

Technical Reports

Laurent Mazare
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.

Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 875095