Cryptanalyse algébrique en caractéristique 2: Gröbner versus SAT

En cryptanalyse algébrique, la résolution des systèmes polynomiaux définis sur un corps fini se fait en utilisant un algorithme de calcul de bases de Gröbner comme F4 ou F5. Cependant, lorsqu’on cherche des solutions dans F_2, l’expérimentation montre que la recherche exhaustive, ou encore les méthodes hybrides combinant la recherche exhaustive et les bases de Gröbner donnent des meilleurs résultats. Dans cet exposé, je montrerai une autre approche, dite logique, qui repose sur la résolution d’une formule booléenne par un solveur SAT. J’expliquerai le fonctionnement des moteurs de résolution SAT et en particulier d’un solveur dédié à la résolution de systèmes polynomiaux que nous avons proposé. Je démontrerai une similarité entre les deux approches, algébrique et logique, qui peut être exploitée davantage pour améliorer la résolution. Cet exposé repose sur des travaux joints avec Gilles Dequen et Monika Trimoska.