SHA-256 Collision Attack with Programmatic SAT

TL;DR

This paper introduces a hybrid SAT + CAS approach to find collisions in step-reduced SHA-256, significantly extending the number of steps for which collisions can be discovered compared to previous methods.

Contribution

The paper presents a novel hybrid SAT + CAS method that outperforms pure SAT approaches in finding SHA-256 collisions in more steps, demonstrating improved efficiency and capability.

Findings

Successfully found a 38-step collision in SHA-256 with modified IV

Hybrid SAT + CAS approach outperforms pure SAT in collision search

Pure SAT approach limited to 28 steps for collision detection

Abstract

Cryptographic hash functions play a crucial role in ensuring data security, generating fixed-length hashes from variable-length inputs. The hash function SHA-256 is trusted for data security due to its resilience after over twenty years of intense scrutiny. One of its critical properties is collision resistance, meaning that it is infeasible to find two different inputs with the same hash. Currently, the best SHA-256 collision attacks use differential cryptanalysis to find collisions in simplified versions of SHA-256 that are reduced to have fewer steps, making it feasible to find collisions. In this paper, we use a satisfiability (SAT) solver as a tool to search for step-reduced SHA-256 collisions, and dynamically guide the solver with the aid of a computer algebra system (CAS) used to detect inconsistencies and deduce information that the solver would otherwise not detect on its own. Our hybrid SAT + CAS solver significantly outperformed a pure SAT approach, enabling us to find collisions in step-reduced SHA-256 with significantly more steps. Using SAT + CAS, we find a 38-step collision of SHA-256 with a modified initialization vector -- something first found by a highly sophisticated search tool of Mendel, Nad, and Schl\"affer. Conversely, a pure SAT approach could find collisions for no more than 28 steps. However, our work only uses the SAT solver CaDiCaL and its programmatic interface IPASIR-UP.