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

National audienceDans 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