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 diferent inputs with the same hash. Currently, the best SHA-256 collision attacks use diferential 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äfer. 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.
only broken in the last few months with the announcement of a 31-step SHA-256 collision [
Traditionally, the best collisions for step-reduced SHA-256 were found using highly sophisticated
tools specifically designed to search for such collisions. Conversely, another line of research examined
using satisfiability (SAT) solvers to search for collisions in step-reduced SHA-256, but the results of SAT
solvers were not at all competitive with the best custom-written search tools. For example, in 2016,
Prokop [
In our work, we develop a hybrid approach of using a programmatic SAT solver that uses a computer
algebra system (CAS) to provide the SAT solver information it wouldn’t be able to detect on its own—an
approach that has been successful on many other problems recently [
In particular, we are able to detect and block inconsistencies in the solver’s state using programmatic
inconsistency blocking (see Section 4) and are able to deduce nontrivial information about the solver’s
state using programmatic propagation (see Section 5). Our “SAT + CAS” solver was able to find several
new 38-step SFS SHA-256 collisions, matching the same step count of the SFS collisions found by Mendel
et al. [
We note that our SAT-based tool is significantly slower than the dedicated search tool of Mendel
et al. [
In this section we provide background on cryptographic hash functions, especially SHA-256, and then discuss diferential cryptanalysis and the notation we use in our work (see Section 2.3). We also briefly discuss SAT solving and summarize previous collision attacks on SHA-256.
Cryptographic hash functions take an arbitrary-length input and produce a short fixed-length output that acts as a signature or fingerprint of the input. The fingerprint is called a hash value and the input is known as a message. Hash functions are extensively used for data integrity and security. They are particularly helpful in cases where storing the message would pose a security threat but a signature is still required for verification, such as a password in a database. The hashes of the passwords can be stored instead and each time the user enters their password, the hashes can be matched for verification.
Hashes can be used for data integrity as well. For example, when some data is stored or transferred, the integrity can be checked by comparing a known hash with the hash of the stored data. This integrity check ensures that the data was preserved without alteration.
Cryptographic hash functions are expected to have three primary characteristics: • Preimage resistance: It’s computationally infeasible to find an input, x, given a hash, y, such that y is the hash of x. • 2nd preimage resistance: Given an input, x, and its hash, y, it’s infeasible to find a diferent input, x′, that produces the same hash y.
IV
Hash
• Collision resistance: It’s infeasible to find an input pair, x and x′ (x ̸= x′), that both produce the same hash.
An example of a weak hash function is MD4 [
In the compression function, 64 rounds (also called steps) of transformations are performed to produce a hash. The hash from processing a single message block is used as the chaining value for the next message block. This means that altering a message block will lead to cascading changes in the next message blocks in the sequence. The chaining value for the first message block is set by the specification [ 14] to a fixed value, known as the standard IV (initialization vector). The hash output is the chaining value produced after applying the compression function on the last message block.
In our work, we focus on a step-reduced version of SHA-256. This means that the number of rounds/steps in the compression function is reduced to make the problem easier. Moreover, we only consider messages with a single block of size 512 bits. Because the hash output has 256 bits, there is certainly enough freedom in the input so that many collisions exist without needing to consider multiple blocks.
A relaxed type of collision known as a semi-free-start (SFS) collision allows an arbitrary initial chaining value CV, so long as the same chaining value is used to initialize the hash function for both colliding messages in the SFS collision (see Figure 2). In our work, we find SFS collisions for SHA-256 using up to 38 steps of the compression function. Note that the actual SHA-256 hash function has 64 steps, meaning we are still very far from finding a true SHA-256 collision (roughly speaking, as the number of steps increases the collision problem becomes exponentially more dificult). The best known collision attacks on SHA-256 are very far from the full 64 steps, so this provides evidence that SHA-256 is secure.
SHA-256 performs operations on 32-bit words only. The input message block consists of 16 such words, Mi for 0 ≤ i < 16, but the compression function expands the Mi to more words (dependant on M0 to M15) to fill up for the rest of the 64 steps. Altogether there are 64 “expanded” message words Wi for 0 ≤ i < 64 defined by
Wi =
(Mi where the functions σ 0 and σ 1 are defined as σ 1(Wi− 2) ⊞ Wi− 7 ⊞ σ 0(Wi− 15) ⊞ Wi− 16 for 16 ≤ i < 64 σ 0(X) = (X ≫ 7) ⊕ (X ≫ 18) ⊕ (X ≫ σ 1(X) = (X ≫ 17) ⊕ (X ≫ 19) ⊕ (X ≫ 3), and
10). Here ⊞ denotes addition modulo 232, ⊕ denotes bitwise XOR, ≫ ≫ denotes the right circular shift operator.
denotes the right shift operator, and The compression function of SHA-256 takes as input a chaining value and message block and computes a new chaining value by applying 64 iterations of a state update procedure. We describe this state update procedure using equations similar to those presented by Mendel et al. [15]. The expanded message words Wi are used to compute internal state variables Ti, Ei, and Ai through the equations Ti = Ei− 4 ⊞ Σ1(Ei− 1) ⊞ IF(Ei− 1, Ei− 2, Ei− 3) ⊞ Ki ⊞ Wi, Ei = Ai− 4 ⊞ Ti, and
Ai = Ti ⊞ Σ0(Ai− 1) ⊞ MAJ(Ai− 1, Ai− 2, Ai− 3).
Here the functions IF and MAJ are defined on words by applying bitwise the functions from F23 to F2 IF(x, y, z) = xy + xz + z, and
MAJ(x, y, z) = xy + yz + xz, and the linear functions Σ0 and Σ1 are defined by Σ0(X) = (X ≫ 2) ⊕ (X ≫ 13) ⊕ (X ≫ 22), and Σ1(X) = (X ≫ 6) ⊕ (X ≫ 11) ⊕ (X ≫ 25).
The chaining value is taken to be [A− 4, . . . , A− 1, E− 4, . . . , E− 1]. In other words, the chaining value sets the initial values of the state variables A and E. For example, A− 4 will be initialized to the first 32-bit word of the chaining value while E− 1 will be initialized to the last word of the chaining value. Ki is a constant given in SHA-256’s specification and there is one unique constant for each step i. The auxiliary variable Ti is introduced to keep the modular additions from having more than 5 addends.
After the state update transformations, the last four A and E words are added with the chaining value to produce a new chaining value, which will be the output of the compression function (and following the final block will be the output of the hash function).
Diferential cryptanalysis is a technique that analyzes how the input diferences influence the output diferences in, for example, a hash function. This technique is crucial in collision attacks of hash functions, since we’re interested in studying the difusion of the input diferences to the output diferences such that we get a zero output diference and a non-zero input diference.
In diferential cryptanalysis of hash collisions, we have two hash inputs and we examine the diferences in all the operations until the output for both inputs. Usually diferences between the values are calculated through XOR operations, such as Δx = x ⊕ x′, where x is a single bit, x′ is its counterpart in the second hash instance, and Δx is the diference of x and x′. In general, a pair (x, x′) representing a bit in one bitvector and its counterpart in the second hash instance may have up to 4 combinations, {(0, 0), (0, 1), (1, 0), (1, 1)}. In some cases, some of the four possibilities may be ruled out, though. The possibilities for (x, x′) can be generalized as the diferential conditions [ 16] presented in Table 1. For example, if a pair (x, x′) has the possibilities {(0, 0), (1, 1)}, we describe it as having the diferential condition ‘-’, whereas the diferential condition ‘ x’ describes the possibilities {(0, 1), (1, 0)}.
For convenience, the diferential conditions of a pair of words (A, A′) can be collectively described in a vector ∇A = [cncn− 1 · · · c1c0], where ci is the diferential condition of the ith bit pair (ai, a′i) with A = [an− 1 · · · a0] and A′ = [a′n− 1 · · · a′0].
The diferential over a function f (X) = Y where X and Y are bitvectors is denoted ∇X → ∇Y . On a high level, we want f to be the hash function while ∇X and ∇Y are the input and output diferences represented by diferential conditions. In practice, analyzing this diferential alone is not helpful as it contains too little information. We want to study all the operations in between as well—chaining the operations in SHA-256 together as a series of steps starting from the input to the output. If we represent the diferences in an operation’s input and output values as a diferential, we can represent the 2 hash function instances as a chain of diferentials. This chain of diferentials is called the diferential path and analyzing this path shows how the diferences propagate from the input diferences all the way to the output diferences, which is essential for finding collisions.
Boolean satisfiability (SAT) solving involves searching for a solution of a Boolean formula (an assignment of the variables that makes the formula true). The tools designed for this purpose are called SAT solvers. Even though all known algorithms for SAT solving run in exponential time in the worst case, in practice many problems can be solved by modern SAT solvers in a reasonable amount of time. In fact, SAT solvers are so efective that in practice there are problems unrelated to logic that are most efectively solved by reducing them to SAT and calling a SAT solver.
The beauty of SAT solving lies in its generic nature, which means that it can be applied to any domain as long as the problem can be encoded into a Boolean formula. This also allows solvers to be tuned for performance independently of a specific problem. Modern SAT solvers can be surprisingly efective at solving SAT problems by incorporating sophisticated techniques like conflict analysis and clause learning, clever branching heuristics, and simplification [ 17]. This combination allows them to be highly potent at general-purpose search.
The SC2 Project. SAT solving, ever since its inception, has been found to be useful for satisfiability checking—determining whether a logical formula is satisfiable. On the other side, Computer Algebra Systems (CASs) include algorithms that are eficient at solving mathematical problems. However, many problems exist that involves both satisfiability checking and symbolic computation, and bridging the two fields was proposed in 2015 in the work of Ábrahám [18] and Zulkoski et al. [19]. Shortly afterwards, the SC2 project [20] was initiated to support the joint community. Since then, a wide variety of problems have been tackled using SC2 techniques, from circuit verification [ 21] to knot theory [22] to quantifier elimination and cylindrical algebraic decomposition [23], and factoring integers with known bits [24]. See England’s survey [25] for an overview of many other examples.
Programmatic SAT. Programmatic SAT involves injecting code into the solver to aid the solver and solve a problem more eficiently than it otherwise could [ 26]. It’s useful especially when aspects of the problem are dificult to express in conjunctive normal form, the typical input of SAT solvers [27].
Programmatic SAT is usually domain-specific and combines the powerful techniques of search possessed by SAT solvers with the most eficient high-level algorithms and analysis tools for the problem. Some modern SAT solvers can be customized in a programmatic way through built-in interfaces like IPASIR-UP [28]. The solver may be aided through the following ways during search: • External propagation: Assigning variables derived through high-level deduction. • External decisions: Making decisions on picking important unassigned variables and guessing their values through high-level analysis. • External learning: Injecting learned clauses during conflicts detected through the high-level conflict analysis.
Cryptographic hash functions such as MD4, MD5, SHA-1, etc. have been extensively relied on for
information security for many years. However, Wang et al. [
The SHA-2 family of hash functions, however, survived these remarkable attacks, likely due to their
relatively complex design with message expansion. One of the earliest attacks on SHA-256 and its
family members was in 2003 by Gilbert and Handschuh [31]. In FSE 2006, Mendel et al. [
In ASIACRYPT 2011, Mendel et al. [15] revealed a collision for 27-step SHA-256 and a semi-free-start (SFS) collision for 32 steps. They automated the search with a domain-specific tool that searches for differential characteristics for SHA-256. The tool utilizes propagation, analysis of the bit constraints, clever branching on the most constraints bits, and contradiction detection in the diferential characteristics.
In EUROCRYPT 2013, Mendel et al. [
Very recently, in the rump session of FSE 2024, Li et al. [
The progress of the attacks on SHA-256 is presented in Table 2.
Our problem is to find two diferent messages whose hashes match, and to do this we use SAT solvers as a search tool for the collision attack. Our SAT formula contains variables encoding two messages (each containing one 512-bit message block) that we want to collide after applying SHA-256. For each block, the formula includes an n-step compression function taking a 512-bit message block and a 256-bit chaining value, and from them computes a 256-bit hash. The number of steps/rounds, n, is adjusted to generate a step-reduced version of SHA-256.
Encoding the compression function includes bitwise Boolean functions such as IF and MAJ. The
other functions, σ 0, σ 1, Σ0, and Σ1, boil down to 3-operand XOR functions after circular rotations and
shifts. For each 3-bit XOR a ⊕ b ⊕ c, our encoding produces x ↔ a ⊕ b ⊕ c (where x is a new auxiliary
variable) using 23 = 8 clauses. A new variable is introduced for every gate in the circuit similar to how
the Tseitin transformation is performed [
The 32-bit modular addition is encoded as bitslices, where each bitslice involves at most 7 addends
(including carries) and a 3-bit output (a high carry, a low carry, and a sum). The addition encoding is
taken from the work of Nejati and Ganesh [
On top of the two hash function instances, we have the diferential cryptanalysis layer. Each Boolean
variable in one instance, say x, has its counterpart x′ in the other instance. For the analysis of the
diferences as per diferential cryptanalysis, we encode the bitwise diferences as Δx ↔ x⊕ x′ (following
Nejati and Ganesh [
A naive way to constrain collisions is to have zero diferences in the hash pair while maintaining at
least one diference in the message pair. However, we want to analyze all the diferences between the
two hash instances, especially the state update as well as the auxiliary variables, to capture as much
information as possible. Thus, we follow the idea of a local collision as presented in the works of Mendel
et al. [
To induce a local collision, we constrain the diferential conditions in the state update variables, A and E, along with the message words, W . The encoding includes clauses for constraining of the conditions as such, and is called the starting point of the diferential path. For example, if a diferential condition on the variable x is constrained to be a ‘-’, we add the unit clause ¬Δx to set the diference to be zero (and thus x = x′). The explicit starting points we used in our work are given in the appendix (Tables 6–9).
Any solution found by the solver will be within the confinements set by the starting point. This reduction of search space is found to very beneficial and the possibility and time required for finding collisions highly depends on a well-crafted starting point.
To make the base problem easier, we also add clauses for the propagation of common diferentials, especially ones with - and x. For example, the encoding has a clause for propagation of [xx-] → [-] for the XOR function, encoding that when x is the auxiliary variable for a ⊕ b ⊕ c we have (Δa ∧ Δb ∧ ¬Δc) → ¬Δx. Such helpful clauses are present for all the operations XOR, MAJ, IF, and the modular addition of words from equation (1) and the state update equations of Section 2.2.2.
As discussed in Section 2.3, analyzing diferential paths is essential in cryptanalysis. There are cases when a diferential path has inconsistencies. In other words, parts of the diferential path define a relation contradicting a relation defined by other parts of the diferential path. For example, if we can derive the conditions a = b and a ̸= b from diferential conditions in the same path, then there certainly cannot exist any message pairs conforming to that path. During solving, it’s crucial to analyze the current path for such inconsistencies and block them as early as possible to prevent the solver from exploring paths that are inconsistent.
The idea of looking for and blocking inconsistencies in the SHA-256 collision attack was utilized by
Mendel et al. [15]. They described having linear equations relating two Boolean variables in SHA-256’s
state. Each of these equations can be derived from bitsliced diferentials of bitwise functions and
modular addition. Such relations can lead to conditions on the equality or inequality of two variables.
Mendel et al. [
Two-bit conditions can be derived from bitsliced diferentials of bitwise functions and addition operations. To deduce the two-bit conditions from a bitsliced diferential, we enumerate all the possibilities and look for a pattern. As an example, consider the diferential ∇[x2x1x0] → ∇[y0] of the XOR operation x0 ⊕ x1 ⊕ x2 = y0. If the diferential is specifically [-0-] → [0], it means that (x2, x0) ∈ {(0, 0), (1, 1)} giving us the two-bit condition x2 = x0.
In practice, two-bit conditions are significantly more common in the bitsliced diferentials of bitwise functions than that of addition operations. Thus, in our experiments, we only computed the two-bit conditions of these bitwise functions to reduce computational costs. Additionally, there are two-bit conditions involving Boolean variables other than that of A, E, and W . For example, two-bit conditions often involve the output variables of bitwise functions along with other auxiliary variables. However, we did not find it beneficial to address inconsistencies involving two-bit conditions of these auxiliary variables. As a result, we focused solely on the two-bit conditions involving the primary variables to block inconsistencies.
The two-bit conditions are expressed in the form x ⊕ y = z where x and y are variables in the diferential path and z ∈ {0, 1}. For example, the two-bit condition x ̸= y gives the equation x ⊕ y = 1. The set of these linear equations often lead to inconsistencies that are non-trivial. For example, if a = b, b = c, and c ̸= a, we have a contradiction involving the 3 two-bit conditions and can be visualized as a cycle a = b = c ̸= a.
Such cycles of inconsistencies translate to cycles of inconsistent diferentials, which in turn are blocked to direct the search away from an invalid diferential path. To do this eficiently we employ a custom-written computer algebraic routine to detect cycles of inconsistent equations during solving. In particular, we use a graph for finding inconsistent cycles, where in the graph each vertex represents a variable and each edge represents a two-bit condition. Every time a new edge is added to the graph, we search for an inconsistent cycle involving that edge (and the shortest such cycle when one exists).
The graph algorithm we use for detecting inconsistent cycles involves a breadth-first search starting from vertex v0 where (v0, vd) is a newly added edge. We look for all possible ways to reach vd excluding the edge (v0, vd). Each edge (u, v) holds a Boolean variable d(u, v) = u ⊕ v, called an edge value, which tells whether the Boolean variables u and v are equal or not.
For each path from v0 to vd found through the method described above, we get a cycle v0, v1, . . . , vd, v0 by adding the edge (v0, vd) to the path. We check if there’s a contradiction in a cycle (connecting Boolean variables v0 to vn) by taking the F2 sum of all the edge values, s = d(v0, v1) + d(v1, v2) + · · · + d(vd− 1, vd) + d(vd, v0). If the sum s is 1, there is an odd number of edges with inequal variables, indicating an inconsistent cycle. We iterate through the inconsistent cycles and take the shortest one for blocking.
When an inconsistency is detected it is blocked by adding a conflict clause constructed from the parts of the SAT solver’s partial assignment (during the time of detection) implying the 2-bit conditions in the cycle. The IPASIR-UP interface [28] is used for feeding the new clause to the solver. The falsified clause causes the solver to backtrack right away, stepping out of the invalid diferential path causing the solver to backtrack earlier than it otherwise would.
During the search for a collision, we work with a partial state that comprises known and unknown variables. Using the known variables, unknown variables may be derived. In other words, the information that we have can spread or propagate. This form of deduction is crucial in the search process. As mentioned in Section 3, many propagation rules such as [xx-] → [-] for the XOR function are encoded directly into the SAT encoding. However, it is not feasible to encode all possible propagation rules on 32-bit words because there are simply too many.
There is a large body of work studying propagation in SAT encodings and metrics by which
propagation can be studied, including propagation completeness [
Since all possibilities for “grounding” ∇X were explored, the maximum amount of possible information was propagated to ∇Y and this is said to be “perfect” propagation. Unfortunately, in general perfect propagation is infeasible because there are too many possibilities to explore.
Perfect propagation is only feasible for small diferentials with a small number of possibilities to explore. However, SHA-256 performs operations on 32-bit words, which means that every function operates on 32-bit words as input. If we want to propagate the output for a function, we’d have to deal with a relatively large number of bits.
To keep the process computationally feasible, we only perform perfect propagation on the output of a bitwise operation in each bit position independently. This reduces the number of bits involved in the propagation while still helping to deduce information. Each output condition is propagated by enumerating all possibilities conforming to the input conditions that the output condition is dependent on—the same as perfect propagation, but only perfect locally. This is a practical version of perfect propagation called “bitsliced” propagation.
For example, suppose we have X ⊞ Y = Z and we want to propagate ∇X = [x-x-] and ∇Y = [x---] to ∇Z. We will focus on propagating information for the second-least significant bit; this bitslice is highlighted in bold in the depiction below: ∇Z = ⊞
??[x-x-] [x---] [???-]
In the example above, the wordwise addition (modulo 24) involves 2 addends with the diferential conditions [x-x-] and [x---], and the first row denotes the diferential conditions of the carries. In general the bitslices involve 3 input conditions and 2 output conditions (namely, a sum diferential bit and a carry diferential bit). The conditions are derived through perfect propagation on each bitslice—in this case the slice having a width of 1 bit.
In this example, the highlighted bitsliced diferential [-x-??] (with the last ? denoting the carry) after propagation becomes [-x-x?] (i.e., the sum diferential bit becomes an x). This process of bitwise propagation can be repeated for the rest of the bit positions, resulting in propagation over a wordwise operation with a low cost.
SHA-256’s hash output is calculated by a series of Boolean operations on 32-bit words. Each step involves the state update equations of Section 2.2.2 that are used for transforming the state variables A and E. We also have the message expansion equation (1) defining Wi for all steps i ≥ 16. All these equations involve modular additions and therefore to efectively search for collisions it is essential to have efective propagation for the modular additions. Bitsliced propagation is helpful in deriving information for modular additions, however, this technique doesn’t capture all the relations between the bits as it is local to a bitslice and doesn’t operate on the entirety of the 32-bit words.
To mitigate this shortcoming of bitwise propagation, we utilize a global “wordwise” propagation technique, that is significantly cheaper than perfect propagation on words pairs in practice but typically derives more information than bitwise propagation.
Wordwise propagation works by exploiting the constraints in the modular addition, such as the
modular integer diferences of words. Modular diferences of words were also used in the work of Wang
and Yu [
When A ⊞ B = C and A′ ⊞ B′ = C′, wordwise propagation may derive additional information on the diferential conditions ∇A and ∇B if the modular diference of C and C′ is known. Denoting modular subtraction of two 32-bit words by ⊟ , the modular diference of C and C′ is (2) (3) δC := C ⊟ C′ = 31 X(ci − c′i)2i i=0 mod 232 where ci and c′i denote the ith least significant bits of C and C′.
In the previous example, the modular addition equations in both the hash instances can be combined via (A ⊟ A′) ⊞ (B ⊟ B′) = C ⊟ C′ which can be rewritten as δA ⊞ δB = δC .
In general, wordwise propagation is performed on equations like
δA 1 ⊞ δA 2 ⊞ · · · ⊞ δA n = C where C can be determined in advance and we want to derive some additional information on at least one of the diferential conditions ∇A1 to ∇An.
For example, suppose we know δA = δB , ∇A = [ux-], and ∇B = [-n-]. It follows that δB = 0 · 22 + (0 − 1) · 2 + 0 = − 2 is known (modulo 8), but δA = (1 − 0) · 22 + (a1 − a′1) · 2 + 0 = 4 ± 2 is either 2 or 6 since a1 − a′1 = ± 1. From ∇A alone the value of δA cannot be determined exactly, but when the additional constraint δA = δB is considered it is clear that the only solution is δA = 6 meaning that a1 − a′1 = 1. Thus, wordwise propagation in this case would derive ∇A = [uu-].
To avoid dealing with negative numbers, the diferential conditions x, n, and ? are normalized by adding an appropriate power of two. For example, in the above example 21 would be added making the equation (1 − 0) · 22 + w · 21 + 0 = − 2 + 21 = 0 where w := a1 − a′1 + 1 ∈ {0, 2} becoming (1 + v) · 22 = 0 where v := w/2 ∈ {0, 1}. As a 3-bit bitvector equation (hence performed modulo 23), this is [1 + v, 0, 0] = [0, 0, 0] which has just one solution v = 1.
Dividing into subproblems. After reducing equations of the form (3) to bitvector equations, we want to determine all solutions for the variables. To do so, we search for possible values through brute force. Since this has an exponential time complexity, we divide the problem into smaller components by analyzing the cascading efects of the carries. In practice, this reduces the computational cost significantly as the subproblems can usually be solved quickly, and any subproblem that is too expensive to solve can be skipped without afecting the other subproblems. In our work, we consider any subproblem with more than 10 variables as expensive, limiting the number of (brute force) iterations to 210 = 1024 for a subproblem.
As an example, suppose δA ⊞ δB = δC where ∇A = [u1xxx], ∇B = [xx-nx], and ∇C = [---u-]. Then δC = 2, and after normalizing A and B we derive
(δA + 22 + 2 + 1) ⊞ (δB + 24 + 23 + 2 + 1) = δA ⊞ δB ⊞ 2 = 4, becoming the bitvector modular addition problem [ 1, v3, v2, v0, 0 ] δA ⊞ δB ⊞ 2 = ⊞ [ v4, 0, 0, v1, 0 ] 0 0 1 0 0 where v0, . . . , v4 ∈ {0, 1}.
Now, a linear scan is performed starting from the least significant digit (the rightmost column). Since there’s no variable in the first column, we skip it. Next, we have a subproblem candidate v0 + v1 ≡ 0 (mod 2). Since this addition can overflow, the next column must be included in the subproblem. Including the next column results in the subproblem v0 + v1 + 2v2 ≡ 2 (mod 4) which cannot overflow since v0 = v1 = v2 = 1 is not a solution. Thus, the problem starting in the next column is independent.
The next problem is then v3 ≡ 0 (mod 2), which only has one solution v3 = 0 and thus also cannot overflow and is independent of the final column. Similarly, the final column results in the subproblem 1 + v4 ≡ 0 (mod 2) which only has the single solution v4 = 1.
In this example wordwise propagation thus determines that v4 = 1 and v3 = 0. Since v4 arose from the second ‘x’ in ∇B which encodes the diference b3 ⊕ b′3, i.e., v4 = (b3 − b′3 + 1)/2, we derive that (b3, b′3) = (1, 0). Similarly, v3 arose from the ‘x’ in ∇A encoding a2 ⊕ a′2, i.e., v3 = (a2 − a′2 + 1)/2, and we derive that (a2, a′2) = (0, 1). Thus, in this example wordwise propagation deduces the updated diferential conditions ∇A = [u1nxx] and ∇B = [xu-nx].
Implementation Details. Wordwise propagation was applied to all the modular addition equations, specifically the message expansion (1) and state update transformation equations, including the one for the auxiliary word Ti. However, the only variables that were propagated were the diferential variables in ∇Ai, ∇Ei, and ∇Wi.
During the wordwise propagation routine, a heuristic that we used which we found dramatically improved the eficiency of the solver was to assume that any diferential ‘ ?’ in the auxiliary variables (including ∇Ti and the diferential variables corresponding to the output of IF, MAJ, σ 0, Σ0, etc.) was actually a ‘-’ diferential. In practice, making this assumption allowed the modular diference of the auxiliary diferential words to be calculable much more frequently, and increased the likelihood that variables in the word diferentials ∇Ai, ∇Ei, and ∇Wi were derived. This heuristic is related to the ‘decision’ search strategy of Mendel et al. [15] which always first imposes a ‘ -’ for a ‘?’ before imposing a ‘x’. However, we found that making assumptions on the primary word diferentials ∇Ai, ∇Ei, and ∇Wi themselves significantly decreased the solver’s performance, preventing us from finding SFS collisions for SHA-256 beyond 28 steps.
Our programmatic SAT solver was implemented in CaDiCaL 1.8.0 [
The IPASIR-UP programmatic interface provides access to the current state of the solver for the relevant variables (i.e., those encoding the state of the hash function and the diferential variables). IPASIR-UP also enables us to perform custom propagation and branching as well as learning custom conflict clauses.
For implementing inconsistency blocking, we used our own implementation of a graph library. This
houses the graph algorithm described in Section 4 for detecting minimal inconsistent cycles in linear
time. Our implementations of bitsliced and wordwise propagation, as well as the two-bit condition
detection engine used for inconsistency blocking, are based on the ideas described in the works of
Mendel et al. [15] and Eichlseder [
In our experiments, most queries to the propagation and two-bit detection engines could be served from the cache, which is much faster than deriving the propagation rules or the two-bit conditions on the fly each time. Since the set of rules that are queried throughout the entire runtime is usually small (i.e., consumes a small portion of the total CPU time), it wasn’t necessary to precompute any rules.
We perform bitsliced propagation for all operations in SHA-256 (including the modular additions) alongside the solver’s built-in Boolean constraint propagation (BCP). As wordwise propagation is much more expensive in terms of computational cost, it’s performed only when the SAT solver finishes with the other propagation methods. This way, wordwise propagation only deduces the conditions that bitsliced propagation couldn’t.
IPASIR-UP asks for a “reason” clause of propagated literals when it becomes necessary for the solver to know why a literal was propagated. For bitsliced propagation, these reason clauses were relatively short, so in this case we provided reason clauses directly via IPASIR-UP’s interface. On the other hand, wordwise propagation involves multiple word pairs and a single propagated literal may depend on a relatively large number of bits, leading to long reason clauses. To avoid overwhelming the solver with long reason clauses, we did not use IPASIR-UP’s propagation interface for wordwise propagation and instead set the values of any literals deduced by wordwise propagation via branching.
We performed the same experiment with three separate solvers: an unmodified version of CaDiCaL
1.8.0, a version of CaDiCaL with programmatic bitsliced and wordwise propagation, and a version
of CaDiCaL with both programmatic propagation and inconsistency blocking. We also tried using
CryptoMiniSat 5.11.21 [
With each solver we searched for semi-free-start collisions for step-reduced SHA-256 with 20 to 38 steps. In order to reduce the randomness inherent in the search, each instance was solved ten times independently using 10 diferent random seeds, though these 10 diferent seeds were consistently used across all our experiments. Each instance was run for a time limit of 500,000 seconds (roughly 5.8 days). The number of instances successfully solved in each case is given in Table 3, and the minimum time for ifnding a collision is plotted in Figure 3. The starting points used for the 21-step, 25-step, 28-step, and 38-step instances are given in the appendix. The starting points for all other step counts were formed from one of these starting points by dropping a number of rows at the bottom, e.g., the 26-step instance matches the 28-step starting point with two rows removed. This means that the instances in the step
CaDiCaL CaDiCaL/P CaDiCaL/P+IB 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
Steps ranges 20–21, 22–25, 26–28, and 29–38 can be expected to roughly have similar dificulty as they were created from the same starting point.
The results show that programmatic propagation was clearly efective at helping the solver find SFS collisions. The plain SAT solver could only find SFS collisions up to 28 steps, while CaDiCaL with programmatic propagation, both with and without inconsistency blocking, successfully found SFS collisions for every step count from 20 to 38, with the exception of 35—no 35-step instances were solved when both programmatic propagation and inconsistency blocking were enabled (see Table 3). In general, we found inconsistency blocking tended to decrease the eficiency of the solver, although using inconsistency blocking did result in the fastest solve times for the instances with 30, 31, 32, and 36 steps.
In this work we combine the programmatic SAT+CAS paradigm with the diferential cryptanalysis
techniques used in previous collision attacks on SHA-256. In the process, we demonstrate that these
computer algebraic techniques can dramatically improve the performance of the SAT solver, enabling
the SAT+CAS solver to find a semi-free-start collision of SHA-256 with 38 steps, while a plain SAT
solver could go no further than 28 steps. Moreover, previous 38-step SFS collisions [
At the time the work in this paper was performed, the best SFS collision ever found for SHA-256
contained 38 steps [
We thank the chairs of the SC-Square 2024 workshop, Daniela Kaufmann and Chris Brown, for their
lfexibility during the publication process of this paper, and the anonymous reviewers for their detailed
comments. We also thank Maria Eichlseder for her insight and answering a number of questions
concerning state-of-the-art hash function collision search tools, as well as Oleg Zaikin for answering
questions about his work on inverting 43-step MD4 [
Knots, Springer International Publishing, 2017, pp. 3–18. doi:10.1007/978-3-319-72453-9_1. [23] C. W. Brown, Projection and quantifier elimination using non-uniform cylindrical algebraic decomposition, in: Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC’17, ACM, 2017, pp. 53–60. doi:10.1145/3087604.3087651. [24] Y. Ajani, C. Bright, SAT and lattice reduction for integer factorization, in: Proceedings of the 2024 ACM on International Symposium on Symbolic and Algebraic Computation, 2024. doi:10.1145/ 3666000.3669712, to appear. [25] M. England, SC-Square: Overview to 2021, in: C. Bright, J. H. Davenport (Eds.), SC-Square 2021: Satisfiability Checking and Symbolic Computation, volume 3273 of CEUR Workshop Proceedings, CEUR, 2022, pp. 1–6. URL: https://ceur-ws.org/Vol-3273/invited1.pdf. doi:10.48550/arXiv. 2209.04359. [26] V. Ganesh, C. W. O’Donnell, M. Soos, S. Devadas, M. C. Rinard, A. Solar-Lezama, Lynx: A Programmatic SAT Solver for the RNA-Folding Problem, Springer Berlin Heidelberg, 2012, p. 143–156. doi:10.1007/978-3-642-31612-8_12. [27] C. Bright, V. Ganesh, A. Heinle, I. Kotsireas, S. Nejati, K. Czarnecki, MathCheck2: A SAT+CAS verifier for combinatorial conjectures, in: Computer Algebra in Scientific Computing, Springer International Publishing, 2016, pp. 117–133. doi:10.1007/978-3-319-45641-6_9. [28] K. Fazekas, A. Niemetz, M. Preiner, M. Kirchweger, S. Szeider, A. Biere, IPASIR-UP: User propagators for CDCL, in: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2023, pp. 8:1–8:13. doi:10.4230/ LIPIcs.SAT.2023.8. [29] X. Wang, Y. L. Yin, H. Yu, Finding collisions in the full SHA-1, in: Advances in Cryptology– CRYPTO 2005: 25th Annual International Cryptology Conference, Santa Barbara, California, USA, August 14-18, 2005. Proceedings 25, Springer, 2005, pp. 17–36. doi:10.1007/11535218_2. [30] M. Stevens, E. Bursztein, P. Karpman, A. Albertini, Y. Markov, The First Collision for Full SHA-1,
Springer International Publishing, 2017, pp. 570–596. doi:10.1007/978-3-319-63688-7_19. [31] H. Gilbert, H. Handschuh, Security analysis of SHA-256 and sisters, in: International workshop on selected areas in cryptography, Springer, 2003, pp. 175–193. doi:10.1007/978-3-540-24654-1_ In the appendix, we provide an example of a 38-step semi-free-start SHA-256 collision that we found (Table 4), a table showing its diferential characteristic (Table 5), and the starting points that we used in our search.
The 21-step starting point (Table 6) is taken from the work of Prokop [
The 38-step starting point (Table 9) is constructed based on the 38-step diferential characteristic
provided by Mendel et al. [
∇Wi
∇Wi -----------------------------------------------------------------------------------------------------------------------------------------------------------???????????????????????????????? ???????????????????????????????? ???????????????????????????????? ???????????????????????????????? ----------------------------------------------------------------------------------------------------------------------------???????????????????????????????? -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
∇Wi --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------???????????????????????????????? ???????????????????????????????? -------------------------------???????????????????????????????? ----------------------------------------------------------------------------------------------------------------------------???????????????????????????????? --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
∇Wi --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------x??????????????????????????????? ???????????????????????????????? ---------------------------------------------------------------------------------------------???????????????????????????????? --------------------------------------------------------------???????????????????????????????? -------------------------------???????????????????????????????? ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------