Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Satisfiability of General Intruder Constraints with and without a Set Constructor

Tigran Avanesov 1 Yannick Chevalier 2, 3 Michael Rusinowitch 1 Mathieu Turuani 1 
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 IRIT-LILaC - Logique, Interaction, Langue et Calcul
IRIT - Institut de recherche en informatique de Toulouse
Abstract : Many decision problem on security protocols can be reduced to solving so-called intruder constraints in the Dolev Yao model. Most constraint solving procedures for cryptographic protocol security rely on two properties of constraint systems called knowledge monotonicity and variable-origination. In this work we relax these restrictions by giving an NP decision procedure for solving general intruder constraints (that do not have these properties). Our result extends a first work by L. Mazaré in several directions: we allow non-atomic keys, and an associative, commutative and idempotent symbol (for modelling sets). We also discuss several new applications of our result.
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Tigran Avanesov Connect in order to contact the contributor
Submitted on : Friday, May 21, 2010 - 2:51:38 PM
Last modification on : Wednesday, October 26, 2022 - 8:15:30 AM
Long-term archiving on: : Wednesday, November 30, 2016 - 10:44:30 PM


Files produced by the author(s)


  • HAL Id : inria-00480632, version 3


Tigran Avanesov, Yannick Chevalier, Michael Rusinowitch, Mathieu Turuani. Satisfiability of General Intruder Constraints with and without a Set Constructor. [Research Report] RR-7276, INRIA : Institut national de recherche en sciences et technologies du numérique. 2010, 48p. ⟨inria-00480632v3⟩



Record views


Files downloads