IACR News item: 29 September 2014
PhD Database
Name: Florian Legendre
Topic: Exploitation de la logique propositionnelle pour la résolution de problèmes cryptograhiques
Category: secret-key cryptography
Description: 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[...]
Topic: Exploitation de la logique propositionnelle pour la résolution de problèmes cryptograhiques
Category: secret-key cryptography
Description: 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[...]
Additional news items may be found on the IACR news page.