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 | Site Map | Site powered by SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4196917