Florian Legendre (CRIL, Université d’Artois)

La sécurité des systèmes d’information est devenu un besoin primordial dans le monde numérique qui nous entoure. Cette sécurité est garantie principalement par l’utilisation de protocoles et d’algorithmes cryptographiques qui doivent être résistants contre tous types d’attaques. L’analyse de ces algorithmes - qu’on appelle cryptanalyse - a vu naître ces dernières années une nouvelle branche, nommée cryptanalyse logique, qui consiste à étudier un algorithme de chiffrement via l’utilisation de la logique propositionnelle et plus particulièrement du problème SAT. Dans ce cadre, l’étude est réalisée en deux temps : l’algorithme et l’attaque souhaitée sont d’abord modélisés en un problème SAT, puis un solveur est appliqué sur la formule générée de sorte que tous modèles trouvés concrétisent l’attaque. Cet exposé s’intéresse à la cryptanalyse logique d’une certaine catégorie d’algorithmes utilisés dans les protocoles d’authentification et d’intégrité de données qu’on appelle fonctions de hachage cryptographiques. Dans cette présentation, nous aborderons la modélisation d’un problème cryptographique en un problème SAT et discuterons de la complexité des formules générées. Puis, nous verrons comment la satisfaisabilité peut tenter d’aider la cryptanalyse à travers l’application de raisonnements logiques et probabilistes sur les formules. Enfin, nous évoquerons les limites de telles attaques en pratique.