Skip to Main content Skip to Navigation

Satisfiability of General Intruder Constraints with and without a Set Constructor

Tigran Avanesov 1 Yannick Chevalier 2 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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 metadatas
Contributor : Tigran Avanesov <>
Submitted on : Tuesday, May 11, 2010 - 10:18:32 AM
Last modification on : Friday, January 10, 2020 - 9:09:11 PM
Document(s) archivé(s) le : Friday, October 19, 2012 - 2:17:29 PM


Files produced by the author(s)


  • HAL Id : inria-00480632, version 1



Tigran Avanesov, Yannick Chevalier, Michael Rusinowitch, Mathieu Turuani. Satisfiability of General Intruder Constraints with and without a Set Constructor. [Research Report] RR-7276, 2010, pp.48. ⟨inria-00480632v1⟩



Record views


Files downloads