Thèse en informatique

 

Ma thèse porte essentiellement sur la mise en place d'une méthode basée sur la cryptanalyse logique pour affaiblir les fonctions cryptographiques. Ces travaux sont donc transversaux à deux domaines : la SATisfaisabilité et la Cryptographie.

 

Les premiers résultats obtenus touchent au domaine des fonctions de hachage cryptographiques les plus utilisées en pratique, à savoir MD5 et SHA-1.

Soutenue à Reims le 30 juin 2014 devant le jury composé de :

  • Bertrand Mazure, Professeur à l'Université d'Artois (Président et Rapporteur)
  • Serge Vaudenay, Professeur à l'École Polytechnique Fédérale de Lausanne (Rapporteur)
  • Michaël Krajecki, Professeur à l'Université de Reims Champagne-Ardenne (Directeur)
  • Gilles Dequen, Professeur à l'Université de Picardie Jules Verne (Directeur)
  • Stéphane Manuel, Enseignant-Chercheur à l'École Polytechnique Féminine (Examinateur)
  • Valérie Rouat, Chercheur à DGA Maîtrise de l'Information (Examinateur)
  • Daniel Singer, Maître de Conférence à l'Université de Lorraine (Examinateur)

Keywords: Logical cryptanalysis, satisfiability, cryptographic hash function, MD5, SHA-1, SHA-3

Abstract: Democratization of increasingly high-performance digital technologies and especially the Internet has considerably changed the world of communication. Consequently, needs in cryptography are more and more numerous and the necessity of verifying the security of cipher algorithms is essential. This thesis deals with a new cryptanalysis, called logical cryptanalysis, which is based on the use of logical formalism to express and solve cryptographic problems. More precisely, works presented here focuses on a particular category of ciphers, called cryptographic hash functions, used in authentication and data integrity protocols. The first contribution is the modeling of a cryptographic problem as a SAT problem. For this, we present some rules that lead to describe easily basic operations involved in cipher algorithms. Then, a section is dedicated to logical reasoning in order to simplify the produced SAT formulas and show how satisfiability can help to enrich a knowledge on a studied problem. Furthermore, we also present many points of view to use our smooth modeling to apply a probabilistic reasoning on all the data associated with the generated SAT formulas. This has then allowed to improve both the modeling and the solving of the problem and underlined a weakness about the use of round constants. Second, a section is devoted to practical attacks. Within this framework, we tackled preimages and the collision problem of the most popular cryptographic hash functions.

Lien vers le document de thèse : Télécharger la thèse au format PDF

Communications internationales :

F. Legendre, G. Dequen, et M. Krajecki. Collisionner md5 : Modélisation logique et résolution parallèle. RenPAR’20 : Rencontres francophones du Parallélisme, Atelier NP-Par, St-Malo, 2011.

F. Legendre, G. Dequen, and M. Krajecki. Inverting thanks to SAT Solving: An application on Reduced-Step MD*. In SECRYPT 2012 : International Conference on Security and Cryptography, Roma (Italy), July 24-27 2012.

F. Legendre, G. Dequen, and M. Krajecki. Encoding hash functions as a SAT problem. In ICTAI 2012 : 24th IEEE International Conference on Tools with Artificial Intelligence, Athens (Greece), November 7-9 2012.

F. Legendre, G. Dequen, and M. Krajecki. From a Logical Approach to Internal States of Hash Functions - How SAT Problem Can Help to Understand SHA-⋆ and MD* . In SECRYPT 2013 : International Conference on Security and Cryptography, Reykjavik (Iceland), July 27-31 2013.

F. Legendre, G. Dequen, and M. Krajecki. Logical Reasoning to Detect Weaknesses About SHA-1 and MD4/5. In Cryptology ePrint Archive: Report 2014/239, Version 20140415:065209.

 

Présentations orales nationales :

Inversion des fonctions de hachage, Journées Jeunes Chercheurs du MIS 2012, Amiens, juin 2012.

Cryptanalyse logique des fonctions de hachage, Journée RGE : cyber-sécurité, Troyes, octobre 2012.

Outil visuel pour la résolution d'instances SAT - Application à la cryptanalyse, Journée STIC du PRES UFECAP, Laon, décembre 2012

La SATisfaisabilité pour aider la cryptanalyse : Approche logique et approche probabiliste, Journées Jeunes Chercheurs du MIS 2013, Amiens, juin 2013.

Cryptanalyse logique des fonctions de hachage, Journée RGE : Colmar, juin 2014

Application du problème SAT aux fonctions de hachages cryptographique, Séminaire au CRIL, Lens, novembre 2014.

 

Posters colloques nationaux :

Comment collisionner MD5 ?, Journées Jeunes Chercheurs du MIS 2011, Amiens, mai 2011.

Exploitation de la logique propositionnelle pour la résolution de problèmes cryptographiques, Doctoriales DGA, St Raphaël, septembre 2011.

Exploitation de la puissance du calcul parallèle pour la résolution de problèmes cryptographiques, Journée ROMEO'2012, Reims, juin 2012.

Zircon - This is a contributing Drupal Theme
Design by WeebPal.