inria-00480632, version 3
Satisfiability of General Intruder Constraints with and without a Set Constructor
N° RR-7276 (2010)
Résumé : 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.
- a – INRIA
- 1 :
- INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- 2 :
- CNRS : UMR5505 – Institut National Polytechnique de Toulouse - INPT – Université des Sciences Sociales - Toulouse I – Université Toulouse I [UT1] Capitole – Université Toulouse le Mirail - Toulouse II – Université Paul Sabatier [UPS] - Toulouse III
- Collaboration : IRIT
- Domaine : Informatique/Calcul formel
Informatique/Cryptographie et sécurité - Mots-clés : Security – Constraint solving – Dolev-Yao intruder – equational theory – ACI
- Référence interne : RR-7276
- Versions disponibles : v1 (04-05-2010) v2 (11-05-2010) v3 (21-05-2010)
- inria-00480632, version 3
- http://hal.inria.fr/inria-00480632
- oai:hal.inria.fr:inria-00480632
- Contributeur :
- Soumis le : Vendredi 21 Mai 2010, 14:51:38
- Dernière modification le : Vendredi 21 Mai 2010, 17:16:48
Documents associés
Exporter