Vérification des protocoles cryptographiques avec le langage PDDL et les solveurs SAT

Résumé : Dans ce papier, nous introduisons une approche basée sur la planification pour détecter des attaques logiques sur les protocoles cryptographiques. Nous montrons que les protocoles cryptographiques peuvent être modélisés avec le langage de planification PDDL, et vérifiés avec un système de planification tel que Blackbox. Notre approche est principalement inspirée des travaux de Compagna sur la planification via SAT des protocoles cryptographiques. Pour vérifier un protocole, Compagna se sert de l'environnement Avispa et ses différents outils de traduction, et finalement des solveurs SAT. Nous proposons une approche plus directe : modélisation en PDDL et vérification avec un planificateur SAT tel que Blackbox. L'idée principale de notre approche est une formulation PDDL compacte et simple des termes à structures complexes, sans employer des techniques de concrétisation proposées par Compagna. En particulier, nous avons réussi à détecter l'attaque par confusion de type, qui ne peut pas être trouvée avec l'approche de Compagna. Ce travail contribue à la modélisation directe en langage de planification PDDL et la résolution avec des solveurs SAT.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008 - Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.21-30, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00290703
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : jeudi 26 juin 2008 - 11:21:15
Dernière modification le : mercredi 31 janvier 2018 - 10:24:04
Document(s) archivé(s) le : vendredi 28 mai 2010 - 20:58:18

Fichier

pages-021-30-article40.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00290703, version 1

Collections

Citation

Noureddine Aribi, Yahia Lebbah. Vérification des protocoles cryptographiques avec le langage PDDL et les solveurs SAT. Gilles Trombettoni. JFPC 2008 - Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.21-30, 2008. 〈inria-00290703〉

Partager

Métriques

Consultations de la notice

188

Téléchargements de fichiers

281