OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Satisfiability of general intruder constraints with and without a set constructor

Avanesov, Tigran and Chevalier, Yannick and Rusinowitch, Michaël and Turuani, Mathieu Satisfiability of general intruder constraints with and without a set constructor. (2017) Journal of Symbolic Computation, 80 (1). 27-61. ISSN 0747-7171

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1016/j.jsc.2016.07.009


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.

Item Type:Article
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Institut National de la Recherche en Informatique et en Automatique - INRIA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > University of Luxembourg (LUXEMBOURG)
Laboratory name:
Deposited On:18 Apr 2019 12:20

Repository Staff Only: item control page