Encoding Hash Functions as a SAT Problem. - Florian Legendre; Gilles Dequen; Michaël Krajecki (ICTAI, 2012)

Inverting Thanks to SAT Solving - An Application on Reduced-step MD*. - Florian Legendre; Gilles Dequen; Michaël Krajecki (SECRYPT, 2012)

From a Logical Approach to Internal States of Hash Functions - How SAT Problem Can Help to Understand SHA-* and MD*. - Florian Legendre; Gilles Dequen; Michaël Krajecki (SECRYPT, 2013)

Logical Reasoning to Detect Weaknesses About SHA-1 and MD4/5. - Florian Legendre; Gilles Dequen; Michaël Krajecki (IACR Cryptol. ePrint Arch., 2014)