Keywords

1 Introduction

Before the devastating attacks in 2005 [38,39,40,41] on the MD-SHA hash family, there was a trend to design fast hash functions with a similar structure to MD4, including MD5, SHA-0, SHA-1, SHA-2, RIPEMD-128 and RIPEMD-160, just to name a few. After 2005, we have witnessed efficient collision attacks on full MD4  [38], MD5  [40], SHA-0  [2, 41], and SHA-1  [15, 16, 36, 39] as well as the SFS collision attack on full RIPEMD-128  [14]. In spite of these successful attacks on the MD-SHA hash family, SHA-2 survived this game, mainly due to its more conservative and complex design. Since SHA-2 has been used worldwide, studying its collision and preimage resistances is always of practical interest, though it is also challenging.

Preimage Attacks on SHA-2. In the past few years, there have been many results for the preimage attacks on SHA-256 and SHA-512. The first preimage attack on SHA-256 and SHA-512  [11] based on the meet-in-the-middle (MITM) technique reached 24 steps with a complexity of about \(2^{240}\) and \(2^{480}\), respectively. These preimage attacks were significantly improved at ASIACRYPT 2009 [1], which were improved to 43-step SHA-256 and 46-step SHA-512, respectively. Then, at ASIACRYPT 2010, Guo et al. [9] presented advanced MITM preimage attacks on 42-step SHA-256 and SHA-512, respectively. At FSE 2012, the biclique technique was applied to find preimages of SHA-2  [12], where preimage attacks on 45-step SHA-256 and 50-step SHA-512 with time complexity of \(2^{255.5}\) and \(2^{511.5}\) were achieved, respectively. It should be noted that the authors in [12] also presented pseudo-preimage attacks on 52-step SHA-256 and 57-step SHA-512 with a complexity of \(2^{255}\) and \(2^{511}\), respectively. However, all these preimage attacks are far from practical.

Distinguishing Attacks on the Compression Function of SHA-2. Compared with preimage and collision attacks, distinguishing attacks are less meaningful for a hash function, though they can help better understand its security. At the rump session of EUROCRYPT 2008 [43], the non-randomness of 39-step SHA-256 was presented, and a practical example for 33 steps was given by Yu and Wang. In [10], free-start (FS) near-collisions for up to 31 steps of SHA-256 were presented. Then, Lamberger and Mendel gave a second-order differential attack on 46 steps of SHA-256 with a practical complexity in [13]. Later, this attack was extended to 47 steps of SHA-256 with a practical complexity at ASIACRYPT 2011 [3]. At INSCRYPT 2014 [42], Yu and Bai further utilized the attack strategy in [3] to mount a practical distinguishing attack on 48 steps of SHA-512.

Collision Attacks on SHA-2. The first practical collision attack on SHA-256  [30] was presented at FSE 2006, only reaching 18 steps. At FSE 2008, Nikolic and Biryukov [33] improved this practical attack to 21 steps, and they also gave a SFS collision attack on 23 steps of SHA-256. This attack was later further extended to 24 steps of SHA-256 and SHA-512 in [10, 34]. Then, at ASIACRYPT 2011, the first major improvement was achieved, where the advanced guess-and-determine (GnD) technique to search for SHA-2 characteristics was invented [26], and the SFS collision for 32-step SHA-256 and the collision for 27-step SHA-256 were presented, respectively. After this work at ASIACRYPT 2011, this advanced automatic tool has been gradually improved in 3 papers published at EUROCRYPT 2013 [28], FSE 2014 [8] and ASIACRYPT 2015 [6]. In addition, much more complex message differences are used to mount (FS/SFS) collision attacks on SHA-2 in these 3 papers. A summary of these collision attacks is shown in Table 1.

Automatic Tools to Search for SHA-2 Characteristics. Although major achievements have been made in collision attacks on SHA-2 in [6, 8, 26, 28], the corresponding advanced automatic tool to find SHA-2 characteristics is not open-source. Due to the complex design of SHA-2, this significantly increased the difficulty to follow these works without this tool, let alone to improve this tool. Although Stevens open sourced his dedicated tools [35,36,37] to find MD5 and SHA-1 characteristics, they could not be applied to SHA-2 as SHA-2 is too complex, and contradictions easily occur in its differential characteristics [26]. Recently, to make finding collision-generating signed differential characteristics easier, Liu et al. invented a novel MILP-based method [24] and it works quite well for RIPEMD-160. As can be observed in [24], two main techniques are how to describe signed difference transitions through each component of the step function and how to automatically detect contradictions in an efficient way. At the end of [24], the authors left an interesting problem whether it is possible to apply this technique to SHA-2 because it is required for the model to detect more contradictions in SHA-2 characteristics.

Our Contributions. We briefly summarize our contributions as follows:

  1. 1.

    We demonstrate for the first time that the technique developed in [24] can be applied to SHA-2, and this obviously gives a positive answer to the question left in [24]. Specifically, we develop a SAT/SMT-based tool to efficiently search for valid SHA-2 differential characteristics based on the technique to search for signed differential characteristics in [24] and the technique to automatically verify the correctness of a differential characteristic in [21].

  2. 2.

    We shed new insight into the (free-start/semi-free-start) collision attacks on SHA-2. For the first time, we are able to propose:

    • the first practical SFS colliding message pair for 39-step SHA-256, breaking the record of 38 steps kept by Mendel et al. at EUROCRYPT 2013 [28] after 10 years;

    • the first practical free-start colliding message pair for 40-step SHA-224, improving the previously best theoretic 40-step attack with time complexity \(2^{110}\) published at FSE 2012 [17];

    • the first practical colliding message pair for 28-step SHA-512, updating the previously best record given at ASIACRYPT 2015 [6] by 1 step.

    • the first collision attack on 31-step SHA-512 with time complexity \(2^{115.6}\), improving the previously best one published at ASIACRYPT 2015 [6] by 4 steps.

In addition to these notable progress, we also improved the best collision attack on 31-step SHA-256 published at EUROCRYPT 2013 [28], reducing the time complexity from \(2^{65.5}\) to \(2^{49.8}\). Our results are summarized in Table 1. Especially, we note that there is gap between the previous (SFS) collision attacks on SHA-256 and SHA-512. Specially, due to the similarity between SHA-256 and SHA-512, a (SFS) collision attack on r steps of SHA-256 should have been applicable to r steps of SHA-512, and vice versa. However, this is not the case in previous attacks, as shown in Table 1. We believe this is caused by the infeasibility to find the corresponding valid SHA-2 characteristics with the current GnD technique. Based on our new technique, we have made the (SFS) collision attacks on SHA-256 and SHA-512 reach the same number of steps.

Moreover, based on our results for SHA-2, it indicates that the SAT/SMT-based method performs much better than the dedicated but non-open-source ones developed in [6, 8, 26, 28]. This also contradicts the claims made in [8] that the performance of SAT-based method for SHA-2 is bad. Note that our SAT/SMT-based method is completely different from the one used in [8], which simply uses a model to describe two parallel instances of the value transitions as in [32].

Table 1. Summary of collision attacks on SHA-2, where FS collision\(^{\star }\) denotes the free-start collision without considering padding, and SFS collision denotes the semi-free-start collision.

The source code to search for the differential characteristics and verify the (SFS/FS) collisions for SHA-256 and SHA-512 is available at https://github.com/Peace9911/sha_2_attack.git.

Outline. This paper is organized as follows. The notations and some preliminary works of this paper are introduced in Sect. 2. A high-level overview of how to implement the MILP-based method with an SAT/SMT-based method and how to overcome more contradictions in the differential characteristics of SHA-2 in is given Sect. 3. Then, we show how to find the differential characteristics to mount the (SFS/FS) collisions for SHA-2 in Sect. 4. Finally, we conclude this paper in Sect. 5.

2 Preliminaries

2.1 Notations

For a better understanding of this paper, we introduce the following notations.

  1. 1.

    \(\boxplus \) and \(\boxminus \) represent modulo addition and modulo subtraction on 32/64 bits, respectively.

  2. 2.

    \(\gg \), \(\ggg \), \(\oplus \), \(\lnot \), \(\vee \) and \(\wedge \) represent shift right, rotate right, exclusive or, not, or, and and, respectively.

  3. 3.

    x[i] denotes the i-th bit of x and x[0] is the least significant bit.

  4. 4.

    \(\delta x\) denotes the modular difference, i.e., \(\delta x = x^{\prime } \boxminus x\).

  5. 5.

    \(\varDelta x\) denotes the signed difference between \(x^{\prime }\) and x. We use the same notation as in [22, 24], i.e.,

    $$\begin{aligned} \varDelta x[i]=\left\{ \begin{aligned} &\texttt {n} \ \ (x[i]=0, x^{\prime }[i]=1)\\ &\texttt {u} \ \ (x[i]=1, x^{\prime }[i]=0)\\ &\texttt {=} \ \ (x[i]=x^{\prime }[i])\\ &\texttt {0} \ \ (x[i]=x^{\prime }[i]=0)\\ &\texttt {1} \ \ (x[i]=x^{\prime }[i]=1) \end{aligned} \right. \end{aligned}$$
    (1)
  6. 6.

    \(M = (m_0, m_1,\ldots , m_{15})\) and \(M^{\prime } = (m_{0}^{\prime }, m_{1}^{\prime },\ldots , m_{15}^{\prime })\) represent two message blocks.

Definition 1

[24]. The signed difference \(\varDelta x\) is said to be an expansion of the modular difference \(\delta x\) only when \(\varDelta x\) corresponds to the modular difference \(\delta x\).

Definition 2

[24]. The hamming weight of the signed difference \(\varDelta x\) is denoted by H(\(\varDelta x\)) and H(\(\varDelta x\)) is the number of indices i such that \(\varDelta x[i] \in \{\texttt {n}, \texttt {u}\}\).

For example, let

figure a

Then, both \(\varDelta x_0\) and \(\varDelta x_1\) are the expansions of \(\delta x = 2^{26}\). Moreover, we have H(\(\varDelta x_0\)) = 2 and H(\(\varDelta x_1\)) = 1. As each signed difference corresponds to a unique modular difference, for convenience, when computing \(\delta x \boxplus \delta y\) for a given \((\varDelta x,\varDelta y)\), we also simply denote \(\delta x \boxplus \delta y\) by \(\varDelta x \boxplus \varDelta y\). For the above example, we have \(\varDelta x_0 \boxplus \varDelta x_1 = 2^{27}\).

2.2 Description of SHA-2

The SHA-2 family is a series of hash functions standardized by NIST as part of the Secure Hash Standard (SHS) [7]. This family mainly consists of two versions, namely SHA-256 and SHA-512. Furthermore, NIST defines a general truncation procedure for SHA-256 and SHA-512, which includes SHA-224, SHA-512/224, SHA-512/256 and SHA-384. SHA-2 adopts the well-known Merkle-Damgård construction [5, 31], and its compression functions employ the Davies-Meyer construction. As the two main versions of SHA-2, SHA-256 and SHA-512 have 32-bit and 64-bit state words, respectively. SHA-256 and SHA-512 utilize 512-bit message words and 1024-bit message words as input, with their chaining variables and final outputs being 256 bits and 512 bits, respectively.

The compression functions of SHA-256 and SHA-512 are computed through iterative updates to internal states. The number of steps, which is denoted by r, is 64 for SHA-256 and 80 for SHA-512. In the following, we provide a brief overview of their compression functions. They consist of two main parts: the message expansion and the state update transformation. A complete description of SHA-2 is given in [7].

Message Expansion. The 512-bit message block for SHA-256 and the 1024-bit message block for SHA-512 are divided into 16 message words of sizes 32 bits and 64 bits, respectively, which are denoted by \((m_1,\ldots ,m_{15})\). Then, the 16 message words are expanded to r expanded message words \(W_{i}\), i.e., \(W_{0}, W_{1}, \ldots , W_{r-1}\):

$$W_i = {\left\{ \begin{array}{ll} m_i &{} 0 \le i \le 15, \\ \sigma _{1}(W_{i-2}) \boxplus W_{i-7} \boxplus \sigma _0(W_{i-15}) \boxplus W_{i-16} &{} 16 \le i \le r-1. \\ \end{array}\right. }$$

The functions \(\sigma _0(x)\) and \(\sigma _{1}(x)\) in SHA-256 are given by

$$\begin{aligned} \sigma _0(x) = & {} (x \ggg 7) \oplus (x \ggg 18) \oplus (x \gg 3),\\ \sigma _1(x) = & {} (x \ggg 17) \oplus (x \ggg 19) \oplus (x \gg 10). \end{aligned}$$

The functions \(\sigma _0(x)\) and \(\sigma _{1}(x)\) in SHA-512 are given by

$$\begin{aligned} \sigma _0(x) = & {} (x \ggg 1) \oplus (x \ggg 8) \oplus (x \gg 7),\\ \sigma _1(x) = & {} (x \ggg 19) \oplus (x \ggg 61) \oplus (x \gg 6). \end{aligned}$$

State Update Transformation. We utilize the alternate description for the state update of SHA-256 and SHA-512, as illustrated in Fig. 1.

Fig. 1.
figure 1

The state update transformation of SHA-2.

The state update transformation starts from a 256-bit (resp. 512-bit) chaining value \(iv = (A_{-1},\ldots , A_{-4}, E_{-1},\ldots , E_{-4})\) for SHA-256 (resp. SHA-512), and updates it by applying the step function r times. In each step \(i = 0,\ldots ,r-1\), one expanded message word \(W_i\) is used to compute the two state words \(E_i\) and \(A_i\) as follows, where \(K_i\) is a predefined constant and can be referred to [7].

$$\begin{aligned} E_i = & {} A_{i-4} \boxplus E_{i-4} \boxplus \varSigma _1(E_{i-1}) \boxplus \textrm{IF}(E_{i-1}, E_{i-2}, E_{i-3}) \boxplus K_i \boxplus W_i,\\ A_i = & {} E_i \boxminus A_{i-4} \boxplus \varSigma _0(A_{i-1}) \boxplus \textrm{MAJ}(A_{i-1}, A_{i-2}, A_{i-3}). \end{aligned}$$

Both SHA-256 and SHA-512 utilize the same Boolean functions IF and MAJ, as defined below:

$$\begin{aligned} \textrm{IF}(x,y,z) = & {} (x \wedge y) \oplus (x \wedge z) \oplus z,\\ \textrm{MAJ}(x,y,z) = & {} (x \wedge y) \oplus (x \wedge z) \oplus (y \wedge z). \end{aligned}$$

However, the linear functions \(\varSigma _0\) and \(\varSigma _1\) are different for SHA-256 and SHA-512. For SHA-256, they are defined below:

$$\begin{aligned} \varSigma _0(x) = & {} (x \ggg 2) \oplus (x \ggg 13) \oplus (x \ggg 22),\\ \varSigma _1(x) = & {} (x \ggg 6) \oplus (x \ggg 11) \oplus (x \ggg 25). \end{aligned}$$

For SHA-512, they are defined below:

$$\begin{aligned} \varSigma _0(x) = & {} (x \ggg 28) \oplus (x \ggg 34) \oplus (x \ggg 39),\\ \varSigma _1(x) = & {} (x \ggg 14) \oplus (x \ggg 18) \oplus (x \ggg 41). \end{aligned}$$

After the last step of the state update transformation, the previous chaining value is added to the output of the state update. The result of this feed-forward sum is the chaining value h:

$$\begin{aligned} h = (A_{63} \boxplus A_{-1},\ldots , A_{60} \boxplus A_{-4}, E_{63} \boxplus E_{-1},\ldots , E_{60} \boxplus E_{-4}). \end{aligned}$$

On Finding (FS/SFS) Collisions. Denote the compression function of SHA-2 by \(h_i=H(h_{i-1},M_i)\). To find a collision with j message blocks, we need to find \((M_1,\ldots ,M_j)\) and \((M_1^{\prime },\ldots ,M_j^{\prime })\ne (M_1,\ldots ,M_j)\) such that \(h_j=h_j^{\prime }\) where \(h_i^{\prime }=H(h_{i-1}^{\prime },M_i^{\prime })\) and \(h_0=h_0^{\prime }\) is a predefined constant. In most cases, only \(M_j\ne M_j^{\prime }\) is required and we have \(M_k=M_k^{\prime }\) for \(1\le k<j\). To find SFS collisions, we need to find \(H(h,M)=H(h,M^{\prime })\) where \(M\ne M^{\prime }\) and h can be an arbitrary value. To find FS collisions, we need to find \(H(h,M)=H(h^{\prime },M^{\prime })\) where \(M\ne M^{\prime }\) and \((h,h^{\prime })\) can be arbitrary values.

2.3 Previous Methods to Search for Differential Characteristics

Almost all effective collision attacks on the MD-SHA hash family rely on Wang et al.’s techniques [38,39,40]. One of the most important steps is to find a collision-generating differential characteristic. For this purpose, there are three methods in the literature, as summarized below.

  • Hand-crafted method: This remarkable work was first done by Wang et al. in their ground-breaking works on MD4 [38], MD5 [40], SHA-0 [41], and SHA-1 [39]. However, for complex designs like SHA-256 and RIPEMD-160, finding such differential characteristics for a large number of steps by hand is almost impossible, or at least considerably time-consuming.

  • Ad-hoc heuristic search tools: De Cannière and Rechberger developed the first heuristic search tool for this problem based on the guess-and-determine (GnD) technique, and successfully applied it to SHA-1  [4]. Subsequently, this heuristic search tool were further developed and it has been applied to many hash functions like RIPEMD-128, RIPEMD-160, SHA-256, and SHA-512  [6, 8, 14, 19, 20, 23, 25,26,27,28,29]. However, the implementation of this GnD-based tool is not open-source. Although Stevens made his tools for MD5 and SHA-1  [35,36,37] open-source, it requires a significant amount of work to tweak them for SHA-2 because contradictions much more easily occur in the differential characteristics of SHA-2, and no existing tools for SHA-2 are based on this method.

  • Off-the-shelf solvers: The method was first explored in [32] with SAT solvers after Wang et al.’s attacks and it was later also applied to SHA-1 in [36]. The main idea is to construct a model to describe two parallel instances of the value transitions. A new MILP-based method proposed by Liu et al. [24] is to model the pure signed difference transitions through each component of the round function, aided with some contradiction-detecting techniques. Especially, this technique [24] works quite well for RIPEMD-160.

3 SAT/SMT-Based Tools for the MD-SHA Hash Family

The first SAT-based method to find collision-generating differential characteristics was proposed in 2006 [32], but the model is to simply describe two parallel instances of the value transitions. To efficiently capture the information of the signed difference propagation, the MILP-based method was proposed in [24]. Although the authors of [24] only target RIPEMD-160, since the MD-SHA hash functions share similar structures, the authors also mention that there are indeed much more applications beyond RIPEMD-160. Especially, whether it is applicable to SHA-2 is left as an interesting problem.

We answer this question in this paper. First, we show how to implement the MILP-based method [24] with an SAT/SMT-based method, and how to detect more contradictions in SHA-2 characteristics. Then, we demonstrate how to utilize our tools to find suitable differential characteristics to significantly improve the (SFS) collision attacks on SHA-2.

For the MILP-based method in [24], the constraints are already in Conjunctive Normal Form (CNF) due to the usage of the software Friday, which can output the minimized CNF for a given truth table with the Quine-McCluskey (QM) algorithm. However, they choose to further convert CNF into linear inequalities in order to use the solver Gurobi [24]. In this sense, we can not claim any novelty for how to re-implement the propagation of signed difference transitions with SAT/SMT. To make this paper self-contained, we briefly describe the idea to model the signed difference propagation with SAT/SMT. Note that when applying it to searching for valid SHA-2 characteristics, nontrivial additional techniques are required, as can be seen later in our detailed description of the search strategy.

For the MD-SHA hash family, it can be observed that in their round functions, there are three basic operations:

  • modular addition;

  • logic shift;

  • Boolean functions.

Hence, we only describe how to describe the signed difference transitions through the modular addition and Boolean functions. For the logic shift, it does affect the model for RIPEMD-160 as shown in [24]. However, in the case of SHA-2, there is no such problem and it only affects the order of the variables. Hence, we simply omit it in this section.

Since we will target both SHA-256 and SHA-512, and their state sizes are 32 and 64 bits, respectively, to make the description of the model general, we treat the state size as n bits, i.e., the modular addition is within modulo \(2^n\).

3.1 SAT/SMT Models for the Signed Difference Transitions

Similar to [24], we use 2 binary variables (vd) to describe the signed difference. Specifically, (0, 0), (0, 1) and (1, 1) correspond to \(\texttt {[=]}\), \(\texttt {[n]}\) and \(\texttt {[u]}\), respectively, while we always exclude (1, 0) as it carries the same information as (0, 0). For the n-bit signed difference \(\varDelta x\), throughout this paper, the signed difference at the i-th \((0\le i\le n-1)\) bit is always represented by \((x_v[i], x_d[i])\). For example, if \(n=5\) and \(\varDelta x=[\)=u==n], we have

$$\begin{aligned} {} & {} (x_v[0],x_d[0])=(0,0), (x_v[1],x_d[1])=(1,1), (x_v[2],x_d[2])=(0,0),\\ {} & {} (x_v[3],x_d[3])=(0,0), (x_v[4],x_d[4])=(0,1). \end{aligned}$$

Modelling the Modular Addition. As explained in [24], given the signed difference \(\varDelta x\) and \(\varDelta y\), it is sufficient to pick only 1 signed difference \(\varDelta z\) to describe the modular difference \(\delta z=\delta x\boxplus \delta y\).

To achieved this, the intermediate variable \(\varDelta c\) with \(\varDelta c[0]=[\texttt {=}]\) is introduced and the propagation rules for

$$ (\varDelta x[i],\varDelta y[i],\varDelta c[i]) {\mathop {\longrightarrow }\limits ^{Add}} (\varDelta z[i],\varDelta c[i + 1]) $$

are shown in Table 2, where \(0\le i\le n-1\).

Table 2. The propagation rules for \((\varDelta x[i],\varDelta y[i],\varDelta c[i]) {\mathop {\longrightarrow }\limits ^{Add}} (\varDelta z[i],\varDelta c[i + 1])\) in [24]

With the above method to describe the signed difference, there are 27 possible values for

$$ (x_v[i], x_d[i], y_v[i], y_d[i], c_v[i], c_d[i], z_v[i], z_d[i], c_v[i + 1], c_d[i + 1]) $$

based on Table 2. With the software LogicFriday, we can obtain the corresponding CNF to describe that this tuple can only take these 27 possible values. For convenience, we denote the CNF by \(\mathcal {C}_{\texttt {Add}}(i)\). In this way, the complete model for the modular addition can be described with \(\mathcal {C}_{Add}(i)\) for \(0\le i\le n-1\) and \((c_v[0],c_d[0])=(0,0)\).

For convenience, we denote the model for the modular addition \(\delta z=\delta x\boxplus \delta y\) by \(\mathcal {C}_{Add}(\varDelta x,\varDelta y,\varDelta z,\varDelta c)\).

Modelling the Expansions of the Modular Difference [24]. In the above model, the signed difference transition through the modular addition is deterministic. To obtain all possible signed differences corresponding to the same modular difference, the authors of [24] introduce a model to describe the expansions of the modular difference. Given one \(\varDelta z\), the aim is to find all possible \(\varDelta \xi \) such that \(\delta \xi =\delta z\), i.e., \(\varDelta \xi \) and \(\varDelta z\) correspond to the same modular difference. To achieve this, as in [24], an intermediate variable \(\varDelta c\) is introduced and there are two methods to model it, as shown in Table 3.

Table 3. Two methods to describe the propagation rules for the expansion of modular difference [24]

Similarly, based on the above way to describe the signed difference and using the software LogicFriday, the corresponding CNF to describe the constraints on

$$\begin{aligned} (z_v[i], z_d[i], c_v[i], c_d[i], \xi _v[i], \xi _d[i], c_v[i + 1], c_d[i + 1]) \end{aligned}$$

for Method 1 can be obtained, which is denoted by \(\mathcal {C}_{Exp}(i)\). The complete model for the expansion of the modular difference is thus \(\mathcal {C}_{Exp}(i)\) for \(0\le i\le n-1\) and \((c_v[0],c_d[0])=(0,0)\) for Method 1.

In the same way, we can also obtain the corresponding CNF denoted by \(\mathcal {C}_{Exp}^{\prime }(i)\) to describe the constraints on

$$\begin{aligned} (\xi _v[i], \xi _d[i], z_v[i], z_d[i], c_v[i], c_d[i], c_v[i + 1], c_d[i + 1]) \end{aligned}$$

for Method 2. The complete model for the expansion of the modular difference is thus \(\mathcal {C}_{Exp}^{\prime }(i)\) for \(0\le i\le n-1\) and \((c_v[0],c_d[0])=(0,0)\) for Method 2.

For convenience, we denote the model for the expansions of the modular addition in Method 1 and Method 2 by \(\mathcal {C}_{Exp}(\varDelta z,\varDelta \xi ,\varDelta c)\) and \(\mathcal {C}_{Exp}^{\prime }(\varDelta z,\varDelta \xi ,\varDelta c)\).

Modelling the Vectorial Boolean Functions \(\boldsymbol{w=f(x,y,z)}\) [24]. In SHA-2, there are some vectorial Boolean functions, i.e., f can be XOR, IF or MAJ where \(XOR(x,y,z)=x\oplus y \oplus z\). Note that \(\sigma _0\), \(\sigma _1\), \(\varSigma _0\) and \(\varSigma _1\) in SHA-2 are basically the same as XOR. Generally speaking, we can have

$$ w[i] = f_i(x[i],y[i],z[i]) $$

where \(f_i\) is a Boolean function \(\mathbb {F}_2^3 \mapsto \mathbb {F}_2\) and \(0\le i\le n-1\). As described in [24], there are two models for \((f_i)_{0\le i\le n-1}:\) (i) the fast filtering model; (ii) the full model.

For the fast filtering model, we first need to build a table to include all valid propagation rules for \((\varDelta x[i],\varDelta y[i],\varDelta z[i],\varDelta w[i])\) and then obtain the corresponding valid values for

$$ (x_v[i], x_d[i], y_v[i], y_d[i], z_v[i], z_d[i], w_v[i], w_d[i]). $$

Finally, LogicFriday is used to obtain the corresponding CNF for the constraints on this tuple.

For the full model, we need to involve both the signed difference and bit values. Specifically, the first step is to list all possible propagation rules for

$$\begin{aligned} (\varDelta x[i],\varDelta y[i],\varDelta z[i],\varDelta w[i], x[i],y[i],z[i]), \end{aligned}$$

where (x[i], y[i], z[i]) can make the signed difference transition

$$\begin{aligned} (\varDelta x[i],\varDelta y[i],\varDelta z[i]){\mathop {\longrightarrow }\limits ^{f_i}}\varDelta w[i] \end{aligned}$$

hold with probability 1. Then, we can obtain all the possible valid values for

$$ (x_v[i], x_d[i], y_v[i], y_d[i], z_v[i], z_d[i], w_v[i], w_d[i],x[i],y[i],z[i]). $$

Finally, with LogicFriday, we obtain the corresponding CNF to describe the constraints on this tuple.

For convenience, we denote the fast filtering model and full model for \(w=f(x,y,z)\) by \(\mathcal {C}_{fast}^{f}(\varDelta x, \varDelta y, \varDelta z, \varDelta w)\) and \(\mathcal {C}_{full}^{f}(\varDelta x, \varDelta y, \varDelta z,\varDelta w,x,y,z)\), respectively.

3.2 SAT/SMT Models for the Value Transitions

In SHA-2, contradictions easily occur in the collision-generating differential characteristics. To avoid this, we use the technique proposed by Liu et al. at CRYPTO 2020 [21]: using one model for the differential characteristic and another model for the value transitions. In the above model for the differential characteristic, we have included the relations between the value and the differential characteristic if using the full model for the Boolean functions. Specially, if the full model is applied to step i, the conditions on the internal states at step \(i-1\), \(i-2\) and \(i-3\) to ensure the difference transitions have been added. Then, we can further build a model to optionally describe how to compute the internal state \(i-1\) or \(i-2\) or \(i-3\) in order to test whether these conditions can hold, which is the model for the value transitions. It is easy to build the model for the value transitions as we only need to model the modular addition and Boolean functions.

To compute \(z=x\boxplus y\), we can simply introduce a variable c with \(c[0]=0\) to denote the carry. Then, we list all possible values for the tuple (x[i], y[i], c[i], z[i]) and get the corresponding CNF for the model addition. For convenience, we denote the model for the modular addition of the value by \(\mathcal {C}_{Val}^{Add}(x,y,z,c)\).

To compute \(w=f(x,y,z)\), we can simply list all possible valid values for the tuple (x[i], y[i], z[i], w[i]) and get the corresponding CNF. For convenience, the model for the vectorial Boolean function f is denoted by \(\mathcal {C}_{Val}^{f}(x,y,z,c)\).

With the two basic models \(\mathcal {C}_{Val}^{Add}\) and \(\mathcal {C}_{val}^f\), we can simply build the model for the value transitions through the step function of SHA-2 by decomposing the step function with intermediate variables. For convenience, the models to compute \(E_i\), \(A_i\) and \(W_i\) are denoted by \(\mathcal {C}_{Val}^{E}(i)\), \(\mathcal {C}_{Val}^{A}(i)\) and \(\mathcal {C}_{Val}^{W}(i)\), respectively.

Remark 1

With the model for value transitions, we can also use it to search for conforming input pairs for some dense parts of the differential characteristic. Specially, after a differential characteristic is obtained, we first derive all the differential conditions. Then, to find the conforming input pairs for the dense part of the characteristic, we simply use the value transitions for this part and add the corresponding differential conditions on the internal states to the model. This will be frequently used in our attacks in order to search for conforming message pairs automatically. Indeed, it is not surprising that this method has been used in [21, 32].

3.3 Models for SHA-2

With the above basic models, it is easy to combine them to fully describe how the signed difference propagates through the step function of SHA-2, and how to detect contradictions by involving the value transitions. We refer the interested readers to the full version of this paper for more details [18].

4 New (SFS/FS) Collision Attacks on SHA-2

In the (FS/SFS) collision attacks on SHA-2  [6, 8, 26, 28] with the GnD tools, a crucial step is to first search for a relatively complex local collision in the message expansion, where nonzero message differences exist in the middle steps, and the differences will be cancelled in as many consecutive steps as possible in the forward and backward directions.

Basically, after determining the local collision in the message expansion, the number of attacked steps is also known. However, finding a valid attack further requires attackers to finish the following two tasks:

  1. Task 1:

    searching for a corresponding differential characteristic in \((A_i,E_i)\);

  2. Task 2:

    finding the conforming message pair to ensure the validity of the differential characteristic since contradictions easily occur.

In some cases, even though we know there may exist a good local collision in the message expansion, it may be still infeasible to find a valid attack due to the difficulty of Task 1 or Task 2. For example, the SFS collision attack can reach 39 steps of SHA-512, but could not reach 39 steps of SHA-256. Moreover, the best collision attack on SHA-256 could reach 31 steps, while it is only 27 steps for SHA-512.

4.1 The First Practical SFS Collision for 39-Step SHA-256

We note that there is a practical SFS collision attack on 39-step SHA-512 published at ASIACRYPT 2015 [6]. However, the authors did not report any attacks on 39-step SHA-256, even though SHA-256 and SHA-512 share almost the same message expansion and state update function, i.e., only with different state sizes and different rotation numbers in \(\varSigma \) and \(\sigma \). Specifically, the strategy to construct the local collision for 39-step SHA-512 should have been applicable to 39-step SHA-256, and this cannot be the bottleneck. We thus believe that the difficulty exists in either Task 1 or Task 2.

Hence, we aim to retake this challenge with the new SAT/SMT-based technique. First, we observe that in the differential characteristic for 39-step SHA-512 in [6], the local collision spans over 19 steps (steps 8−26), and the nonzero message differences exist in 9 words \((W_{8},\ldots ,W_{12}, W_{16}, W_{17}, W_{24}, W_{26})\). In addition, in (\(W_{26},W_{17},A_{18})\), there is only a one-bit difference, respectively.

In our new attack on 39-step SHA-256, we use the same strategy to construct the local collision, as shown in Fig. 2(a). Different from the ad-hoc GnD techniques [6, 8, 28], it is efficient to use our SAT/SMT-based technique to find a sparse differential characteristic by minimizing the Hamming weight of the signed differences. This is crucial to improve the uncontrolled differential probability and to make the message modification more practical. Our general procedure to search for the differential characteristic for 39-step SHA-256 is summarized below:

  1. Step 1:

    Minimize the Hamming weight of \(\varDelta W_i\). Specifically, find the minimal value of \(t_w=\sum _{i=0}^{38}{} {\textbf {H}}(\varDelta W_{i})\) such that the nonzero differences only exist in the 9 expanded message words \((W_{8},\ldots , W_{12}, W_{16}, W_{17}, W_{24}, W_{26})\). Note that the concrete message differences are not specified at this step and the only goal is to find the minimal value \(t_w\).

  2. Step 2:

    Minimize the Hamming weight of \(\varDelta A_i\). Specifically, under the conditions

    $$\begin{aligned} \forall i\in [19,38]:\ \delta A_i = & {} 0,\\ \forall i\in [23,38]:\ \delta E_i = & {} 0,\\ \forall i\in [0,38]\ {\text {and}}\ i\notin \{8,\ldots ,12,16,17,24,26\}: \delta W_i = & {} 0,\\ \sum _{i=0}^{38}{} {\textbf {H}}(\varDelta W_{i})= & {} t_w, \end{aligned}$$

    find the minimal value of \(t_A=\sum _{i=0}^{38}{} {\textbf {H}}(\varDelta A_{i})\) such that there exists a solution of a 39-step collision-generating differential characteristic, i.e., there is a solution to \((\varDelta W_i,\varDelta A_i,\varDelta E_i)\) for \(0 \le i \le 38\) to allow a 39-step attack. Still, we only aim at the minimal value \(t_A\), and do not fix \((\varDelta W_i,\varDelta A_i,\varDelta E_i)\) according to the solution at this step.

  3. Step 3:

    Minimize the Hamming weight of \(\varDelta E_i\). In addition to the conditions at Step 2, we further add the condition

    $$ \sum _{i=0}^{38}{} {\textbf {H}}(\varDelta A_{i})=t_A. $$

    Under these conditions, find and output the solution of \((\varDelta W_i,\varDelta A_i,\varDelta E_i)\) for \(0\le i\le 38\) that minimizes \(\sum _{i=0}^{38}{} {\textbf {H}}(\varDelta E_{i})\).

Following the above procedure, we successfully found a corresponding 39-step differential characteristic, as shown in Table 4. By our procedure, this differential characteristic can be kept as sparse as possible and hence it is expected to be valid.

Remark 2

Our strategy to search for a concrete 39-step differential characteristic is different from the GnD technique in [6] because we first minimize the Hamming weight of \((\varDelta W_i,\varDelta A_i)\) and then search the solution under such constraints. However, there is no such a minimization procedure when searching for the differential characteristic in 39-step SHA-512 in [6]. Without this strategy, the differential characteristic may be dense and there is a high chance that it is invalid, which may somehow explain why the technique in [6] failed for 39-step SHA-256.

Message Modification. As the differential characteristic is still relatively dense, we could not ensure that there must exist a conforming message pair. To verify this, we first extract all the constraints on \((A_i,E_i)_{-4\le i\le 22}\) and \((W_i)_{0\le i\le 38}\) for this differential characteristic. Then add these constraints to the SAT/SMT model for the value transitions of SHA-256, and solve the model to find a solution of these variables. We succeed in finding a practical SFS colliding message pair for 39-step SHA-256 in 120 s with 26 threads, as shown in Table 5.

Fig. 2.
figure 2

(a) represent the shape of the 39-step differential SHA-256 and (b) represent the shape of the differential characteristic for 31-step SHA-256

4.2 Improved Collision Attacks on 31-Step SHA-256

The best existing collision attack on SHA-256 reaches 31 steps, which was published at EUROCRYPT 2013 [28]. The main idea is to use a two-block method to convert a SFS collision into a collision by utilizing the available degrees of freedom in the first few message words. To achieve this purpose, the first step is to find a suitable differential characteristic for 31-step SHA-256. In [28], this 31-step differential characteristic relies on a properly constructed local collision in the message expansion, which spans over 14 steps (steps 5−18). Specifically, the nonzero message differences only exist in 7 expanded message words

$$ (W_5, W_6, W_7, W_8, W_9, W_{16}, W_{18}). $$

Moreover, there are no conditions on the first 5 expanded message words \((W_i)_{0\le i\le 4}\) and hence they can be freely chosen to efficiently convert a SFS collision into a collision. The shape of the 31-step differential characteristic is shown in Fig. 2(b).

Table 4. The differential characteristic for 39 steps of SHA-256
Table 5. The SFS colliding message pair for 39 steps of SHA-256

The method in [28] to convert SFS collisions into collisions is described below:

  1. Step 1:

    Find \(2^{\ell }\) solutions of \((A_i)_{-3\le i\le 12}\), \((E_i)_{1\le i\le 12}\) and \((W_i)_{5\le i\le 12}\) that satisfy the differential conditions on steps 5−12. Store them in a table denoted by \(\texttt {TAB}_1\).

  2. Step 2:

    Compute \(2^{96-\ell }\) arbitrary first message blocks and get \(2^{96-\ell }\) chaining inputs \((A_{-4},\ldots ,A_{-1})\) and \((E_{-4},\ldots ,E_{-1})\). Check \(\texttt {TAB}_1\) and find a match in \((A_{-3},A_{-2},A_{-1})\). Then, \((W_i)_{0\le i\le 4}\) and \(E_0\) are all determined for this match.

  3. Step 3:

    At this step, \((W_i)_{0\le i\le 12}\) have been fixed. Use the degrees of freedom in \((W_{13},W_{14},W_{15})\) to fulfill the remaining uncontrolled conditions on \((E_{13},E_{14},E_{15},W_{16},W_{18})\). If it fails, go to Step 2.

Supposing Step 3 succeeds with probability \(2^{-\gamma }\), the time complexity for this two-block method to find a collision is \(2^{96-\ell +\gamma }+2^{\ell }\cdot T_{\texttt {tool}}\), where \(T_{\texttt {tool}}\) denotes the time to find a solution of \((A_i)_{-3\le i\le 12}\), \((E_i)_{1\le i\le 12}\) and \((W_i)_{5\le i\le 12}\) at Step 1. The memory complexity is \(2^{\ell }\). In [28], \(\ell \approx 34\), \(\gamma \approx 3.5\) and \(T_{\texttt {tool}}\) is negligible. Hence the time complexity is estimated as \(2^{65.5}\) and the memory complexity is \(2^{34}\).

According to the above analysis, it is clear that \(\ell \) and \(\gamma \) should be improved to get better attacks. Moreover, the best time-memory trade-off cannot be achieved with their 31-step differential characteristic [28]. Note that the maximal value of \(\ell \) is dominated by the number of differential conditions on steps 5−12 and hence we can expect a relatively larger \(\ell \) with a sparser differential characteristic. Therefore, we are interested whether it is possible to find a new sparser differential characteristic with our tool that can help achieve the optimal time-memory trade-off, i.e., with time and memory complexity close to \(2^{96/2}=2^{48}\). The overall searching procedure is stated as follows:

  1. 1.

    Minimize the Hamming weight of \(\varDelta W_i\). Specifically, find the minimal value of \(t_w=\sum _{i=0}^{30}{} {\textbf {H}}(\varDelta W_{i})\) while keeping the minimal \({\textbf {H}}(\varDelta W_{16})\) and the minimal \({\textbf {H}}(\varDelta W_{18})\) such that the nonzero differences only exist in the 7 expanded message words \((W_5, W_6, W_7, W_8, W_9, W_{16}, W_{18})\). Note that the concrete message differences are not specified at this step.

  2. 2.

    Minimize the Hamming weight of \(\varDelta A_i\). Specifically, under the conditions

    $$\begin{aligned} \forall i\in [11,30]:\ \delta A_i = & {} 0,\\ \forall i\in [15,30]:\ \delta E_i = & {} 0,\\ \forall i\in [0,30]\ {\text {and}}\ i\notin \{5,\ldots ,9,16,18\}: \delta W_i = & {} 0,\\ \sum _{i=0}^{30}{} {\textbf {H}}(\varDelta W_{i})= & {} t_w, \end{aligned}$$

    find the minimal value of \(t_A=\sum _{i=0}^{30}{} {\textbf {H}}(\varDelta A_{i})\) such that there is a solution to \((\varDelta W_i,\varDelta A_i,\varDelta E_i)\) for \(0 \le i \le 30\) to allow a 31-step attack. Still, we only aim at the minimal value \(t_A\), and do not fix \((\varDelta W_i,\varDelta A_i,\varDelta E_i)\) according to the solution at this step.

  3. 3.

    Minimize the Hamming weight of \(\varDelta E_i\). In addition to the conditions at Step 2, we further add the condition

    $$ \sum _{i=0}^{30}{} {\textbf {H}}(\varDelta A_{i})=t_A. $$

    Under these conditions, find and output the solution minimizing \(\sum _{i=0}^{30}{} {\textbf {H}}(\varDelta E_{i})\) to allow a 31-step attack.

As already mentioned in our SAT/SMT models, to further detect the contradictions caused by the complex relationship between \((A_i,E_i,W_i)\), we sometimes add the value transitions at certain steps to ensure its validity. In our model for the 31-step differential characteristic, this strategy is applied to \((A_i, E_i, W_i)_{7\le i\le 10}\). Without this strategy, we found that the obtained differential characteristic was indeed invalidFootnote 1. Our new 31-step differential characteristic is shown in Table 6.

Estimating \(\boldsymbol{\ell }\) and \(\boldsymbol{\gamma }\). We use a dedicated method to find valid solutions of \((A_i)_{-3\le i\le 12}\), \((E_i)_{1\le i\le 12}\) and \((W_i)_{5\le i\le 12}\) such that \(\ell \) can be better estimated. First, use the model for the value transitions to find a solution of \((A_i)_{1\le i\le 12}\), \((E_i)_{5\le i\le 12}\) and \((W_i)_{9\le i\le 12}\) that satisfy the differential conditions on steps 5−12. For simplicity, this solution is called a starting point for 31-step SHA-256. Due to

$$\begin{aligned} A_i = E_i \boxminus A_{i-4} \boxplus \varSigma _0(A_{i-1}) \boxplus \textrm{MAJ}(A_{i-1}, A_{i-2}, A_{i-3}), \end{aligned}$$
(2)

(\(A_{-3}\), \(A_{-2}\), \(A_{-1}\), \(A_{0}\)) will then depend on (\(E_1\), \(E_2\), \(E_3\), \(E_4\)) for this starting point. Moreover, according to

$$\begin{aligned} E_i = A_{i-4} \boxplus E_{i-4} \boxplus \varSigma _1(E_{i-1}) \boxplus \textrm{IF}(E_{i-1}, E_{i-2}, E_{i-3}) \boxplus K_i \boxplus W_i, \end{aligned}$$
(3)

(\(E_1\), \(E_2\), \(E_3\), \(E_4\)) will depend on (\(W_5\), \(W_6\), \(W_7\), \(W_8\)) for this starting point. By analyzing the conditions on (\(W_5\), \(W_6\), \(W_7\), \(W_8\)) to ensure the local collision in the message expansion, we find that there are in total \(2^{14}\), \(2^{23}\), \(2^{27}\) and \(2^{25}\) possible values of \(W_5\), \(W_6\), \(W_7\) and \(W_8\), respectively. Since there are no conditions on \((E_1, E_2)\) or (\(A_{-3}\), \(A_{-2}\), \(A_{-1}\), \(A_{0}\)) for this differential characteristic to hold, we only need to check how many \((W_7, W_8)\) are left to ensure the conditions on \((E_3, E_4)\) for this starting point. Experiments suggest that there are \(2^{11}\) valid \((W_7,W_8)\) left. Hence, based on this starting point, we can expect to generate \(2^{14+23+11}=2^{48}\) valid solutions of \((A_i)_{-3\le i\le 12}\), \((E_i)_{1\le i\le 12}\) and \((W_i)_{5\le i\le 12}\). For \(\gamma \), since we do not have enough degrees of freedom in \((W_{13}, W_{14}, W_{15})\), we found that \(\gamma \approx 1.3\) by 100 tests. If we can generate \(2^{\ell _1}\) starting points, then we have \(2^{\ell }=2^{\ell _1+48}\). Hence, the time complexity of the new collision attack on 31-step SHA-256 is estimated as

$$ 2^{96-48-\ell _1+1.3} + 2^{48+\ell _1} + 2^{\ell _1}\cdot T_{\texttt {model}}, $$

where \(T_{\texttt {model}} \approx 2^{31.7}\) denotes the time to generate a starting point and is always negligible. With \(\ell _1=0\), i.e., only using one starting point, the time complexity is about \(2^{49.8}\) and the memory complexity is \(2^{48}\). With this improved attack, we are much closer to a practical collision attack on 31-step SHA-256 and the bottleneck is the memory consumption. A possible practical implementation is to use less memory at the cost of increased time complexity.

Table 6. The differential characteristic for 31 steps of SHA-256

4.3 The First Collision Attack on 31-Step SHA-512

While the best existing collision attack on SHA-256 reaches 31 steps, the best collision attack on SHA-512 could only reach up to 27 steps, which was reported at ASIACRYPT 2015 [6]. The authors also stated in [6] that they could not find better collision attacks on SHA-512 because they could not find a suitable differential characteristic with their tools. In this part, we show how to overcome this obstacle.

Our practical SFS collision attack on 39-step SHA-256 benefits much from the practical SFS collision attack on 39-step SHA-512 due to their similarity. Hence, we feel interested to know whether it is possible to find a suitable differential characteristic for 31-step SHA-512 based on the collision attack on 31-step SHA-256  [28] with our new tool.

Specifically, similar to the 31-step attack on SHA-256, the nonzero message differences are injected in

$$ (W_5, W_6, W_7, W_8, W_9, W_{16}, W_{18}), $$

and the local collision in the message expansion spans over 14 steps (steps 5−28), as shown in Fig. 2(b). Similar to the collision attack on 31-step SHA-256, we first find SFS collisions and then convert them into collisions with the two-block method. The general procedure to convert SFS collisions into collisions is essentially the same and we refer the readers to the above improved attack on 31-step SHA-256.

The most challenging step to achieve the collision attack on 31-step SHA-512 is how to find a valid differential characteristic. In what follows, we describe how to use our tool to solve this problem.

  1. Step 1:

    Find a solution of \((\varDelta W_i)_{0\le i\le 30}\) with the minimal \(\sum _{i=0}^{30}{} {\textbf {H}}(\varDelta W_{i})\), while keeping the minimal \({\textbf {H}}(\varDelta W_{16})\) and the minimal \({\textbf {H}}(\varDelta W_{18})\), which allows a local collision in the message expansion.

  2. Step 2:

    With the fixed solution of \((\varDelta W_i)_{0\le i\le 30}\) obtained at Step 1, find a valid solution of \((\varDelta A_i,\varDelta E_i)_{0 \le i \le 30}\), which follows the shape of the 31-step differential characteristic shown in Fig. 2(b). Here, set a threshold to \(\sum _{i=0}^{30}{} {\textbf {H}}(\varDelta A_{i})\). Specifically, choose an integer tr and add the constraint

    $$ \sum _{i=0}^{30}{} {\textbf {H}}(\varDelta A_{i}) \le tr $$

    to the model. If the solver cannot output a solution in a reasonable time, e.g., 72 h, increase tr until a valid solution of \((\varDelta A_i,\varDelta E_i)_{0\le i\le 30}\) is found. Keep the solution of \((\varDelta A_i)_{0\le i\le 30}\).

  3. Step 3:

    With the fixed solution of \((\varDelta A_i,\varDelta W_i)_{0\le i\le 30}\), find a valid solution of \((\varDelta E_i)_{0\le i\le 30}\) with the minimal \(\sum _{i=0}^{30}{} {\textbf {H}}(\varDelta E_{i})\), which allows a 31-step collision attack.

It is found that the obtained 31-step differential characteristic is invalid. Therefore, we propose to use the following method to correct this obtained solution.

  1. Step 1:

    Set \((\varDelta E_i)_{5\le i\le 7}\) as unknown variables. For the remaining \((\varDelta E_i)_{0\le i\le 30}\) where \(i\notin \{5,6,7\}\), keep them the same as those in the obtained solution. For \((\varDelta A_i)_{0\le i\le 30}\) and \((\varDelta W_i)_{0\le i\le 30}\), they are also kept the same as those in the obtained solution.

  2. Step 2:

    Add the constraints describing the value transitions for \((A_i,E_i,W_i)_{7\le i\le 12}\) to the model.

In summary, we utilize the degrees of freedom in \((\varDelta A_i,\varDelta E_i)_{5\le i\le 7}\) and the model for value transitions to correct an invalid 31-step differential characteristic. In our search, the corresponding 31-step differential characteristic is shown in Table 7.

Complexity Evaluation. As already mentioned, the only challenge to achieve the collision attack on 31-step SHA-512 is to find a suitable differential characteristic. Once it is found, the two-block method for 31-step SHA-256 can be directly applied. For consistency, we use the same notation, i.e., use \((\ell ,\gamma ,\ell _1)\) to describe the time complexity and memory complexity as in the above collision attack on 31-step SHA-256. For our 31-step differential characteristic, there are in total \(2^{36}\), \(2^{26}\), \(2^{25}\) and \(2^{43}\) possible values for \(W_5\), \(W_6\), \(W_7\) and \(W_8\), respectively. For each starting point, i.e., the solution of \((A_i)_{1\le i\le 12}\), \((E_i)_{5\le i\le 12}\) and \((W_i)_{9\le i\le 12}\), we have experimentally found that there are on average \(2^{15.3}\) possible \((W_7,W_8)\) that can make the conditions on \((E_3,E_4)\) hold. Therefore, for each starting point, we can generate \(2^{36+26+15.3}=2^{77.3}\) candidate solutions of \((A_i)_{-3\le i\le 12}\), \((E_i)_{1\le i\le 12}\) and \((W_i)_{5\le i\le 12}\). For \(2^{\ell _1}\) starting points, we thus can expect to generate \(2^{\ell }=2^{\ell _1+77.3}\) such many solutions. For \(\gamma \), similarly, we found \(\gamma \approx 0.9\) according to 100 experiments. Since the time complexity to generate a starting point is negligible, the whole time complexity is estimated as

$$ 2^{64\times 3-(\ell _1+77.3)+0.9} + 2^{\ell _1+77.3} $$

and the memory complexity is \(2^{\ell _1+77.3}\). With \(\ell _1=0\), i.e., only one starting point, the time and memory complexity are \(2^{115.6}\) and \(2^{77.3}\), respectively.

Table 7. The differential characteristic for 31-step SHA-512

4.4 The Practical Collision Attack on 28-Step SHA-512

Similar to the 28-step attack on SHA-256  [28], the nonzero message differences are injected in

$$ (W_8, W_9, W_{13}, W_{16}, W_{18}), $$

and the local collision in the message expansion spans over 11 steps (steps 8−18), resulting in a collision on 28-step SHA-512.

The most challenging step to achieve the collision attack on 28-step SHA-512 is how to find a valid differential characteristic. In what follows, we describe how to use our tool to solve this problem.

  1. Step 1:

    Find a solution of \((\varDelta W_i)_{0\le i\le 27}\) with the minimal \(\sum _{i=0}^{27}{} {\textbf {H}}(\varDelta W_{i})\) while keeping the minimal \({\textbf {H}}(\varDelta W_{16})\) and the minimal \({\textbf {H}}(\varDelta W_{18})\), which allows a local collision in the message expansion.

  2. Step 2:

    Find the suitable \(\varDelta E_i\). With the fixed solution of \((\varDelta W_i)_{0\le i\le 27}\) obtained at Step 1, find a valid solution of \((\varDelta A_i,\varDelta E_i)_{0 \le i \le 27}\).

To improve the efficiency of the message modification, we have tried three strategies for Step 2, as detailed below:

  1. Strategy 1:

    First, with the fixed solution of \((\varDelta W_i)_{0\le i\le 27}\), find a valid solution of \((\varDelta A_i, \varDelta E_i)_{0 \le i \le 27}\), and we minimize \(\sum _{i=0}^{27}{} {\textbf {H}}(\varDelta A_{i})\).

    Then, with the fixed solution of \((\varDelta W_i, \varDelta A_i)_{0\le i\le 27}\), find a valid solution of \((\varDelta E_i)_{0 \le i \le 27}\) with the minimal \(\sum _{i=0}^{27}{} {\textbf {H}}(\varDelta E_{i})\).

  2. Strategy 2:

    With the fixed solution of \((\varDelta W_i)_{0\le i\le 27}\), find a valid solution of \((\varDelta A_i, \varDelta E_i)_{0 \le i \le 27}\), and we minimize \(\sum _{i=0}^{27}{} {\textbf {H}}(\varDelta E_{i})\).

  3. Strategy 3:

    With the fixed solution of \((\varDelta W_i)_{0\le i\le 27}\), find a valid solution of \((\varDelta A_i, \varDelta E_i)_{0 \le i \le 27}\), and we minimize \(\sum _{i=11}^{27}{} {\textbf {H}}(\varDelta E_{i})\).

After testing, it is found that Strategy 3 is more suitable for message modifications. However, such a 28-step differential characteristic is invalid. Similar to the method to correct the SHA-512 31-step differential characteristic, we also use the same technique to correct this invalid 28-step differential characteristic.

  1. Step 1:

    Set \((\varDelta E_i)_{8\le i\le 10}\) as unknown variables. For the remaining \((\varDelta E_i)_{0\le i\le 27}\) where \(i\notin \{8,9,10\}\), keep them the same as those in the obtained solution. For \((\varDelta A_i)_{0\le i\le 27}\) and \((\varDelta W_i)_{0\le i\le 27}\), they are also kept the same as those in the obtained solution.

  2. Step 2:

    Add the constraints describing the value transitions for \((A_i,E_i,W_i)_{10\le i\le 12}\) to the model.

With this method, we eventually found a valid 28-step differential characteristic, as shown in Table 8.

Table 8. The differential characteristic for 28-step SHA-512

Message Modification. We use a different message modification technique than in [28]. In our message modification technique, we first determine all expanded message words and state variables in steps 8−12. Since the first 8 message words can be (almost) freely chosen, it is easy to connect the \((A_i, E_i)_{{-4}\le i \le {-1}}\) and \((A_i, E_i)_{8\le i \le 12}\) by using \((W_i)_{0\le i \le 7}\). Currently, \((A_i, E_i)_{{-4}\le i\le 12}\) and \((W_i)_{0\le i\le 12}\) has been determined. Then, the degree of freedom in message words \(W_{13}-W_{15}\) can be used to fulfill the conditions on \(E_{13}-E_{15}\) and \((W_{16}, W_{18})\). With this method, the cost to find the colliding message pair is almost negligible. The colliding message pair is shown in Table 9.

Table 9. The colliding message pair for 28 steps of SHA-512

4.5 The First Practical FS Collision for 40-Step SHA-224

In SHA-224, the last one output word \((E_{60} + E_{-4})\) was truncated. Therefore, similar to [6], we inject differences in \(E_{-4}\) to mount a FS collision attack. The best practical FS collision attack on SHA-224 was presented in [6] and it reaches 39 steps. With our tool, we could find a practical FS collision for 40-step SHA-224 for the first time. Specifically, we inject message differences at 10 expanded words

$$ (W_0, W_9, W_{10}, W_{11}, W_{12}, W_{13}, W_{17}, W_{18}, W_{25}, W_{27}), $$

and then search for the corresponding 40-step differential characteristic. The searching strategy is almost the same as in our attack on 39-step SHA-256.

The 40-step differential characteristic and the conforming message pair are shown in Tables 10 and 11, respectively.

Table 10. The differential characteristic for 40 steps of SHA-224
Table 11. The FS colliding message pair for 40 steps of SHA-224

5 Summary and Future Work

Although there was major progress on collision attacks on SHA-2 between 2011 and 2015, which essentially benefited from the development of the GnD technique to search for SHA-2 characteristics, no other progress has been made for nearly 8 years. One reason we believe is that the GnD technique has reached the bottleneck. In addition, the code for this GnD technique is not open source, which may further increase the difficulty to follow these works. Given the importance of SHA-2, there is no doubt that advancing the understanding of its collision resistance is always of practical interest.

By this work, we report for the first time that it is possible to overcome the obstacle to find SHA-2 characteristics with a SAT/SMT-based method, which is supported by several new improved attacks on the SHA-2 family. As can be observed, these new attacks highly depend on our SAT/SMT-based tool and how to use it in a dedicated way. Especially, we could find useful SHA-2 characteristics that could not be found with the GnD technique.

Through this work, we also expect that there could be more efforts to further improve this SAT/SMT-based method in the future, and that more and more researchers can easily perform analysis of SHA-2 with our tool.