From a logical approach to internal states of Hash functions how SAT problem can help to understand SHA-⋆ and MD⋆

This paper deals with logical cryptanalysis of hash functions. They are commonly used to check data integrity and to authenticate protocols. These functions compute, from an any-length message, a fixed-length bit string, usually named digest. This work defines an experimental framework, that allows, thanks to the propositional formalism, to study cryptosystems at the bit level through corresponding instances of the SAT problem. Thus, we show that some internal words of popular hashing functions MD⋆ and SHA-⋆ are not as random as expected and provide some convincing elements to explain this phenomenon by the use of round constants. Because this presents several weaknesses, we show how to detect and exploit these ones through an application based on logical cryptanalysis. As a result we show equivalences, and quasi-equivalences between digits and explain how we inverse reduced-step versions of MD5 and SHA-1.