Satisfiability of General Intruder Constraints with and without a Set Constructor

Tigran Avanesov 1 Yannick Chevalier 2 Michaël Rusinowitch 3 Mathieu Turuani 3
1 SnT - Interdisciplinary Centre for Security, Reliability and Trust [Luxembourg]
2 IRIT - Institut de recherche en informatique de Toulouse
3 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Many decision problems on security protocols can be reduced to solving deduction constraints expressing whether an instance of a given message pattern can be constructed by the intruder. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity} and variable-origination}. In this work we relax these restrictions by giving a decision procedure for solving general intruder constraints (that do not have these properties) that stays in NP. The result is also valid modulo an associative, commutative and idempotent theory. The procedure can be applied to verify security protocols in presence of multiple intruders.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2017, 80, pp. 27-61. 〈10.1016/j.jsc.2016.07.009〉
Liste complète des métadonnées

Littérature citée [45 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01405842
Contributeur : Michaël Rusinowitch <>
Soumis le : jeudi 1 décembre 2016 - 09:44:34
Dernière modification le : mardi 18 décembre 2018 - 16:38:25
Document(s) archivé(s) le : lundi 20 mars 2017 - 22:33:31

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

UNIV-TLSE3 | INRIA | SMS | UNIV-TLSE2 | LORIA | LORIA-FM | UNIV-LORRAINE | INRIA2017

Citation

Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani. Satisfiability of General Intruder Constraints with and without a Set Constructor. Journal of Symbolic Computation, Elsevier, 2017, 80, pp. 27-61. 〈10.1016/j.jsc.2016.07.009〉. 〈hal-01405842〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

583

Téléchargements de fichiers

85

Contact


archive-ouverte@inria.fr