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 1MB |
Official URL: https://doi.org/10.1016/j.jsc.2016.07.009
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.
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: | |
Statistics: | download |
Deposited On: | 18 Apr 2019 12:20 |
Repository Staff Only: item control page