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, 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.
Type de document :
Rapport
[Research Report] RR-7276, INRIA. 2010, pp.50
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00480632
Contributeur : Tigran Avanesov <>
Soumis le : vendredi 21 mai 2010 - 14:51:38
Dernière modification le : jeudi 11 janvier 2018 - 06:21:34
Document(s) archivé(s) le : mercredi 30 novembre 2016 - 22:44:30

Fichier

RR-7276.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

475

Téléchargements de fichiers

363