Encoding Hash Functions as a SAT Problem

The SATisfiability Problem is a core problem in mathematical logic and computing theory. In the last years, progresses have led it to be a great and competitive approach to practically solve a wide range of industrial and academic problems. Thus, the current SAT solving capacity allows the propositional formalism to be an interesting alternative to tackle cryptographic problems, and particularly introduced a new field called logical cryptanalysis [15]. This paper deals with an original application of the SAT problem to encode the well-known MD? and SHA? hash functions algorithm in a generic DIMACS formula. As cryptographic hash functions are central elements in modern cryptography we choose to validate our modelisation with a dedicated attack on the inversion of these functions. This attack behaves like a reverse-engineering process, thanks to a state of the art SAT solver achieving a weakening of the second preimage of MD? and SHA?. As a result, we present our modelisation and an improvement of the current limit of best practical attacks on step-reduced MD4, MD5 and SHA? inversions, respectively up to 39, 28 and 23 broken steps. Finally, a brief analyse of our results allows to give an idea about logical cryptanalysis and hash functions.