Pre-image attack of the MD5 hash function by proportional logic

Hash functions are important cryptographic primitives that map arbitrary length messages to fixed length message summaries such that: it is easy to compute the digest given a message, while invert the hash process (for example, finding a message that maps a summary of a specific message) is difficult. An attack against a hash function is an algorithm that nevertheless manages to invert the hash process. Hash functions are used in authentication, digital signature, and key exchange systems. The most widely used hash function in many applications is the Message Digest-5 (MD5) algorithm. In this paper we study the current state of the technique of realization of the preimage attack of MD5 using solver SAT, we try improvements in the process of encoding and resolution. An important part of our work is to use the methods of propositional logic to model the attack problem and to determine which heuristic leads to the best resolution. Our most important result is a new encoding of the addition to several operands which considerably reduce the time required for the SAT solvers to find a solution to coding’s previously known.