New Records of Pre-image Search of Reduced SHA-1 Using SAT Solvers

Although the first SHA-1 collision attack has been carried out in 2017, the cryptographic hash function seems still robust against pre-image attacks. The aim of this work is to measure how many rounds of SHA-1 can be inverted in practice using SAT solvers. To do so, we have first modeled the problem of finding a pre-image of SHA-1 as a system of Boolean formulas, explicitly describing the procedure to obtain such model. Then, we configured the model based on different combinations of number of rounds and number of free bits in our target pre-image. Finally, to find a solution of the model, we used a SAT solver on our server, testing several combinations of restart policies and polarity modes. We analyze and report the number and positions of the pre-image bits that can be fixed to influence the ability of the SAT solver to find the remaining free bits of the pre-image in a shorter time. In particular, we execute partial pre-image attacks on 64-, 80- 96-, 112- and 128-bit messages, outperforming the current state-of-the-art records.