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

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/inria-00480632
Contributor : Tigran Avanesov <>
Submitted on : Friday, May 21, 2010 - 2:51:38 PM
Last modification on : Thursday, June 27, 2019 - 4:27:48 PM
Long-term archiving on : Wednesday, November 30, 2016 - 10:44:30 PM

File

RR-7276.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00480632, version 3

Citation

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

Share

Metrics

Record views

620

Files downloads

955