Keywords

1 Introduction

Many symmetric key primitives are proposed with the ARX design strategy which only uses three operations: Additions (\(\boxplus \)), Rotations (\(\lll \)) and XORs (\(\oplus \)). These operations are very simple and efficient in software implementation, but interactively provide non-linearity. The ARX structure can be found in a large number of symmetric key designs, including hash functions BLAKE [2] and Skein [9], which are two of the five SHA-3 finalists, stream ciphers such as Salsa20 [5] and ChaCha [4], block ciphers such as TEA [27], XTEA [18], HIGHT [12] and SPECK [3], and MAC algorithm Chaskey [16]. Even though the ARX structure receives a considerable amount of attention due to its elegance and efficiency, it remains a difficult problem to evaluate its security margin against known attacking techniques.

Differential cryptanalysis [6] and linear cryptanalysis [15] are two main techniques used in the analysis of symmetric primitives, including ARX designs. Differential characteristics (resp. linear trails) with optimal probability (resp. correlation) can lead to efficient attacks with complexity better than the brute force searching. Hence the resistance against differential cryptanalysis and linear cryptanalysis is a crucial feature to consider for both designers and attackers. Among the methods and algorithms proposed in finding good differential characteristics and linear trails, automatic searching is a popular and efficient way. Several automatic toolkits dedicated to the searching of differential characteristics in ARX are proposed in the literature [7, 14]. Comparing to the significant efforts which have been dedicated to the automatic search of differential characteristics, the searching tool of linear trails in ARX designs fell behind. The first paper on this topic as far as we know is presented by Yao et al. [28], where an algorithm based on branch and bound is used to find optimal (round-reduced) linear trails in SPECK32, and short linear trails of larger versions of SPECK.

Our motivation is to model the problem of searching optimal linear trails in an ARX structure as a boolean satisfiability problem [24]. The boolean satisfiability problem is widely used to determine whether the boolean variables in a given set of boolean conditions have valid assignments such that the conditions evaluate to TRUE. Specifically, in order to construct linear trails with nonzero correlation, the idea is to explore the bit-level conditions on the bits of the masks when passing through every operation of an ARX structure, render them into boolean satisfiability language, and call solvers to obtain valid linear trails with certain correlations. Our work can be applied to general ARX designs and has good performance in finding linear trails with best correlation for round-reduced primitives. Therefore it could provide a rigorous security evaluation for some ARX primitives against linear cryptanalysis.

Table 1. The number of covered rounds in finding optimal linear trails for SPECK family and Chaskey
Full size table

In this paper, our method is applied to the linear cryptanalysis of round-reduced SPECK family and Chaskey. Table 1 gives an overview of the number of rounds for which optimal linear trails are found in SPECK and Chaskey. Note that there is no previous research on finding optimal linear trails in round-reduced Chaskey.

This paper is organised as follows. In Sect. 2, we recall linear cryptanalysis and the boolean satisfiability problem. We study the propagation of bits in masks through operations of the ARX structure and transform them using boolean satisfiability language such that they can be solved automatically in Sect. 3. In Sect. 4, we apply the method to block cipher SPECK and MAC algorithm Chaskey, and find linear hulls for round-reduced SPECK32. Finally, we conclude in Sect. 5.

2 Preliminaries

We denote an n-bit boolean vector by \(x =(x_{n-1}, \cdots , x_1, x_0)\), where \(x_0\) is the least significant bit. For two n-bit boolean vectors x and y, the inner product is \(x\cdot y = \bigoplus _{i=0}^{n-1}x_iy_i\). The partial order \(\preccurlyeq \) is defined by \(x \preccurlyeq y \Leftrightarrow x_i \le y_i, \forall i \in \{0, \cdots , n-1 \}\). The characteristic function \(1_{x \preccurlyeq y}\) is defined as

$$\begin{aligned} 1_{x \preccurlyeq y} = {\left\{ \begin{array}{ll} 1, &{} \text{ if } x \preccurlyeq y, \\ 0, &{} \text{ otherwise. } \end{array}\right. } \end{aligned}$$

Logical operations OR, AND, NOT, XOR are referred to as \(\vee , \wedge , \lnot , \oplus \), respectively. All linear masks are hexadecimal, and we omit the 0x symbol.

2.1 Linear Cryptanalysis

Linear cryptanalysis investigates linear relations among the parities of plaintext, ciphertext and the secret key. Let \(f:\mathbb {F}_{2^n}\rightarrow \mathbb {F}_{2^m}\) be a vectorial boolean function. Assume that masks for input x and output f(x) are \(\varGamma _{in}\) and \(\varGamma _{out}\). The correlation of the linear approximation is defined as

$$\begin{aligned} C(\varGamma _{in}, \varGamma _{out}) = 2 \cdot \Pr (\varGamma _{in} \cdot x \oplus \varGamma _{out} \cdot f(x) = 0) -1. \end{aligned}$$

Equivalently, the correlation can also be written as a Walsh transformation,

$$\begin{aligned} C(\varGamma _{in}, \varGamma _{out}) = 2^{-n} \sum \limits _{x \in \text {GF}(2^n)} (-1)^{\varGamma _{in} \cdot x \oplus \varGamma _{out} \cdot f(x)}. \end{aligned}$$

Let \(g = f_{r-1} \circ \cdots \circ f_1 \circ f_0\) be an iterated permutation which is the composition of r round functions \(f_i\). Linear approximations \((\gamma _i,\gamma _{i+1})\) of a single round \(f_i\) can be concatenated into a linear trail \((\gamma _0, \gamma _1, \cdots , \gamma _r)\) of g.

Lemma 1

([8]). Let \((\gamma _0, \gamma _1, \cdots , \gamma _r)\) be a linear trail of an iterated permutation. Then the correlation of the linear trail can be calculated as

$$\begin{aligned} C(\gamma _0, \gamma _r) = \prod \limits _{i=0}^{r-1} C(\gamma _i, \gamma _{i+1}) \end{aligned}$$

We call a linear trail over a (round-reduced) cipher with maximum correlation amplitude an optimal linear trail.

A linear approximation \((\varGamma _{in}, \varGamma _{out})\) of a block cipher is called a linear hull [19], which contains all linear trails with input mask \(\varGamma _{in}\) and \(\varGamma _{out}\). The potential (averaged linear probability over the key space \(\mathcal {K}\)) of a linear hull is defined as

$$\begin{aligned} ALP(\varGamma _{in}, \varGamma _{out}) = \frac{1}{|\mathcal {K}|}\sum \limits _{k\in \mathcal {K}} C(\varGamma _{in}, \varGamma _{out})^2, \end{aligned}$$

and gives the expected value of the data complexity of a linear attack.

2.2 Description of SPECK and Chaskey

The lightweight block cipher SPECK family was designed by the NSA in 2013. The block sizes are defined as 2n with \(n\in \{16,24,32,48,64\}\), and key size as mn with \(m \in \{2,3,4\}\) depending on n. The instances corresponding to a block size 2n and key size mn are denoted by SPECK2n / mn. Since we do not explore the key schedule in this paper, the instances of SPECK will simply be referred to as SPECK2n. The round function of SPECK with inputs x and y, a round key k is defined as:

$$F_k(x, y)=(f_k(x, y),f_k(x, y)\oplus (y\lll \beta ))$$

where \(f_k(\cdot ,\cdot )\) is defined as \(f_k(x, y)=((x\ggg \alpha )\boxplus y)\oplus k\), the rotation offset \((\alpha , \beta )\) is (7, 2) for SPECK32, and (8, 3) for the larger instances. One round of SPECK is depicted in Fig. 1. For more details, we refer to the design [3].

Fig. 1.
figure 1

Round function of SPECK

Full size image

Chaskey is a permutation-based MAC algorithm presented by Mouha et al. in 2014. The underlying permutation is an Even-Mansour block cipher with the ARX structure. The block size is 128-bits, which is separated into four 32-bit words. The design of Chaskey is inspired by Siphash [1], and has a structure similar to the block cipher Threefish [9]. The total number of rounds is 8, and there are four modular addition operations and some rotation operations in each round. The round function of the Chaskey permutation is showed in Fig. 2.

Fig. 2.
figure 2

Round function of Chaskey

Full size image

2.3 Boolean Satisfiability Problem

The boolean satisfiability problem is often called SAT. It considers whether there is a valid assignment to boolean variables satisfying a given set of boolean clauses. A Boolean clause consists of boolean variables (called literals), operators AND, OR, NOT, and parentheses. For example, the clause x AND (NOT y) is satisfiable since \(x=\) TRUE, \(y=\) FALSE is a valid assignment.

The SAT problem is NP-complete. However for most practical situations, the solutions can be found in reasonable time. There are a large number of heuristic SAT solvers, and all of them accept DIMACS CNF (Conjunctive Normal Form) files as the standard input format. In CNF format, all clauses are literals with logical operation OR and NOT, while the clauses are concatenated by AND. The output is either satisfiable or unsatisfiable, when satisfiable, the solver can also return a valid assignment to all literals. More specifically, SAT solvers will start searching with an initial assignment, then calculate the number of conflicting clauses, based on which the search tree of the SAT solver decides the next step of searching to eliminate possible conflicts until a valid or no solution is found. It is believed that, for cryptographic problems, the time for unsatisfiable decision is much longer than that of satisfiable, because the search is roughly brute-force before returning the decision of unsatisfiable [23].

In some applications, we also consider arithmetic operations, for instance, the arithmetic sum of boolean variables, which leads to the satisfiability modulo theory (SMT) problem. SMT has certain similarity with the 0-1 integer programming problem or mixed integer linear programming (MILP), while the underlying ideas to solve them differ significantly. For the MILP problem, linear programming solvers first regard the problem as a general linear programming problem in real numbers, then by Branch and Cut, they carefully rule out illegal branches and then limit the solution to 0-1 integers. SMT solvers try to translate the problem to SAT, then solve it within a binary field. Due to the different methodologies of solvers, the performances depend heavily on the background and structure of the underlying problem.

3 Translating Clauses for Modular Addition

The behaviours of masks through linear operations are easy to describe, since the correlation is either zero or \(\pm 1\). For example, with input masks \(\varGamma _a, \varGamma _b\) and output mask \(\varGamma _c\), the condition for being a linear approximation of XOR with nonzero correlation is \(\varGamma _a = \varGamma _b = \varGamma _c\). The condition for being a nontrivial linear approximation of three-fork branching is \(\varGamma _a \oplus \varGamma _b \oplus \varGamma _c = 0\), and the conditions for rotational circular shift is the equality on each corresponding bit of masks.

However for the nonlinear operation modular addition, it is necessary to have a better understanding on the nature of addition modulo \(2^n\).

3.1 Propagation of Masks Through Modular Addition

The milestone works on linear correlation of modular addition are by Wallén et al. [20, 26]. They propose a recursive method to calculate the correlation of a linear approximation in addition modulo \(2^n\) efficiently by an automaton. The only drawback of the recursive automaton is that it is very difficult to translate the expression into bit-level linear relations in masks, i.e. every bit is dependent on all previous bits, which leads to a huge number of complex constraints. Therefore, even though there are several papers discussing the heuristic search methods of differentials, no previous result is on finding linear trails in ARX ciphers with SAT theory.

In order to avoid the recursive expression, an explicit result on calculating the correlation of linear approximations in modular addition is proven by Schulte-Geers [21]. Despite the recursive property of the carry, modular addition is CCZ-equivalent to a vectorial quadratic boolean function. A more natural formula to calculate the correlation in addition modulo \(2^n\) is given in Proposition 1.

Proposition 1

([21]). Let z be an n-bit vector satisfying \(z \oplus (z \gg 1) \oplus ((u\oplus v \oplus w) \gg 1) = 0\text {, } z_{n-1} = 0\), where u is the output mask, v, w are the input masks in a linear approximation of addition modulo \(2^n\). Then the correlation of the linear approximation is given by

$$\begin{aligned} cor(u,v,w) = 1_{u\oplus v\preccurlyeq z}1_{u\oplus w\preccurlyeq z}(-1)^{(u\oplus w)\cdot (u\oplus v)}2^{-|z|}. \end{aligned}$$

Comparing to a recursive algorithm, the Hamming weight of z determines the amplitude of the correlation directly, while each bit of z can be explicitly calculated from input and output masks. Next, we will mainly focus on the absolute value of the correlation.

From Proposition 1, to obtain a valid linear approximation, the input masks v, w and output mask u through addition modulo \(2^n\) need to follow the constraints below.

$$\begin{aligned} \begin{aligned}&z_{n-1} = 0, \\&z_{n-2} = u_{n-1} \oplus v_{n-1} \oplus w_{n-1}, \\&z_j = z_{j+1} \oplus u_{j+1} \oplus v_{j+1} \oplus w_{j+1},\\&z_i \ge u_i \oplus v_i, \\&z_i \ge u_i \oplus w_i,\\ \end{aligned} \end{aligned}$$
(1)

where \(0\le i \le n-1\), \(0\le j \le n-3\).

3.2 From Linear Relations Towards SATisfiability

When considering problems in cryptanalysis, XOR is one of the most common operations. If we translate XOR clauses into CNF, a sentence \(a \oplus b\) becomes two clauses \((\lnot a \vee \lnot b)\wedge (a \vee b)\). In general, the XOR of n boolean variables will give \(2^{n-1}\) clauses in CNF format. Even if the expressions are logically equivalent, the underlying structure of the XOR equation system is missing in terms of the CNF format. A system of XOR equations is in fact a linear equation system on \(\text {GF}(2)\), therefore, it can be solved by Gaussian elimination in time \(O(n^3)\), where n is the number of variables. In many circumstances, Gaussian elimination is much more efficient than translating XOR into operations \(\vee \) and \(\wedge \). One SAT solver called Cryptominisat4 [23] is specially designed to be compatible with XOR operations and solve the XOR equation system by Gaussian elimination.

The remaining constraints in Eq. (1) are inequalities. Consider the inequality in boolean variables, \(z \ge a \oplus b\). It is equivalent to if \(a\oplus b\) , then z, which is logically consistent with \((\lnot a \vee b \vee z)\wedge (a \vee \lnot b \vee z)\).

Recall that in order to find good linear trails with large correlation values, we need to minimize the Hamming weight of z. By the piling-up lemma, the sum of z in every round \(\sum _{i,r}z_i^r\) is the objective function to be minimized. Addition over integers is an unnatural operation in SAT language, which is not easy to describe with only OR and AND. In SAT/SMT theory, Constraints like objective function \(\sum _i x_i \le k\), where \(k\ge 1\), are called cardinality constraints, which belongs to an even larger class called Pseudo Boolean constraints (PB-constraints). There are two directions to handle the cardinality constraints: one is to develop new PB-solvers dedicated to cardinality constraints, the other one is to convert cardinality constraints into CNF format, which is what we adopt in this paper.

One plain method is enumerating all the possible combinations of no more than k out of n variables being true, i.e. the conjunction of \(n \atopwithdelims (){k+1}\) clauses \(\bigwedge _{i_1,..., i_{k+1}} (\lnot x_{i_1} \vee \cdots \vee \lnot x_{i_{k+1}})\). However it is not applicable when n, k are large. Throughout the literature, a large number of methods to encode the cardinality constraints are presented. The basic idea is to add new variables to reduce the number of constraints. Since it is a tradeoff between the number of new variables needed and the number of clauses, while the sizes of variables and clauses both have a significant influence on the efficiency of solving, it is critical to find a good encoding method. In this paper, we use sequential encoding method [22], as shown in Eq. (2). For \(\sum _i x_i \le k\), new dummy variables \(\{u_{i,j}\}_{1\le i \le n-1, 1\le j \le k}\) are introduced to return contradiction when the cardinality is larger than k.

$$\begin{aligned} {\left\{ \begin{array}{ll} \begin{aligned} &{}(\lnot x_1 \vee u_{1,1}) \wedge ( \lnot u_{1,j}),\\ &{}(\lnot x_i \vee u_{i,1}) \wedge (\lnot u_{i-1,1} \vee u_{i,1}) \wedge (\lnot x_i \vee \lnot u_{i-1,j-1} \vee u_{i,j}) \\ &{}\qquad \quad \wedge (\lnot u_{i-1,j} \vee u_{i,j}) \wedge (\lnot x_i \vee \lnot u_{i-1,k}), \\ &{}\lnot x_n \vee \lnot u_{n-1,k}, \end{aligned} \end{array}\right. } \end{aligned}$$
(2)

where \(1< j \le k, 1< i < n\). The sequential encoding of cardinality constraints is one of the best methods, with relatively small amount of additional variables and a great reduction of clauses.

When \(k=0\), all variables are zero, which can be translated to n clauses as \(\lnot x_{i}\text {, } 1\le i \le n\).

Fig. 3.
figure 3

Notation of masks in round function of SPECK32

Full size image

4 Applications

4.1 Application to the SPECK Family

For simplicity, we take SPECK32 as an illustration. Figure 3 shows the notation of the masks in round r. From Eq. (1), we can derive the constraints on linear approximation of SPECK32 in round r as

$$\begin{aligned} \begin{aligned} z_{15}^r&= 0, \\ z_{14}^r&= a_6^r \oplus c_{15}^r \oplus d_{15}^r, \\ z_j^r&= z_{j+1}^r \oplus a_{j+8}^r \oplus c_{j+1}^r \oplus d_{j+1}^r, \\ z_i^r&\ge a_{i+7}^r \oplus d_i^r, \\ z_i^r&\ge c_i^r \oplus d_i^r,\\ d_i^r&= a_i^{r+1} \oplus b_i^{r+1},\\ c_i^r&= b_i^r \oplus b_{i+2}^{r+1}, \\ \end{aligned} \end{aligned}$$
(3)

where \(0\le i \le 15\), \(0\le j \le 13\), and \(\sum _{r,i} z_i^r\) is to be minimized.

Since usually the time for unsatisfiable decision is much longer than that for satisfiable, we follow Algorithm 1 below to find linear trails with optimal correlation, which ensures that the most time-consuming part unsatisfiable only appears once during the search.

figure a

Table 2 gives an overview of the correlation of optimal linear trails in round-reduced SPECK ciphers.Footnote 1 We confirm all the correlations of optimal linear trails in [28]. Moreover, our method covers significantly more rounds in larger versions of SPECK: 11/13/9/9 rounds comparing to 7/5/4/4 rounds in previous paper [28] for SPECK48/64/96/128.

Table 2. Correlation of best linear trail in SPECK family.
Full size table

We also show examples of linear trails with best correlation for round-reduced SPECKs in Table 3. Sometimes without further constraints, input and output masks may have very high Hamming weight. By setting cardinality constraints on the Hamming weights of the masks, we can obtain trails with input and output masks of the lowest Hamming weight under a given correlation and number of rounds, an example is the linear trail of 11-round SPECK32 in Table 3.

Table 3. Linear trail with best correlation in reduced-round SPECK.
Full size table

4.2 Application to Chaskey

The designers of Chaskey did not give a security evaluation against linear cryptanalysis in their paper. Using our method, we are able to find the correlation of the best linear trail for the round-reduced Chaskey permutation, as shown in Table 4. Table 5 is an example trail for 3-round Chaskey. Notations a, b, c, d are the masks on each 32-bit branch.

Table 4. Correlation of optimal linear trails in round-reduced Chaskey.
Full size table
Table 5. A linear trail with optimal correlation in 3-round Chaskey.
Full size table

4.3 Enumerating Linear Trails in a Linear Hull

For most SAT solvers, if the problem is satisfiable, they can print all the solutions. However, due to the additional variables introduced by encoding methods in generating the CNF files, the solvers may output duplicated solutions which represent the same trail, as also observed by Kölbl et al. in [13]. To avoid inaccuracy, we generate the solutions one by one:

  • Step 1: Generate the CNF file for the problem, ask the solver to give one solution \(\bar{s}\) if it exists.

  • Step 2: Append a new clause to the current CNF file in order to rule out \(\bar{s}\).

  • Step 3: Ask solver to give a solution, repeat step 2 until the solver returns unsatisfiable.

In Table 6, we give the best linear hulls found and their corresponding distribution of trails for 9-round, 10-round SPECK32, where ALP is the estimated averaged linear probability. The experimental average ALP with 128 random keys for the above linear hulls are \(2^{-28.9}\) and \(2^{-31.1}\) respectively.

Table 6. The Distribution of linear trails in best found 9-/10-round SPECK32 linear hull.
Full size table

4.4 Comparison of Solvers

In some previous papers on automatic searching of differential and linear trails, e.g. [17, 25], the searching idea is modelled as a MILP problem and solved by CPLEX. To compare the performance of CPLEX and Cryptominisat4, we encode the same constraints with MILP language and CNF without optimisation. Despite the connection between the MILP and the SAT problem with an objective function, our method has an advantage over CPLEX. For instance, to find an optimal linear trail in 6-round SPECK32, it takes over 4000 s on CPLEX, comparing to about 2 s on Cryptominisat4.Footnote 2

Another commonly used solver is STP [11], which is a SMT solver and also a CNF generator. It can encode constraints into CNF file inside the solver based on SMTLIB2 language, and then call a SAT solver to solve the problem. Unlike Cryptominisat4, STP does not support XOR clauses and Gaussian elimination, therefore all clauses involving XOR are translated into standard CNF format. Thus, with exactly the same constraints derived in Sect. 3.1, we generate different CNF files encoded by STP and our method, and compare their performances on the searching problem of SPECK by considering the number of variables and clauses in corresponding CNF file, as well as the run time for getting optimal linear trails and unsatisfiable decision. Both CNF files run on Cryptominisat4.

Table 7. Comparison between the runtime of CNF files generated by Sect. 3 and STP on the searching problems of SPECK128.
Full size table

In most cases, the CNF file encoded by our method has a smaller number of variables and clauses than the STP-generated ones, and the difference can be two times for problems in SPECK with larger block sizes. Although the size of the problem and the speed of solving are not strictly proportional, in general, less variables and clauses are preferable. Table 7 shows the comparison between the runtime of CNF files generated by the method in Sect. 3 and STP solver, where time1 is the time to find an optimal linear trail, and time2 is the time to return unsatisfiable. In general, the performance of both methods is comparable. However it is interesting to notice that, it takes 2 s to find one optimal trail for 8-round SPECK128 by our method while STP uses around one hour. It shows that the performance of CNF files depends heavily on the encoding method and the underlying problem, therefore our method may provide an alternative way to solve problems which are not solvable using other solvers.

5 Conclusion

In this paper, we focus on how to find linear trails with optimal correlations in the ARX structures. We model the question as a boolean satisfiability problem, translate the propagation of masks through ARX operations into bitwise expressions and CNF constraints, and then solve the problem by SAT solvers. We apply the automatic search method to the block cipher SPECK and MAC proposal Chaskey, and obtain the correlation of optimal linear trails for 22/11/13/9/9-round reduced SPECK32/48/64/96/128 and 3-round Chaskey, where the analysis of optimal linear trails on Chaskey is presented for the first time so far. In addition, our method is applied to enumerate linear trails in two linear hulls of 9-round and 10-round SPECK32.

Our work provides a searching tool with improved performance towards analysing the security of ARX designs against linear cryptanalysis, which is meaningful to both designers and attackers.