Finding a preimage for a SHA-1 hash is, at present, a computationally intractable problem. SAT-solvers have been useful tools for handling such problems and can often, through heuristics, generate acceptable solutions. This research examines the intersection between the SHA-1 preimage problem, the encoding of that problem for SAT-solving, and SAT-solving. The results demonstrate that SAT-solving is not yet a viable approach to take to solve the preimage problem, and also indicate that some of the intuitions about “good” problem encodings in the literature are likely to be incorrect.
Reference:
Motara, Y.M. and Irwin, B.V.W. 2017. SHA-1, SAT-solving, and CNF. Southern Africa Telecommunication Networks and Applications Conference (SATNAC) 2017, 3 - 10 September 2017, Freedom of the Seas, Royal Caribbean International, Barcelona, Spain
Motara, Y., & Irwin, B. V. (2017). SHA-1, SAT-solving, and CNF. http://hdl.handle.net/10204/9692
Motara, YM, and Barry VW Irwin. "SHA-1, SAT-solving, and CNF." (2017): http://hdl.handle.net/10204/9692
Motara Y, Irwin BV, SHA-1, SAT-solving, and CNF; 2017. http://hdl.handle.net/10204/9692 .
Paper presented at Southern Africa Telecommunication Networks and Applications Conference (SATNAC) 2017, 3 - 10 September 2017, Freedom of the Seas, Royal Caribbean International, Barcelona, Spain
