Proposing an MILP-based method for the experimental verification of difference-based trails: application to SPECK, SIMECK

Abstract

Searching for the right pairs of inputs in difference-based distinguishers is an important task for the experimental verification of the distinguishers in symmetric-key ciphers. In this paper, we develop an MILP-based approach to verify the possibility of difference-based distinguishers and extract the right pairs. We apply the proposed method to some published difference-based trails (Related-Key Differentials (RKD), Rotational-XOR (RX)) of block ciphers SIMECK, and SPECK. As a result, we show that some of the reported RX-trails of SIMECK and SPECK are incompatible, i.e. there are no right pairs that follow the expected propagation of the differences for the trail. Also, for compatible trails, the proposed approach can efficiently speed up the search process of finding the exact value of a weak key from the target weak key space. For example, in one of the reported 14-round RX trails of SPECK, the probability of a key pair to be a weak key is $2^{-94.91}$ when the whole key space is $2^{96}$; our method can find a key pair for it in a comparatively short time. It is worth noting that it was impossible to find this key pair using a traditional search. As another result, we apply the proposed method to SPECK block cipher, to construct longer related-key differential trails of SPECK which we could reach 15, 16, 17, and 19 rounds for SPECK32/64, SPECK48/96, SPECK64/128, and SPECK128/256, respectively. It should be compared with the best previous results which are 12, 15, 15, and 20 rounds, respectively, that both attacks work for a certain weak key class. It should be also considered as an improvement over the reported result of rotational-XOR cryptanalysis on SPECK.

1 Introduction

Mixed Integer Linear Programming (MILP) was introduced in [37, 48] to evaluate the security of a block cipher against differential and linear cryptanalysis. Mouha et al. [37] used MILP method to minimize the number of active S-boxes in a differential or linear trail. Later, Sun et al. in [45, 46] extended Mouha et al.’s work from byte-oriented ciphers to bit-oriented ciphers. Recently, MILP has been widely used for the cryptanalysis of block ciphers so that [13, 17, 38, 39, 41, 52] can be mentioned as some examples among others. Other automatic tools for the cryptanalysis of block ciphers are constraint programming see [18, 19, 44], SAT/SMT/CryptoSMT see [12, 21, 28, 34].

ARX-based ciphers are designed using only modular Addition, Rotation, and XOR. In particular, the only source of non-linearity in an ARX scheme is the modular addition. Algorithms built in this fashion are usually faster and smaller than S-Box-based algorithms in software, and have some inherent security against side-channel attacks as modular addition leaks less information than table look-ups. However, modular addition is not very attractive in designing hardware optimized algorithms due to its latency and “large” input and output size. Some examples of ARX ciphers are: the block ciphers SPECK [5], HIGHT [23], LEA [22], the stream cipher SALSA20 [6], and the SHA-3 finalists SKEIN [16] and BLAKE [4]. SPECK is a family of lightweight block ciphers that uses an ARX structure that was publicly released by the National Security Agency (NSA) in 2013 [5]. SPECK has been optimized for performance in software implementations. SPECK is evaluated by many cryptanalysis techniques [2, 10, 11, 14, 17, 24, 33, 42, 51].

The probability of differential trails (in differential [8] or rotational-XOR [3] cryptanalysis) is usually built by multiplying the probabilities of each non-linear operation, but this approach can lead to very misleading results in some ciphers. For example, in some ARX-based ciphers, the independence assumption does not hold since it is possible for an output of modular addition to be directly given as input to another modular addition. Therefore, in such cases, the probabilities of modular additions cannot be computed as the product of probabilities of the individual modular additions. It is important to note that in the case of ARX ciphers such differences were already described for some attacks. For example, Knudsen et al. in [27], treated this issue for the differential attack on RC2 block cipher. As another example, the authors of [26], investigated this issue for the rotational cryptanalysis on ARX structures. Several recent works have found trails that were incompatible when analyzing ARX hash functions [9, 29, 30, 36, 40, 47] and many others. Also, Elsheikh et al. in [15] recently studied this issue and proposed an MILP model to describe the differential propagation through the modular addition considering the dependency between the consecutive modular additions and utilized their approach to automate the search process for the differential trails for Bel-T cipher.

Recently, Liu et al. presented an MILP model for the automatic verification of differential characteristics in permutation-based primitives [32]. Their main idea is modeling the differential transitions and value transitions simultaneously for permutation-based primitives and then connecting the value transitions and differential transitions for non-linear operations used in primitives. They successfully applied their approach to reduced Gimli hash function [7]. To this end, in a part of their work, they described how they connected the value and differential transitions of AND and OR operations (the only non-linear operations used in Gimli). However, they did not explain how one can connect the value and differential transitions simultaneously for the other non-linear operations.

Hence, our work has some advantages over [32]. In fact, our approach in this paper can be applied easily to any cipher structure with usual non-linear operations such as AND, OR, Addition modulo $2^{n}$, S-boxes layers, and others. Also, as will be explained later, our approach can be efficiently used to verify the differential, related-key differential, and rotational-XOR trails of ciphers.

In this paper, for the first time, to the best of our knowledge, we present an MILP-based approach to experimentally verify whether a difference-based distinguisher includes any right pair. As for the applications, we apply our approach to the obtained differential trails of SIMECK and SPECK family of block ciphers. Also, the designers of SPECK family claim that SPECK is designed to have resistance against related-key attacks. Part of this paper, focuses on the automatic related-key differential cryptanalysis of a reduced SPECK block cipher to find distinguishers covering more rounds than those found previously. Moreover, the SPECK family of block ciphers is standardized by ISO in the RFID area of Sc31. Hence, analysis from various aspects is important.

1.1 Our contribution

Our contribution in this paper is as follows:

• In this paper, we applied the MILP approach to identify incompatible differential trails of block ciphers. Moreover, to the best of our knowledge, for the first time we applied the MILP approach to efficiently speed up the search process of finding the exact value of a weak key from the target weak key space. As the applications, we apply our approach to verify the presented Rotational-XOR (RX) trails of SPECK and SIMECK family of block ciphers based on papers [33] and [35], respectively.

• We find some weak keys for 15 and 20-round RX-trails of SIMECK32/64, according to the Tables 4 and 6 of [35]. Also, our approach returns this fact that the RX-trails for 27 and 35 rounds of SIMECK48/96, and SIMECK64/128, based on Tables 7 and 8, respectively in [35], are incompatible.

• Our approach can find the weak keys for 12, 13, and 15-round RX-trail of SPECK48/96 based on Tables 3 and 4 in [33]. Moreover, our approach shows that RX-trails for 11 and 12 rounds of SPECK32/64, and 14 rounds of SPECK48/96, according to Tables 2 and 4 in [33], are incompatible trails.

• In addition, we explain how we can search compatible differential trails in block ciphers and apply it to search related-key differential trails of some variants of SPECK family. As a result, we present a search strategy for the searching of related-key differential trails of SPECK family. We also present several distinguishers for the reduced version of SPECK32/64, SPECK48/96, SPECK64/128, and SPECK128/256, in related-key mode. We consider our result for related-key differential as an improvement over Liu et al.’s work [33], but from differential view. For SPECK32/64, the longest distinguisher proposed in this paper covers 15 rounds of the cipher while the best previous related work, i.e., rotational-XOR differential trail, covers only 12-round [33] (of course we show that this 12-round is an invalid trail). In total, for this version of SPECK, we present distinguishers for 10 to 15 rounds which work for a certain weak key class. It is worth noting that the proposed distinguishers for 13 to 15 rounds are the new distinguishers for these rounds of SPECK32/64. For SPECK48/96, our longest distinguishers cover 16 rounds, while the best previous related work covers 15 rounds [33] and both work for a certain weak key class. We present the distinguishers for 13 to 17 rounds of SPECK64/128 so that the distinguishers for 16 and 17 rounds are the new distinguishers for these rounds of SPECK64/128, for a certain weak key class. Also, we present the distinguishers for 16 and 19 rounds of SPECK128/256.

• Moreover, for every obtained related-key differential of SPECK family, we use our MILP-based approach to test whether the key differential trails are valid. For each one, we report a weak key to verify it. Based on our experimental verification, our results are consistent with the theoretical predictions.

In this paper, the computations are performed on PC (Intel Core (TM)i-5, CPU 3.50 GHz, 8 Gig RAM, Windows 10 x64) and also on a server (36 Core, Intel(R) Xeon(R) CPU E5-2695, 2.10GHz) with the optimizer Gurobi [20].

1.2 Outline

The remainder of this paper is organized as follows. Section 2 provides the required preliminaries, including a brief description of SPECK and SIMECK block ciphers and as well as Rotational-XOR cryptanalysis. In Sect. 3, our MILP-based method in searching for the right pairs of difference-based trails is presented. In Sect. 4, some applications of our approach are given. We explain how we can search compatible differential trails in block ciphers and apply it to search related-key differential trails of some variants of SPECK family. Finally, the paper is concluded in Sect. 6.

2 Preliminaries

2.1 Notations

In this paper, we denote an n-bit vector by $x = (x_{n-1}, \ldots , x_1, x_0)$, where $x_0$ is the least significant bit. Also, the logical operation XOR, left circular rotation, right circular rotation, the concatenation of x and y, the modular addition of bit string x and y, and the bit-wise AND are referred to as $\oplus$, $\lll$, $\ggg$, $x \Vert y$, $x\boxplus y$, and&, respectively. Also, all input/output differentials (or values) are in hexadecimal form and we omit the $\mathtt {0x}$ symbol.

2.2 A brief description of SPECK

SPECK is a family of lightweight block ciphers designed by NSA in 2013 [5]. Generally, SPECKb/mn will denote SPECK with $b=2n$ bit block size ($n \in \{16,24,32,48,64\}$) and mn bits key size ($m \in \{2,3,4\}$). The round function $F: {\mathbb {F}}_2^{n} \times {\mathbb {F}}_2^{2n} \rightarrow {\mathbb {F}}_2^{2n}$ of SPECK takes as input a n bit sub-key $k^{i-1}$ and a cipher state consisting of two n bit words $(x^{i-1},y^{i-1})$ and produces the next round state $(x^{i},y^{i})$ as follows:

$$\begin{aligned} x^i:= \big ( (x^{i-1} \ggg \alpha ) \boxplus y^{i-1} \big ) \oplus k^{i-1},\,\,\, y^{i}:=\big ( y^{i-1} \lll \beta \big ) \oplus x^i \end{aligned}$$

The value of rotation constant $\alpha$ and $\beta$ are specified as: $\alpha =7$, $\beta =2$ for SPECK32/64 and $\alpha =8$, $\beta =3$ for all other variants. The SPECK key schedules algorithm uses the same round function to generate the round keys. Let $K=(l^{m-2},\ldots ,l^{0},k^0)$ be a master key for SPECK2n/mn where $l^i,k^0 \in {\mathbb {F}}_{2^n}$. The round key $k^{i+1}$ is generated as $k^i = ((l^{i-1}\ggg \alpha ) \boxplus k^{i})\oplus c \oplus (k^{i-1}\lll \beta )$ for $l^{i+m-2}=((l^{i-1}\ggg \alpha )\boxplus k^{i-1})\oplus c,$ with $c = i-1$ the round number starting from 1.

A single round of SPECK with $m = 4$ is depicted in Fig. 1a.

Fig. 1

Illustration of the SPECK and SIMECK ciphers

In this paper, we consider those members of SPECK family for which the parameter of m is 4, i.e., SPECK32/64, SPECK48/96, SPECK64/128, and SPECK128/256 that respectively include 22, 23, 27, and 34 rounds, to produce a ciphertext from a plaintext.

2.3 A short description of SIMECK

SIMECK is a family of block ciphers that was proposed at CHES 2015 [50]. For $n=16,24,$ and 32, SIMECKb/k has a block size of $b=2n$ and a key size of $k=2b$. It is a classical Feistel network shown in Fig. 1b where the function F is defined as $F(x^{i-1}) = x^{i-1} \& (x^{i-1} \lll 5)$. In the key schedule of SIMECK, the round keys $K^i \quad (i= 0,\ldots , r)$ are generated from a given master key $(K^3,K^2,K^1,K^0)$ with the help of the feedback shift registers as follows:

$$\begin{aligned} K^{i+4}=K^{i}\oplus f_{c^{i}}(K^{i+1})\oplus c^{i}, \quad i=0,1,\ldots ,r-4, \end{aligned}$$

(1)

where r for SIMECK32/64, SIMECK48/96, and SIMECK64/128 is 32, 36, and 44, respectively. Also, $c^{i} \in \{1_{n-2}01,1_{n-2}00\}$ is predefined constants ($1_{n-2}$ is a sequence of $n-2$ bit 1) and $f_c^{i}$ is the SIMECK round function with $c^{i}$ acting as the round key.

2.4 Rotational-XOR(RX) cryptanalysis

Rotational cryptanalysis is a generic attack targeting ARX structures [25, 26]. RX-cryptanalysis is a recent technique as a related-key chosen plaintext attack to ARX structures proposed by Ashur and Liu in 2016 [3]. This attack was applied to the block cipher SPECK [33], SIMECK [35] and the hash function SipHash [49].

An RX-pair is defined as a rotational pair with rotational offset $\gamma$ under translation a as $(x,(x \lll \gamma )\oplus a)$.

Definition 1

(RX-difference [3]) The RX-difference of x and $x'=(x\lll \gamma )\oplus a$ with rotational offset $\gamma$, and translation a is denoted by

$$\begin{aligned} \varDelta _\gamma (x,x') = (x \lll \gamma ) \oplus x' . \end{aligned}$$

Furthermore, we will argue that RX difference of a pair $(x,x')$ is $\varDelta _\gamma (x,x')$ if $(x\lll \gamma ) \oplus x' = \varDelta _\gamma (x,x')$. It is clear that the rotation of an RX pair is an RX pair, the XOR of two RX pairs is also an RX pair. Also, the XOR of a constant c to each of the values in $(x,x') = (x, (x \lll \gamma )\oplus a)$ is the RX-pair $(z,z')=(x\oplus c,(x \lll \gamma )\oplus a \oplus c)$. Now, soppose that we denote the corresponding RX-difference in c by $\varDelta ^{\gamma }c$. Then the following condition should be satisfied.

$$\begin{aligned} \varDelta _{\gamma }(x,x^{'}) \oplus \varDelta ^{\gamma }c = \varDelta _{\gamma }(z,z^{'}). \end{aligned}$$

Since $\varDelta _{\gamma }(x,x^{'}) = a$ and $\varDelta _{\gamma }(z,z^{'}) = a\oplus c \oplus (c\lll \gamma )$, therefore, the condition above gives us $\varDelta ^{\gamma }c= c \oplus (c \lll \gamma )$. Hence, by considering the corresponding RX-difference in c as $\varDelta ^{\gamma }c= c \oplus (c \lll \gamma )$, $\varDelta _{\gamma }(x,x^{'})$ propagates to $\varDelta _{\gamma }(z,z^{'})$ with propability 1.

For modular addition, in ( [3], theorem 1) the authors showed how one can calculate the transition probability of RX pair through modular addition. In addition, the authors of [35] extended the idea of RX-cryptanalysis to AND-RX ciphers with applications to SIMON and SIMECK. We assume that $\gamma =1$ throughout this paper.

3 MILP-based method to identify incompatible differential trails

In this section, we explore a simple approach based on the MILP method to verify whether the differential trails are compatible. Also, it must be noted that our method in this section can be very useful in most cases to find weak keys in related-key scenarios.

3.1 Our approach

To experimentally verify whether an RX or differential distinguisher includes any right pair, a common way is to use a simple method of guessing the keys and check the differences of the states. However, it is often infeasible because of the block size of the cipher and the probability of the distinguisher. In this section, we model an MILP-based method to determine whether there exist right pairs for the differential trails. To this end, suppose f is a function with variables $x_0,x_2,\ldots x_{n_v-1}$. In our approach, we built some linear inequalities to ensure that the following conditions are exactly established and added them to the MILP model.

$$\begin{aligned} f({x_0},{x_2}, \ldots ,{x_{{n_v-1}}})= & {} y\, , \,\,\,\,\,\,f({x'_0},{x'_2}, \ldots ,{x'_{{n_v-1}}}) = y',\\ \varDelta ({x_0},{x'_0})= & {} {X_0},\,\,\,\varDelta ({x_2},{x'_2}) = {X_2}, \ldots ,\varDelta ({x_{{n_v-1}}},{x'_{{n_v-1}}}) = {X_{{n_v-1}}},\\ \varDelta (y,y')= & {} Y, \end{aligned}$$

where the difference $\varDelta (a,b)$ is defined as $a\oplus b$ and $\varDelta _1(a,b)$ in case of differential and RX trails, respectively. In this paper, the function f is considered as the encryption function or key expansion function of a block cipher. It is obvious that for a given differential trail of a cipher, if its MILP model, as shown above is infeasible then the trail will be an incompatible trail; otherwise, the model returns the right pairs.

Each cipher is designed by combining several operations. The most important operations used in cryptographic algorithms are AND, modular addition, rotation, XOR operations. In the following section, we show that there is a set of linear inequalities which can exactly describe all valid values of these operators in the MILP model.

3.1.1 Modeling the XOR operation

For every XOR operation, with bit-level input values $x_1, x_2$, and bit-level output value y, the constraints are as follows¹:

$$\begin{aligned} \left\{ {\begin{array}{*{20}{c}} {x_1 + x_2 + y \le 2,}\,\,\,\,\, {x_1 + x_2 - y \ge 0,}\\ {x_1 + y -x_2 \ge 0,}\,\,\,\,\, {x_2 + y - x_1 \ge 0.} \end{array}} \right. \end{aligned}$$

(2)

3.1.2 Modeling the modular addition

In the following section, we present the basic definition of modular addition that will be used to model the modular addition.

Definition 2

(Addition modulo $2^n$ [31]) The carry, carry$(x,y): = c \in {\{ 0,1\} ^n},x,y \in {\{ 0,1\} ^n},$ of addition $x+y$ is defined recursively as follows. First, $c_0:=0$. Second, ${c_{i + 1}}: = ({x_i} \wedge {y_i}) \oplus ({x_i} \wedge {c_i}) \oplus ({y_i} \wedge {c_i}),$ for every $i \ge 0$. Equivalently, ${c_{i + 1}} = 1 \Leftrightarrow {x_i} + {y_i} + {c_i} \ge 2.$

Property 1

([31]) If $(x,y) \in {\{ 0,1\} ^n} \times {\{ 0,1\} ^n},$ then $x+y=x \oplus y \oplus carry(x,y).$

Based on Definition 2 and Property 1, to model the modular addition $(z=x+y)$ in the MILP model, we must consider the linear inequalities whose solution set is exactly satisfied in the following conditions.

$$\begin{aligned}&1. \,\,\,{c_0} = 0. \nonumber \\&2. \,\,\, {c_{i + 1}} = 1 \Leftrightarrow {x_i} + {y_i} + {c_i} \ge 2,\,\,for\,\,\,i = 0, \ldots ,n - 2.\nonumber \\&3. \,\,\, {z_i} = {x_i} \oplus {y_i} \oplus {c_i},\,\,for\,\,\,i = 0, \ldots ,n - 1. \end{aligned}$$

(3)

Therefore, it is enough to describe these conditions of the Eq. (3) as linear inequalities. The first condition is obvious. To model the second condition, we can consider the vector $({x_i},{y_i},{c_i},{c_{i + 1}})$ as follows.

$$\begin{aligned}({x_i},{y_i},{c_i},{c_{i + 1}}) \in \left\{ {\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} {(0,0,0,0)}&{}{(0,0,1,0)}&{}{(0,1,0,0)}&{}{(0,1,1,1)} \end{array}}\\ {\begin{array}{*{20}{c}} {(1,0,0,0)}&{}{(1,0,1,1)}&{}{(1,1,0,1)}&{}{(1,1,1,1)} \end{array}} \end{array}} \right\} . \end{aligned}$$

Therefore, we consider the equations which prohibit the invalid $({x_i},{y_i},{c_i},{c_{i + 1}})$. Hence, for $i = 0, \ldots ,n - 2$, we have

$$\begin{aligned}\left\{ {\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} {{x_i} + {y_i} - {c_{i + 1}} \ge 0,}\,\,\,\,\, {{x_i} + {c_i} - {c_{i + 1}} \ge 0,}\,\,\,\,\, {{y_i} + {c_i} - {c_{i + 1}} \ge 0,}\\ \end{array}} \end{array}}\\ {{y_i} + {c_i} - {c_{i + 1}} \le 1,}\,\,\,\,\, {{x_i} + {c_i} - {c_{i + 1}} \le 1,}\,\,\,\,\, {{x_i} + {y_i} - {c_{i + 1}} \le 1,} \end{array}} \right. \end{aligned}$$

To model the third condition, we can consider the following equations.

$$\begin{aligned} {x_i} + {y_i} + {z_i} + {c_i} - 2{d_i} = 0,\,\,\,\,\,\,{d_i} = 0\,\,or\,\,1\,\,or\,\,2,\,\,\,\,i = 0, \ldots ,n - 1. \end{aligned}$$

Therefore, with these inequalities, we can model the exact values of modular addition operation to the MILP.

3.1.3 Modeling the AND operation

For every AND operation with bit-level input values $x_1,x_2$. and bit-level output value y, the constraints are as follows:

$$\begin{aligned} {x_1} - y \geqslant 0,\,\,\,\,\,{x_2} - y \geqslant 0,\,\,\,\,\,{x_1} + {x_2} - y \leqslant 1. \end{aligned}$$

4 Applications

In this section, we apply our method to verify RX trails for SPECK and SIMECK presented in [33] and [35], respectively.

4.1 Verifying the previous reported RX trails on SIMECK

The authors of [35] analyzed the propagation of RX-differences through AND-RX rounds and developed a formula for their expected probability. Also, they formulated an SMT model for searching RX-trails in SIMON and SIMECK. They found RX-distinguishers up to 20, 27, and 35 rounds with respective probabilities of $2^{-26}$,$2^{-42}$, and $2^{-54}$ for SIMECK32/64, SIMECK48/94, and SIMECK64/128, for a weak key class of size $2^{30}, 2^{44}$ and $2^{56}$ respectively. In most cases, these are the longest published distinguishers for the respective variants of SIMECK. The authours of [35] only presented the details of a 15 and 20-round RX trail in SIMECK32/64, a 27-round RX trail in SIMECK48/96, and a 35-round RX trail in SIMECK64/128 (see [35], Tables 4, 6, 7, and 8, respectively). Here we intend to find the right key pairs that satisfy the required RX-difference of the sub-keys in tables mentioned in [35].

The SIMECK key schedule algorithm is designed by combining AND, bit rotation, and XOR operations. Hence, we can model the SIMECK key schedule with the method described in Sect. 3 and then fix the RX-difference in sub-keys based on the mentioned RX trails. Our model returned the following result:

• For 15 and 20-round RX trails of SIMECK32/64 ( [35], Tables 4, 6), our method found some weak keys (see Table 1).

Table 1 Some master key values to satisfy the RX-differences in 15 and 20-round of SIMECK32/64 based on Tables 4 and 6 in [35]

• The RX trails in [35] for 27 and 35 rounds of SIMECK48/96 and SIMECK64/128, respectively, are incompatible.

In the following lemma, we prove the incompatibility of RX trail related to 27 rounds of SPECK48/96 in [35].

Lemma 1

There are no right pair to satisfy the RX-difference of the sub-keys of 27 rounds of SIMECK48/96 based on the Table 7 in [35].

Proof

To find a contradiction in the RX-difference of sub-keys in this Table 7 of [35], we only consider the rounds 2, 3, and 6 of the trail. These rounds are shown in Fig. 2 in details. The red numbers show the RX-differences.

Fig. 2

Part of the 27-round RX-trail of sub-keys for SIMECK48/96 based on Table 7 in [35]

As can be seen in Fig. 2, the AND operations in rounds 2, 3, and 6 satisfy the conditions of Lemma 1 in [35] and so they hold with probabilities of $2^{-2},2^{-4}$, and $2^{-4}$, respectively. Assuming independency, the probability of the RX-difference of these three rounds should hold with a probability of $2^{-32}$; however, we show that it is an incompatible trail. To this end, let $f(x) = x \& (x \lll 5)$ be the F-function of key schedule of SIMECK. Also, assume that $\varDelta _1\alpha$ and $\varDelta _1\beta$ respectively are RX-differences of the input and output of f(x), such that the probability $\varDelta _1\alpha$ to $\varDelta _1\beta$ is non-zero. If we consider the input pairs of f(x) as $\left( {x,(x \lll 1) \oplus \varDelta _1\alpha } \right)$, then there is the following relation between $\varDelta _1\alpha ,\varDelta _1\beta$, and x:

$$\begin{aligned} (f(x)\lll 1) \oplus f(x \lll 1 \oplus \varDelta _1\alpha ) = \varDelta _1\beta . \end{aligned}$$

By considering x as $x=(x_{23},\ldots ,x_{1},x_{0})$, the j-th bit of $\varDelta _1\beta$ (i.e., $\varDelta _1\beta _j$) is determined as follows.

$$ \begin{aligned} \left( {{x_{j - 1}} \& {x_{j - 6}}} \right) \oplus \left( {({x_{j - 6}} \oplus {\varDelta _1\alpha _{j - 5}}) \& ({x_{j - 1}} \oplus {\varDelta _1\alpha _{j - 1}}} )\right) = {\varDelta _1\beta _j}. \end{aligned}$$

(4)

Now, in the second round by considering the sub-key $k^2$ as the input of f(x) and for $j=6$, we have

$$ \begin{aligned} \left( {{k^2_{5}} \& {k^2_{0}}} \right) \oplus \left( {({k^2_{0}} \oplus {\varDelta _1\alpha _{1}}) \& ({k^2_{5}} \oplus {\varDelta _1\alpha _{5}}}) \right) = {\varDelta _1\beta _{6}}, \end{aligned}$$

since in the second round $\varDelta _1\alpha =\varDelta _1\beta =\mathtt {000002}$, we have

$$ \begin{aligned} \left( {{k^2_{5}} \& {k^2_{0}}} \right) \oplus \left( ({k^2_{0}} \oplus 1) \& k^2_{5} \right) = 0, \end{aligned}$$

and this gives $k^2_{5}=0$.

Now, in the third round by considering the sub-key $k^3$ as the input of f(x), for $j=6$, and due to the $\varDelta _1\alpha =\mathtt {000003}$ and $\varDelta _1\beta =\mathtt {000001}$ we have

$$ \begin{aligned} \left( k^3_{5} \& k^3_{0} \right) \oplus \left( ({k^3_{0}} \oplus 1) \& {k^3_{5}} \right) = 0, \end{aligned}$$

so we have $k^3_{5}=0$. Also, for $j=5$,

$$ \begin{aligned} \left( k^3_{4} \& k^3_{23} \right) \oplus \left( ({k^3_{23}} \oplus 1) \& {k^3_{4}} \right) = 0, \end{aligned}$$

so this concludes

$$\begin{aligned} k^3_{4}=0. \end{aligned}$$

(5)

In the sixth round, $k^6$ will be the input of f(x) and also $\varDelta _1\alpha =\varDelta _1\beta =\mathtt {000003}$, therefore, by considering $j=6$ in Eq. (4), we have

$$ \begin{aligned} \left( k^6_{5} \& k^6_{0} \right) \oplus \left( ({k^6_{0}} \oplus 1) \& {k^6_{5}} \right) = 0, \end{aligned}$$

so we have $k^6_{5}=0$.

On the other hand according to the third round, we have

$$ \begin{aligned} k^6_{5}=\left( (k^3_{0} \& k^3_{5}) \oplus k^3_{4} \oplus k^2_{5} \oplus c_{5} \right) . \end{aligned}$$

For the third round the constant $c=\mathtt {fffffd}$ and so $c_{5}=1$. As was shown above, we have $k^2_{5}=k^3_{5}=k^6_{5}=0$ so the equation above concludes $k^3_{4}=1$. Hence, by considering the Eq. 5, we reach a contradiction. $\square$

4.2 Verifying the previous reported RX trails on SPECK

In [33], the authors formulated a SAT/SMT model for RX cryptanalysis in the ARX primitives and applied it to the block cipher family SPECK. They obtained longer distinguishers than the ones previously published for the block cipher family SPECK working for a certain weak key class. They presented several distinguishers for SPECK32/64, SPECK48/96, SPECK64/128, SPECK96/144, and SPECK128/256. Note that the authors only presented the details of several trails and for other trails they only reported the probabilities. Hence, in this section, we just verified the trails that are presented in detail in [33]. We modeled the SPECK key schedule with the method described in Sect. 3 to verify the trails in [33]. Our MILP model returned the following result.

• Our model found the weak keys for 12, 13, and 15-round RX-difference of SPECK48/96 with respective probabilities of $2^{-26.75}, 2^{-31.98}$, and $2^{-43.81}$, for a weak key class of size $2^{43.51}, 2^{24.51}$, and $2^{1.09}$, respectively (for more details of these trails refer to Tables 3 and 4 in [33]). Note that based on the authors’ claim, for experimental verification of trails they injected key differences artificially and only tested the probability of the RX characteristics over the cipher part. The resultant weak key for these RX trails are listed in Table 2. Note that, [33] did not report the RX-differences for the master keys $(\varDelta _1l^{2},\varDelta _1l^{1},\varDelta _1l^{0})$. Therefore, in our MLP model we did not fix the RX-differences of these master keys and let the MILP model choose any appropriate differences.

Table 2 Some master key values to satisfy the RX-differences in 12, 13, and 15-round of SPECK48/96 based on Tables 3 and 4 in [33]

• Our model did not find any weak keys for the following RX trails:

  $\circ$:

  RX trails for 11 and 12 rounds of SPECK32/64 with respective probabilities of $2^{-22.15}$ and $2^{-25.57}$, for a weak key class of size $2^{18.68}$ and $2^{4.92}$, respectively (for more details of these trails refer to Table 2 in [33]).

  $\circ$:

  RX trails for 14 rounds of SPECK48/96 with respective probabilities of $2^{-37.40}$, for a weak key class of size $2^{0.34}$ (for more details of this trail refer to Table 4 in [33]).

  In the following lemma, we prove the incompatibility of RX trail related to 11 rounds of SPECK32/64 in [33]. In fact, the reason for this incompatibility is that the independence assumption in the key schedule algorithm of SPECK does not hold since an output of modular addition is given as input to another modular addition. A schematic view of this fact is depicted in Fig. 3.

Lemma 2

There are no right pairs to satisfy the RX-difference of the sub-keys of 11 rounds of SPECK32/64 based on the Table 2 in [33].

Proof

Based on Eq. (3), the bit values of $x, y, z \,\,(z=x+y)$, with the carry c, belong to the following set.

$$\begin{aligned} ({x_j},{y_j},{z_j},{c_j},{c_{j + 1}}) \in \left\{ {\begin{array}{*{20}{c}} {(0,0,0,0,0),(0,0,1,1,0),(0,1,1,0,0),(0,1,0,1,1)} \\ {(1,0,1,0,0),(1,0,0,1,1),(1,1,0,0,1),(1,1,1,1,1)} \end{array}} \right\} \end{aligned}$$

(6)

We denote the two n-bit vectors representing RX-differences at the input of modular addition in the round i where $i=5, 8$, as $\varDelta _1 x^{i}=(\varDelta _1 x_{n-1}^{i},\ldots ,\varDelta _1 x_1^{i},\varDelta _1 x_0^{i})$ and $\varDelta _1 y^{i}=(\varDelta _1 y_{n-1}^{i},\ldots ,\varDelta _1 y_1^{i},\varDelta _1 y_0^{i})$ and the n-bit vectors representing RX-difference for output of modular addition as $\varDelta _1 z^{i}=( \varDelta _1 z_{n-1}^{i},\ldots ,\varDelta z_1^{i},\varDelta _1 z_0^{i})$ and the n-bit vectors representing RX-difference for carry as $\varDelta _1 c^{i}=(\varDelta _1 c_{n-1}^{i},\ldots ,\varDelta _1 c_1^{i},\varDelta _1 c_0^{i})$. It should be noted that based on the third condition of Eq. (3), the RX-difference of carry bit $c^{i}$ can be obtained as $\varDelta _1 c^{i}=\varDelta _1 x^{i} \oplus \varDelta _1 y^{i} \oplus \varDelta _1 z^{i}$.

Fig. 3

Part of the 11-round RX-trail of sub-keys for SPECK32/64 based on Table 2 in [33]

Therefore, the input/output RX-differences and the carry RX-difference of modular additions for the 5-th and 8-th rounds based on Fig. 3 can be written as binary notation as follows.

$$\begin{aligned}\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} {\varDelta _1 {x^{5}} = \mathrm{{0000000000000000,}}}&{}{\varDelta _1{x^{8}} = \mathrm{{0000011000000000,}}} \end{array}}\\ {\begin{array}{*{20}{c}} {\varDelta _1 {y^{5}} = \mathrm{{0000000000000000,}}}&{}{\varDelta _1 {y^{8}} = \mathrm{{0000001000000101,}}} \end{array}}\\ {\begin{array}{*{20}{c}} {\varDelta _1 {z^{5}} = \mathrm{{0000000000001111,}}}&{}{\varDelta _1 {z^{8}} = \mathrm{{0000000000011100,}}} \end{array}}\\ {\begin{array}{*{20}{c}} {\varDelta _1 {c^{5}} = \mathrm{{0000000000001111,}}}&{}{\varDelta _1 {c^{14}} = \mathrm{{0000010000011001}}\mathrm{{.}}} \end{array}} \end{array} \end{aligned}$$

By considering the modular addition operation for the 11-th round, we have $(\varDelta _1 x_{0}^{5},\varDelta _1 y_{0}^{5}$,$\varDelta _1 z_{0}^{5},\varDelta _1 c_{0}^{5},\varDelta _1 c_{1}^{5})=(0,0,1,1,1)$. It should be noted that the pair values that can have RX-difference (0, 0, 1, 1, 1) must be selected from the Set (6). Therefore, according to the Set (6), the following pairs have the differential (0, 0, 1, 1, 1).

$$\begin{aligned}\left\{ {({x_{0}^{5}},{y_{0}^{5}},{z_{0}^{5}},{c_{0}^{5}},{c_{1}^{5}})} \right\} \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,1,1,0,0)}\\ {(0,1,0,1,1)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(1,0,1,0,0)}\\ {(1,0,0,1,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

So, for each pair we get the condition

$$\begin{aligned} z_{0}^{5}={\overline{c}}_{1}^{5}, \end{aligned}$$

(7)

where ${\overline{c}}$ is the bit-wise NOT of c. Now, in a similar way and by considering the RX-difference $(\varDelta _1 x_{1}^{5},\varDelta _1 y_{1}^{5}$, $\varDelta _1 z_{1}^{5},\varDelta _1 c_{1}^{5},\varDelta _1 c_{2}^{5})=(0,0,1,1,1),$ for each possible pair we have

$$\begin{aligned} z_{1}^{5}={\overline{c}}_{1}^{5}, \end{aligned}$$

(8)

By considering the Eqs. (7) and (8), we have

$$\begin{aligned} z_{0}^{5}=z_{1}^{5}. \end{aligned}$$

(9)

Now, in the modular addition operation for the 8-th round, we have

$$\begin{aligned} (\varDelta _1 x_{9}^{8},\varDelta _1 y_{9}^{8},\varDelta _1 z_{9}^{8},\varDelta _1 c_{9}^{8},\varDelta _1 c_{10}^{8})=(1,1,0,0,1). \end{aligned}$$

Thus, from Set (6) the following pairs will lead to the RX-difference (1, 1, 0, 0, 1).

$$\begin{aligned} ({x_{9}^{8}},{y_{9}^{8}},{z_{9}^{8}},{c_{9}^{8}},{c_{10}^{8}}) \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,0,1,1,0)}\\ {(1,1,1,1,1)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(0,0,0,0,0)}\\ {(1,1,0,0,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

Hence, for these pairs we can get the condition

$$\begin{aligned} x_{9}^{8}=c_{10}^{8}. \end{aligned}$$

(10)

Now, by considering the RX-difference $(\varDelta _1 x_{10}^{8},\varDelta _1 y_{10}^{8},\varDelta _1 z_{10}^{8},\varDelta _1 c_{10}^{8},\varDelta _1 c_{11}^{8})$ = (1, 0, 0, 1, 0) for the 10-th bit, the following pairs will lead to this differential.

$$\begin{aligned} ({x_{10}^{8}},{y_{10}^{8}},{z_{10}^{8}},{c_{10}^{8}},{c_{11}^{8}}) \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,0,1,1,0)}\\ {(1,0,1,0,0)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(0,1,0,1,1)}\\ {(1,1,0,0,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

Therefore, we have the condition

$$\begin{aligned} x_{10}^{8}={{\overline{c}}}_{10}^{8}. \end{aligned}$$

(11)

By combining the Eqs. (10) and (11), we have

$$\begin{aligned} x_{9}^{8}={\overline{x}}_{10}^{8}. \end{aligned}$$

(12)

Since $x^{8} = (z^{5} \oplus 0004)\ggg 7$ (see Fig. 3), we have $z_{0}^{5}=x_{9}^{8}$ and $z_{1}^{5}=x_{10}^{8}$. Hence, by considering the Eqs. (9) and (12), we reach a contradiction. $\square$

5 Searching compatible differential trails in block ciphers

The two following steps can help us to search the compatible differential trails in the block ciphers.

• 1 Build an MILP-based model for searching a (related-key) differential trail or a SMT-based model for a RX trail (targeting ARX/AND structures) to obtain a satisfactory differential trail.²

• 2 Check if there exists a right pair of messages/keys based on the method mentioned in Sect. 3.

It is worth noting that if there exist no right pairs, the differential trail found above is an incompatible differential trail.³

5.1 Application on SPECK family of block ciphers

In the following section, we search the compatible related-key differential trails of SPECK family of block ciphers.

5.1.1 Searching the related-key differential trails of SPECK family of block ciphers

In this section, first, thanks to the MILP method, we present several distinguishers for the reduced version of SPECK32/64, SPECK48/96, SPECK64/128, and SPECK128/256, in related-key mode. Then, we apply the method described in Sect. 3 to find the incompatible trails. Our result in this section should be considered as an improvement over Liu et al.’s work [33], but from differential view. Both works analyze SPECK-family in weak key models but Liu et al. presented RX trails while we intend to present differential trails. However, as can be seen in the following section, we obtain significantly better results, in terms of weak key(s), class-size, or the number of rounds of the distinguishers.

5.1.2 Attack models

Let $Q_D$ be the encryption datapath and $Q_K$ be the key expansion datapath of SPECK block cipher and $\Pr (Q_D)$ and $\Pr (Q_K)$ show probability over the data path and the key expansion datapath, respectively. In this paper, inspired by the rotational-XOR analysis [33], we also consider 3 models of weak key attacks. In these models, an adversary can obtain data encrypted under two different keys with a known relation, for plaintexts that are chosen by the adversary. Attack models considered in this paper are as follows where $b=2n$, and mn denote the length of the block size and the length of the key, respectively.

• 1. Finding a good related-key differential trail of the cipher such that $\Pr (Q_D) \times \Pr (Q_K) > 2^{-b}$.

• 2. Finding a good related-key differential trail of the cipher with probability $\Pr (Q_D) > 2^{-b}$ such that $\Pr (Q_D) \times \Pr (Q_K) > 2^{-mn}$. This case of attacks is in a weak key class and the results are marked with $^\dag$ in the results tables.

• 3. Finding a good related-key differential trail of the cipher with probability $\Pr (Q_D) > 2^{-b}$ over the data part, and the key expansion part with probability $\Pr (Q_K) > 2^{-mn}$ (i.e., ensuring that at least one weak key exists). This case of attack can only be used in the open-key model, i.e., in addition to being in the weak key class and knowing the differential of the two related-keys; the adversary also knows the key values. These results are marked with $^\ddag$ in the results tables.

5.1.3 MILP-based differential trail search for SPECK family block cipher

In order to model the differential behavior of SPECK block cipher with the linear constraints expression in the MILP, it is sufficient to express XOR, bit-wise rotation, and modular addition. Both XOR and bit rotation are linear operations and can be modeled similar to the ones in Sect. 3.

5.1.4 MILP model for modular addition

Definition 3

(The differential of addition modulo $2^n$ [31]) We define the differential of addition modulo $2^n$ as a triplet of two input and one output differences, denoted as $(\alpha ,\beta \mapsto \gamma )$, where $(\alpha ,\beta ,\gamma ) \in \{0,1\}^{n}$. The differential probability of addition ($D{P^ + }$) is defined as follows:

$$\begin{aligned} D{P^ + }(\alpha ,\beta \mapsto \gamma ): = {2^{ - 2n}}.\# \left\{ {x,y:(x + y) \oplus \left( {(x \oplus \alpha ) + (y \oplus \beta )} \right) = \gamma } \right\} . \end{aligned}$$

In order to characterize the feasible differential trails for the modular addition and their corresponding probabilities, Lipmaa and Moriai in [31] proposed two theorems as follows.

Theorem 1

The necessary and sufficient condition for the differential $(\alpha ,\beta \rightarrow \gamma )$ to have a probability $>0$ is the following two conditions.

• 1. $\alpha _{0} \oplus \beta _{0} \oplus \gamma _{0} = 0,$

• 2. $if\,\,\alpha _{i - 1} = \beta _{i - 1} = \gamma _{i - 1} ,\,\,then\,\alpha _{i - 1} = \beta _{i - 1} = \gamma _{i - 1} = \alpha _{i} \oplus \beta _{i} \oplus \gamma _{i} ,\,\, i = 1, \ldots ,n - 1.$

Theorem 2

When the differential $(\alpha ,\beta \rightarrow \gamma )$ has a probability $> 0$, the probability is

$$\begin{aligned} {2^{ - \sum \limits _{i = 0}^{n - 2} {\sim eq\left( {\alpha _{i},\beta _{i},\gamma _{i}} \right) } }} \end{aligned}$$

where

$$\begin{aligned} eq\left( {\alpha _{i},\beta _{i},\gamma _{i}} \right) = eq_i = \left\{ {\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} 1&{}{\alpha _{i}= \beta _{i} = \gamma _{i}} \end{array}}\\ {\begin{array}{*{20}{c}} {0\,\,\,\,\,\,\,\,\,\,\,\,\,}&{}{o.w\,\,\,\,\,\,\,\,\,} \end{array}} \end{array}} \right. \end{aligned}$$

(13)

Based on these theorems, Fu et al. proposed an MILP modeling method for modular addition operation in [17].

The first feasibility condition $\alpha _{0} \oplus \beta _{0} \oplus \gamma _{0} = 0,$ in Theorem 1 can be represented in MILP model as Inequalities (2). To describe the second conditions of Theorem 1 and also the definition of $eq_i$ in the MILP model, Fu et al. considered the vectors $\left( {\alpha _{i-1},\beta _{i-1},\gamma _{i - 1},\alpha _{i},\beta _{i},\gamma _{i},\sim eq_{ i - 1} } \right)$ (for $i=1,\ldots ,n-1$) such that it is satisfied in the conditions. For example, the differential patterns (0, 0, 0, 1, 0, 1, 0) and (1, 0, 0, 0, 0, 1, 1) are possible patterns and the differential pattern (0, 0, 0, 1, 0, 0, 0) is an impossible pattern as ${\alpha _{i - 1}} = {\beta _{i - 1}} = {\gamma _{i - 1}} \ne {\alpha _i} \oplus {\beta _i} \oplus {\gamma _i}.$ Hence, 56 vectors were generated in each bit in total. Fu et al. used the "inequality generator()" function in the sage. geometry. polyhedron class of SAGE [43] and the greedy algorithm in [45] to get 13 linear inequalities satisfying all these 56 possible transitions. Then, given Theorem 2, it is sufficient to set the objective function as sum of $\sim eq_{i-1}$’s for $i=1,\ldots ,n-1$.

Hence, for n-bit words of the modular addition, the total number of the constraints contains $13(n - 1) + 4$ linear inequalities.

5.1.5 Searching for differential trails of SPECK

In this paper, we use the MILP model for related-key differential (RKD) cryptanalysis of reduced SPECK block cipher. Hence, first, we explain our strategy for searching the RKD trails and then present the searching result of SPECK.

5.1.6 Our searching strategy

We will give the details on how to search for the differential trails for SPECK. Based on the structure of the key schedule of SPECK, the maximum number of consecutive rounds of sub-keys that there are no differentials is 3 rounds. Based on the observation from our identified differential trail for the small number of rounds, we found that the differential probability is better when these 3 consecutive rounds of sub-keys lead to four consecutive rounds with zero input differential in the encryption datapath of SPECK. The details of this strategy are shown in Fig. 4. In this figure, we do not have any differentials in the input of i-th round to $(i+3)$-th round, such that i can be 2 to $r-3$ for r-round of SPECK.

Fig. 4

Our strategy for searching the differential trails of SPECK

The only non-linear operation in the SPECK round function is the modular addition, and the only key-dependent operation is the sub-key addition. Given that the sub-key addition happens after the modular addition, i.e., the cipher operation is completely predictable until this first sub-key addition, we can ignore the modular addition in the first round of the distinguishers.

5.1.7 Search results

In this section, we apply the technique described above in order to find a good differential trail of the reduced-round variants of SPECK.

5.1.8 Differential trails of SPECK32/64

Table 3 shows the RKD trail covering up to 15 rounds found by our model. To the best of our knowledge, the best published distinguisher trail so far has covered 12 rounds of SPECK32/64 with a probability of $2^{-25.57}$ for a weak key class of size $2^{4.92}$ [33]. Based on Table 3, our 13-round trail has a much better probability of $2^{-23.85}$ for a weak key class of size $2^{41}$.

Tables 9, 10, 11, 12, 13, and 14 in the Appendix A.1, show the differential trails covering 10 to 15 rounds found by our program.

Table 3 The comparison of our related-key differentials (RKD) with rotational-XOR (RX) result of [33] for SPECK32/64

Note that the authors of [33] wrote that “ We extended our search to 13-round trails and found that none exists, suggesting that a 12-round RX-trail is the longest possible one.” So, our result shows that the related-key differential is more powerful against SPECK32/64, compared to the rotational-XOR.

5.1.9 Differential trails of SPECK48/96

We found RKD trails covering up to 16 rounds for SPECK48/96. Table 4 shows the summary of searching result and also a comparison of our results with [33] for SPECK48/96. The trails for 11 to 16 rounds are shown in Tables 15, 16, 17, 18, 19, and 20 in the Appendix A.2.

Table 4 The comparison of our related-key differentials (RKD) with rotational-XOR (RX) result of [33] for SPECK48/96

5.1.10 Differential trails of SPECK64/128

For SPECK64/128, we successfully extended a distinguisher up to 17 rounds with a probability of $2^{-60.81}$ for a weak key class of size $2^{78}$. Our results for 13 to 17 rounds of SPECK64/128 are shown in Table 5. Tables 21, 22, 23, 24, and 25 in the Appendix A.3, show the RKD trail for these 13 to 17 rounds of SPECK64/128.

Table 5 The comparison of our related-key differentials (RKD) with rotational-XOR (RX) result of [33] for SPECK64/128

5.1.11 Differential trails of SPECK128/256

We present the distinguishers for 16 and 19 rounds of SPECK128/256 as shown in Table 6. Also, Tables 26 and 27 in the Appendix A.4, show the RKD trail for these 16 and 19 rounds of SPECK128/256.

Table 6 The comparison of our related-key differentials (RKD) with rotational-XOR (RX) result of [33] for SPECK128/256

5.1.12 Experimental verification

Here we intend to measure the accuracy of our estimates for the probabilities, and therefore, we first try to identify a weak key and then encrypt $2^{32}$ (for case of SPECK32/64) plaintexts, and measure the probability such that the differential feature is met.

We modeled the SPECK key schedule with the method described in Sect. 3 and fixed the key input differentials based on Tables 9, 10, 11, 12, 13, and 14 for rounds 10 to 15 of SPECK32/64, respectively. The time of solving the model to find the first weak key is shown in the third column of Table 7. Also in this table, the number of pairs that is satisfied in the encryption datapath are listed in the fifth column. This table shows that the results matched the theoretical predictions. For all versions of SPECK mentioned above, we tested whether the key differential trail is followed. For each version, we reported a weak key (see Tables 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, and 27 in Appendix A)

Table 7 The number of pairs for rounds 10 to 15 of SPECK32/64 with a weak key

5.1.13 Incompatible trails

It must be noted that the method mentioned in Sect. 3 can be very useful in most cases to find a weak key. For example, our MILP model to find the related-key trails can find a 14-round related-key trail with the input differential $(\mathtt {1805},\mathtt {1281})$, the output differential $(\mathtt {DA52},\mathtt {25AD})$, and the key input differential $(\mathtt {0201},\mathtt {4080}$, $\mathtt {1891},\mathtt {4A25} )$ with the data probability of $2^{-26}$ and key probability of $2^{-63}$ (key class size of $2^{1}$). In this case, our model, after 150 seconds shows that there are no keys which can satisfy the differentials of round keys. Note that without using our MILP method, we had to run the SPECK key schedule algorithm for $2^{64}$ times to know it. As a few other examples, in Table 8, we listed some of the differential trails for which there are not any key values to reach the differentials of round-keys.

Table 8 The list of some of the related-key differential trails of SPECK for which there are not any key values to satisfy the differential of key rounds

In fact, the independency assumption between the two continuous modular addition of the key schedule algorithm of SPECK is not enough to ensure the validity of the some of the differential trails. As an example, in the following lemma, we show that the modular additions used in the key schedule algorithm of SPECK are not independent. To show this, we consider one of the differential trails shown in Table 8 shows that the cause of the invalidity of that trail is the dependence of the modular additions.

Lemma 3

There are no right pair to satisfy the RK-difference of the sub-keys of 16 rounds of SPECK48/96 as shown in Table 29.

Proof

The proof is almost the same with proof of Lemma 2 and its detrails are presented in Appendix C. $\square$

6 Conclusion and future works

Thanks to the MILP method, in this study, we presented an efficient method to verify differential trails and also search for the right pairs. We applied our approach to the the previously known RX trails of SIMECK and SPECK family of block ciphers to verify their corectness. In addition, we presented related-key differential distinguishers on different variants of the SPECK block cipher and obtained longer distinguishers compared to the ones previously published. For each variant of the SPECK family of block ciphers, we presented several distinguishers. The longest distinguishers for SPECK32/64, SPECK48/96, SPECK64/128, and SPECK128/256, cover 15, 16, 17, and 19 rounds, respectively, which are working on a certain weak key class. In addition, we showed that the transitional probability over two consecutive modular addition operations in the key schedule structure of SPECK is not independent and our approach in this paper could find this case of the trails.

To the best of our knowledge, the current method for searching RX trails is based on SAT/SMT solvers and thus proposing an MILP-based method to find the RX trails can be considered as a future work. Also, based on our result, some previously reported RX trails of SPECK and SIMECK were incompatible, for instance, 11 and 12 rounds of SPECK32/64, 27 and 35 rounds of SIMECK48/96 and SIMECK64/128, respectively, therefore, finding compatible RX trails or prove nonexistence of them can be considered as another future work. In addition, in our analysis to find a good differential distinguisher for SPECK family, we noticed that most of the obtained trails are incompatible (especially in case of SPECK128/256). Thus, considering a direct approach to find a compatible differential trail may help improve the results (e.g., inspired by [15, 32]). As another work, considering our search to find a weak key in this paper may help find a collision in hash functions at a reasonable time. Besides, the results of this paper could be used to verify many differential trails which have been already considered as theoretical trails and we were not sure whether there could be any pair of inputs following that trail (as we did this for recent results on SPECK and SIMECK, in this article).

Appendices

A RKD trails of SPECK variants

1.1 A.1 RKD trails of SPECK32/64

Tables 9, 10, 11, 12, 13 and 14.

Table 9 10-round related-key differential trail in SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(2800,0200,0080,0001)}$

Table 10 11-round related-key differential trail in SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(0200,0080,0071,4A00)}$

Table 11 12-round related-key differential trail in SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(0080,0051,0008,1200)}$

Table 12 13-round related-key differential trail in SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=(4000,1880,0400,0009)$

Table 13 14-round related-key differential trail in SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(1480,04C0,0128,1002)}$

Table 14 15-round related-key differential trail in SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(4000,1580,0400,0009)}$

1.2 A.2 RKD trails of SPECK48/96

Tables 15, 16, 17, 18, 19 and 20.

Table 15 11-round related-key differential trail in SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(020000,004000,000882,120008)}$

Table 16 12-round related-key differential trail in SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(020000,004000,000882,120008)}$

Table 17 13-round related-key differential trail in SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(000200,0000C0,820008,081200)}$

Table 18 14-round related-key differential trail in SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(020000,004010,248801,102088)}$

Table 19 15-round related-key differential trail in SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(000010,000002,441000,}\mathtt {004090)}$

Table 20 16-round related-key differential trail in SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(000010,000020,00441000,} \mathtt {004090)}$

1.3 A.3 RKD trails of SPECK64/128

Tables 21, 22, 23, 24 and 25.

Table 21 13-round related-key differential trail in SPECK64/128 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(00000200,00000040,}\mathtt {00820008,08001200)}$

Table 22 14-round related-key differential trail in SPECK64/128 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(00000002,40000000,}\mathtt {08008200,00080012)}$

Table 23 15-round related-key differential trail in SPECK64/128 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(00000002,40000000,}\mathtt {08008200,00080012)}$

Table 24 16-round related-key differential trail in SPECK64/128 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)$ = $\mathtt {(00000200,00000040,}\mathtt {00820008,08001200)}$

Table 25 17-round related-key differential trail in SPECK64/128 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)$ = $\mathtt {(00000200,00000040,00820008,}\mathtt {08001200)}$

1.4 A.4 RKD trails of SPECK128/256

Tables 26 and 27.

Table 26 16-round related-key differential trail in SPECK128/256 with $(\varDelta l_2{,}\varDelta l_1{,}\varDelta l_0{,}\varDelta k_0)$ = $\mathtt {(0200000000000000,0040000000000010,0008000001248000,} \mathtt {1000080000002080)}$

Table 27 19-round related-key differential trail in SPECK128/256 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)$ = $\mathtt {(0200000000000000,0040000000000010,0008000001248000,} \mathtt {1000080000002080)}$

B Some of incompability RKD trails of SPECK variants

Tables 28, 29, 30 and 31.

Table 28 An incompatible differential trail for 14 rounds of SPECK32/64 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(0001,4000,0880,0025)}$

Table 29 An incompatible differential trail for 16 rounds of SPECK48/96 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)=\mathtt {(020000,004000,000882,} \mathtt {120008)}$

Table 30 An incompatible differential trail for 16 rounds of SPECK64/128 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)$=$\mathtt {(00208002,40000000,08000200,00080012)}$

Table 31 An incompatible differential trail for 21 rounds of SPECK128/256 with $(\varDelta l_2,\varDelta l_1,\varDelta l_0,\varDelta k_0)$= $\mathtt {(00500040000005A4,0008000800000034,} \mathtt {4001400100010400,0240014001000024)}$

C Manual verification of one of the incompatible RKD trails

Lemma 4

There are no right pair to satisfy the RK-difference of the sub-keys of 16 rounds of SPECK48/96 as shown in Table 29.

Proof

To find a contradiction in the key expansion datapath of the key differences of the trails in Table 29, we fixed the input differential of sub-keys in all 16 rounds. Our MILP model gives us an infeasible solution. This means that there are not any key values to satisfy the differential of round keys for 16 rounds of SPECK48/96 based on Table 29. After that, we tried to find the key values for fewer rounds by removing some last rounds. When we removed the fourteenth round, the MILP model found two key values whose differential was the differential of the key rounds for 14 rounds of SPECK48/96. So, the fourteenth round of key expansion datapath can be effective in finding a contradiction. Note that the left input differential of round 14 is the same as the left output differential of round 11 (see Fig. 5).

We denote the two n-bit vectors representing differentials at the input of modular addition in the round i where $i=11, 14$, as $\varDelta x^{i}=(\varDelta x_{n-1}^{i},\ldots ,\varDelta x_1^{i},\varDelta x_0^{i})$ and $\varDelta y^{i}=(\varDelta y_{n-1}^{i},\cdots ,\varDelta y_1^{i},\varDelta y_0^{i})$ and the n-bit output differential as $\varDelta z^{i}=(\varDelta z_{n-1}^{i},\ldots ,\varDelta z_1^{i},\varDelta z_0^{i})$ and the n-bit vectors representing carry differential as $\varDelta c^{i}=(\varDelta c_{n-1}^{i},\ldots ,\varDelta c_1^{i},\varDelta c_0^{i})$. It should be noted that based on the third condition of Inequality (3), the differential of carry bit $c^{i}$ can be obtained as $\varDelta c^{i}=\varDelta x^{i} \oplus \varDelta y^{i} \oplus \varDelta z^{i}$.

Fig. 5

Part of the 16-round incompatible differential trail of SPECK48/96 based on Table 29

Therefore, the input/output differentials and the carry differentials of modular additions for the 11-th and 14-th rounds based on Fig. 5, can be written as binary notation as follows.

$$\begin{aligned}\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} {\varDelta {x^{11}} = \mathrm{{100000000000000000000000,}}}&{}{\varDelta {x^{14}} = \mathrm{{100000000000011111101100,}}} \end{array}}\\ {\begin{array}{*{20}{c}} {\varDelta {y^{11}} = \mathrm{{100000010010010010000000,}}}&{}{\varDelta {y^{14}} = \mathrm{{001000111001000110000100,}}} \end{array}}\\ {\begin{array}{*{20}{c}} {\varDelta {z^{11}} = \mathrm{{000001111110110010000000,}}}&{}{\varDelta {z^{14}} = \mathrm{{100111001000110000100000,}}} \end{array}}\\ {\begin{array}{*{20}{c}} {\varDelta {c^{11}} = \mathrm{{000001101100100000000000,}}}&{}{\varDelta {c^{14}} = \mathrm{{001111110001101001001000}}\mathrm{{.}}} \end{array}} \end{array} \end{aligned}$$

As can be seen in Fig. 5, the modular addition operations in rounds 11 and 14 satisfy the conditions of Theorem 1 and they hold with probabilities of $2^{-9}$ and $2^{-17}$, respectively. Assuming independency, the differential probability of these two rounds should hold with probability of $2^{-26}$; however, we show that it is an incompatibility differential. To this end, by considering the modular addition operation for the 11-th round, we have $(\varDelta x_{13}^{11},\varDelta y_{13}^{11},\varDelta z_{13}^{11},\varDelta c_{13}^{11},\varDelta c_{14}^{11})=(0,1,1,0,1)$. It should be noted that the values that can have this differential must be selected from the set (6). According to the set (6), the following pairs have the differential $(\varDelta x_{13}^{11},\varDelta y_{13}^{11},\varDelta z_{13}^{11},\varDelta c_{13}^{11},\varDelta c_{14}^{11})=(0,1,1,0,1).$

$$\begin{aligned} \left\{ {({x_{13}^{11}},{y_{13}^{11}},{z_{13}^{11}},{c_{13}^{11}},{c_{14}^{11}})} \right\} \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,0,1,1,0)}\\ {(0,1,0,1,1)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(1,0,1,0,0)}\\ {(1,1,0,0,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

So, for each pair we get the condition

$$\begin{aligned} z_{13}^{11}={\overline{c}}_{14}^{11}, \end{aligned}$$

(14)

where ${\overline{c}}$ is the bit-wise NOT of c. Now, by considering the differential $(\varDelta x_{14}^{11},\varDelta y_{14}^{11},\varDelta z_{14}^{11},\varDelta c_{14}^{11}$, $\varDelta c_{15}^{11})=(0,0,1,1,1),$ for the 14-th bit, the following pairs can reach to this differential.

$$\begin{aligned} ({x_{14}^{11}},{y_{14}^{11}},{z_{14}^{11}},{c_{14}^{11}},{c_{15}^{11}}) \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,1,1,0,0)}\\ {(0,1,0,1,1)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(1,0,1,0,0)}\\ {(1,0,0,1,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

So, these pairs conclude the condition

$$\begin{aligned} z_{14}^{11}={\overline{c}}_{14}^{11}. \end{aligned}$$

(15)

By combining the Eqs. (14) and (8), we have

$$\begin{aligned} z_{13}^{11}=z_{14}^{11}. \end{aligned}$$

(16)

Now, in the modular addition operation for 14-th round, we have $(\varDelta x_{5}^{14},\varDelta y_{5}^{14},\varDelta z_{5}^{14},\varDelta c_{5}^{14},\varDelta c_{6}^{14})=(1,0,1,0,1).$ Thus, the following pairs will lead to the differential (1, 0, 1, 0, 1).

$$\begin{aligned} ({x_{5}^{14}},{y_{5}^{14}},{z_{5}^{14}},{c_{5}^{14}},{c_{6}^{14}}) \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,0,1,1,0)}\\ {(1,0,0,1,1)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(0,1,1,0,0)}\\ {(1,1,0,0,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

Hence, for these pairs, we can get the condition

$$\begin{aligned} x_{5}^{14}=c_{6}^{14}. \end{aligned}$$

(17)

Now, by considering the differential $(\varDelta x_{6}^{14},\varDelta y_{6}^{14},\varDelta z_{6}^{14},\varDelta c_{6}^{14},\varDelta c_{7}^{14})=(1,0,0,1,0)$ for the 6-th bit, the following pairs will lead to this differential.

$$\begin{aligned} ({x_{6}^{14}},{y_{6}^{14}},{z_{6}^{14}},{c_{6}^{14}},{c_{7}^{14}}) \in \left\{ {\left\{ {\begin{array}{*{20}{c}} {(0,0,1,1,0)}\\ {(1,0,1,0,0)} \end{array}} \right\} ,\left\{ {\begin{array}{*{20}{c}} {(0,1,0,1,1)}\\ {(1,1,0,0,1)} \end{array}} \right\} } \right\} . \end{aligned}$$

Therefore, we have the condition

$$\begin{aligned} x_{6}^{14}={{\overline{c}}}_{6}^{14}. \end{aligned}$$

(18)

By combining the Eqs. (17) and (18), we have

$$\begin{aligned} x_{5}^{14}={\overline{x}}_{6}^{14}. \end{aligned}$$

(19)

Since $x^{14} = (z^{11}\ggg 8)$ (see Fig. 5), we have $z_{13}^{11}=x_{5}^{14}$ and $z_{14}^{11}=x_{6}^{14}$. Hence, by considering the Eqs. (16) and (19), we reach a contradiction. $\square$