Satisfiability of General Intruder Constraints with and without a Set Constructor - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Symbolic Computation Année : 2017

Satisfiability of General Intruder Constraints with and without a Set Constructor

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (793.9 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01405842 , version 1 (01-12-2016)

Identifiants

Citer

Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani. Satisfiability of General Intruder Constraints with and without a Set Constructor. Journal of Symbolic Computation, 2017, Special issue: SI: Program Verification, 80, pp.27-61. ⟨10.1016/j.jsc.2016.07.009⟩. ⟨hal-01405842⟩
359 Consultations
134 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More