La cryptographie à clé secrète ou cryptographie symétrique est une des deux formes de cryptographie les plus employées dans les transactions informatiques. Les primitives de la cryptographie symétrique sont les chiffrements à flot, les chiffrements par bloc qui garantissent la confidentialité des échanges et les fonctions de hachage pour l’intégrité. Depuis quelques années, de nombreux résultats proposent des outils automatiques permettant d’attaquer ces primitives. Ils sont essentiellement basés sur des solveurs SAT ou de la programmation linéaire en nombres entiers (ILP). Cependant transformer un problème de cryptanalyse en instance SAT ou ILP qui soit efficacement résolvable par les solveurs existants nécessite généralement un important travail de modélisation. Le but de ce projet est de proposer un langage déclaratif dédié aux problèmes de cryptanalyse en cryptographie symétrique. Ce langage sera basé sur la programmation par contraintes (CP) et permettra d’améliorer les attaques existantes et de construire de nouveaux algorithmes qui résistent à ces attaques. Cet objectif très général est décomposé en quatre sous-objectifs : - étudier et comparer les performances des approches déclaratives existantes (SAT, ILP et CP) pour modéliser et résoudre des problèmes de cryptanalyse symétrique ; - améliorer le passage à l’échelle des solveurs CP pour résoudre des problèmes de cryptanalyse symétrique, en les combinant avec d’autres approches et en définissant de nouvelles contraintes globales dédiées à ces problèmes ; - concevoir de nouvelles procédures d’explication afin d’une part d’améliorer les performances des solveurs CP en leur permettant d’exploiter leurs échecs, et d’autre part de générer des preuves de correction intelligibles pour un être humain ; - améliorer les attaques existantes et construire de nouveaux algorithmes qui résistent à ces attaques en utilisant les solveurs CP.