Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SHA-256 Collision Attack with Programmatic SAT

Nahiyan Alamgir, Saeed Nejati, Curtis Bright

TL;DR

This paper addresses the SHA-256 collision problem by exploring step-reduced collisions using a hybrid SAT+CAS solver. It encodes the collision search as a SAT problem and enhances the solver with programmatic inconsistency blocking and propagation guided by a computer algebra system, through the IPASIR-UP interface. The authors demonstrate 38-step semi-free-start collisions, surpassing plain SAT which stalls at 28 steps, and show that SAT+CAS can approach the performance of specialized search tools for this regime. The work highlights the effectiveness of integrating CAS techniques with SAT solving for cryptanalytic tasks and discusses implications for the security assessment of SHA-256 and future research directions toward even longer-step collisions.

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äffer. 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.

SHA-256 Collision Attack with Programmatic SAT

TL;DR

This paper addresses the SHA-256 collision problem by exploring step-reduced collisions using a hybrid SAT+CAS solver. It encodes the collision search as a SAT problem and enhances the solver with programmatic inconsistency blocking and propagation guided by a computer algebra system, through the IPASIR-UP interface. The authors demonstrate 38-step semi-free-start collisions, surpassing plain SAT which stalls at 28 steps, and show that SAT+CAS can approach the performance of specialized search tools for this regime. The work highlights the effectiveness of integrating CAS techniques with SAT solving for cryptanalytic tasks and discusses implications for the security assessment of SHA-256 and future research directions toward even longer-step collisions.

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äffer. 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.
Paper Structure (22 sections, 9 equations, 3 figures, 9 tables)

This paper contains 22 sections, 9 equations, 3 figures, 9 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Cryptographic Hash Functions
  4. SHA-256
  5. Message Expansion
  6. State Update Transformation
  7. Differential Cryptanalysis
  8. Boolean Satisfiability (SAT)
  9. The $\mathbf{\text{SC}^2}$ Project.
  10. Programmatic SAT.
  11. Previous Work
  12. The SAT Encoding
  13. Programmatic Inconsistency Blocking
  14. Programmatic Propagation
  15. Bitsliced Propagation
  16. ...and 7 more sections

Figures (3)

  • Figure 1: SHA-256 processes the input (with padding if needed) into message blocks (abbreviated as "MB"), which are sequentially fed to the compression function, $f$. The output of each compression is used as the chaining value in the next compression. The compression of the last message block produces the final hash. The initial chaining value ( IV) is fixed by the specification of SHA-256. The entire method is known as the Merkle--Damgård construction, which is popular for building collision-resistant hash functions.
  • Figure 2: A diagram depicting the simplified version of SHA-256 we consider in our work. $f_n$ is the step-reduced compression function having $n$ steps. The chaining value, CV, is arbitrary for semi-free-start (SFS) collisions and is not required to match the IV actually used in SHA-256---though a SFS colliding message pair is required to have matching CVs.
  • Figure 3: Running times for finding a SFS collision for step-reduced SHA-256 for a varying number of steps. The plot compares a plain SAT solver with two programmatic SAT solvers. The lack of a data point indicates no collisions were found within 500,000 seconds.