Keywords

1 Introduction

Block ciphers, stream ciphers, and hash functions are the fundamental symmetric cryptographic primitives that are at the base of almost all cryptographic protocols. One of the most successful set of techniques to evaluate their security are techniques based on higher-order derivatives.

Higher-order derivatives were first considered in the context of symmetric cryptography by Lai [Lai94] and shown by Knudsen [Knu95] to attack weaknesses not covered by differential cryptanalysis, and successfully used to break a cipher design [JK97]. A higher-order derivative in the context of cryptography is the discrete equivalent of higher-order derivatives of multivariate continuous functions. The cryptographic primitive can be seen as a vectorial Boolean function where a higher-order derivative evaluates this function at a given point with respect to some directions/subspace. Such a derivative can for example be used to find the coefficients of the monomials of the algebraic normal form (ANF) of a cryptographic primitive.

An important category of higher-order attacks is integral cryptanalysis. This type of cryptanalysis appeared first in the Square attack [DKR97a], and was later generalised to be apply to other ciphers as well ([KW02, BS10]). In integral cryptanalysis, the goal is to find a set of input bits and a set of output bits, such that when taking the sum over a set of input messages taking all possible values in the selected input bits and arbitrary but constant values in the other input bits, the sum will be balanced in the selected output bits. This can be described as a higher-order derivative that can be taken at any point and evaluates to zero in the specified output bits.

Originally such property was derived using arguments based on the structure of the primitive but Yosuke Todo demonstrated in his EUROCRYPT 2015 paper [Tod15b] a novel method to derive integral distinguishers using the so-called division property formalism whose effectiveness he demonstrated with an attack on full-round Misty [Tod15a]. The technique originally being used on words of at least four bits, has since been applied to bit-based designs as well, albeit at a higher computational cost [TM16].

Another type of higher-order attacks are so-called cube attacks [Vie07, DS09]. In these attacks the cryptographic primitive is viewed as a vectorial Boolean function in both public and secret input bits. By finding coefficients of terms in the public bits that are linear in the secret bits, it is possible to derive a set of linear equations that we can solve to extract the secret input bits. This technique has successfully been applied to stream ciphers and hash functions [DS11, DMP+15].

Contributions. This paper presents a new framework to analyse the security of cryptographic primitives with respect to the bit-based division property by providing a simple way to find distinguishers and testing the number of rounds required for no such distinguisher to exist. We take a look at how finding division property distinguishers can be efficiently automated. To this end, we elaborate how the bit-based division property can be mapped to conditions on the state bits which in turn maps easily to a SAT problem.

Our tool focuses especially on the usability and allows to describe the cryptographic primitives at a high level by providing commonly used operations like S-boxes, linear layers, bit-permutations or modular addition. This completely removes the need of constructing any domain specific models like previous search strategies [XZBL16, SWW17, ZR17].

In order to demonstrate the usability of our tool we implemented 30 primitives following different design strategies. We then use our tool to find several new integral distinguishers, provide a bound for which number no such distinguishers exist in our model and also evaluate for which design strategies our approach becomes computationally infeasible.

In particular we find the following new results:

  • We provide the first bit-based integral distinguishers for the permutations used in ChaCha (6 rounds), Chaskey (4 rounds) and Salsa (6 rounds). We further show that for one more round no distinguisher of this type exists.

  • For DES we show that by using the bit-based division property we can improve upon the word-based division property distinguishers by Todo [Tod15b] and add one round. We also show that for 8 rounds no such distinguishers exist.

  • We present the first integral distinguisher for both Mantis (3 forward, 2 backward rounds) and several variants of Qarma (2 forward, 2 backward rounds).

  • For the SM4 block cipher we can show a distinguisher for 12 rounds and that no bit-based division property distinguisher exists for 13 rounds. This improves the best previously known integral distinguisher by 4 rounds [LJH+07].

  • We find a distinguisher for 17 rounds of LBlock, which improves the best previously known results by one round [XZBL16].

  • We present 9-round distinguishers for GIFT-64 which improve upon the data complexity of the distinguishers provided by the designers [BPP+17].

  • For RoadRunner we are able to extend the distinguishers found by the authors [BS15] by one additional round.

For several other primitives we provide a bound at which no bit-based division property distinguishers exists in our model. Furthermore, we present an efficient algorithm to find distinguishers with reduced data complexity by only covering the search space which can actually lead to distinguishers.

Software. We place the tool developed for this paper into the public domain and it is available at https://github.com/kste/solvatore.

Related Work. The division property has been applied to a large variety of cryptographic primitives and has led to significant improvements [Tod15b, Tod15a] over classical integral attacks in some cases. With the extension of the division property to bit-based designs [TM16] the technique can be applied to a larger class of cryptographic primitives. However finding distinguishers with this approach is a difficult task and requires a lot of effort.

The first automated approach for finding bit-based division property distinguishers was presented in [SWW16] and is based on reducing the problem to mixed integer linear programming (MILP). This simplifies the search for distinguishers and allows to apply the bit-based division property to a larger class of cryptographic primitives. Another automated approach based on constraint programming has been proposed in [SGL+17] to find integral distinguishers for Present . In the paper the authors show that this approach can have a better performance than the MILP based technique. The search for ARX and word-based division property has been dealt with in [SWW17] by using SAT resp. SMT solvers.

2 Division Property and Division Trails

The methodology of division properties was devised by Yosuke Todo in his EUROCRYPT 2015 paper [Tod15b]. We elaborate this methodology here in the setting where the words are single bits, i.e., when applied as bit-based division property. While using the original formalism, we will look at it from a slightly different angle to simplify the discussion. For the division property over larger word sizes, we refer to the original paper.

2.1 Background

The formalism of division properties belongs to the family of attack vectors collectively named integral cryptanalysis. The goal of integral cryptanalytic techniques is to find a set of input texts such that the sum of the resulting output texts evaluates to zero in some of the bits. If such a property can be found it directly yields a distinguisher which often can be turned into a key recovery attack.

The most common sets of input texts that are used are those that are equal in some bit positions and take all possible combination of values in the remaining bit positions. The first attack that successfully used this attack vector is the Square attack [DKR97a] on the block cipher Square that is equally applicable to the Advanced Encryption Standard (AES).

There are two main methods that are used to derive an integral distinguisher: structural properties and algebraic degree bounds. In the Square attack and subsequent generalizations [BS01] the integral property could be derived by only looking at structural properties of the cipher such as the SPN or Feistel structure without taking much of the cipher details into consideration (such as concrete S-box, concrete linear layer).

Later it was recognised that these kinds of integral distinguishers correspond to discrete derivatives [Lai94] where the derivative is taken with respect to the active input bits, i.e., those that are varied. As such the structural techniques are a way to determine output bits whose polynomial representations do not contain terms that include all active input bits simultaneously. Taking the derivative with respect to these active input bits will thus necessarily evaluate to zero in these output bits.

The second major technique that is used to derive integral distinguishers uses this view of integral distinguishers as derivatives. By determining upper bounds on the algebraic degree of the polynomials of the output bits, we can determine that derivatives of sufficient degree have to evaluate to zero. Similar to the structural method, the methods used to bound the degree usually ignore large parts of the implementation details, for example by just looking at the degree of rounds and multiplying these.

The division property is an improvement with respect to this situation as it manages to take more implementation details of the cipher into consideration. The downside to this is an increased cost of finding the distinguishers.

2.2 Formalism of Bit-Based Division Properties

In the bit-based division property methodology, the goal is to find, given a set of chosen active input bits, those output bits whose polynomial representations do not contain terms that feature all of these active bits simultaneously. While this could principally be done by simply calculating the exact polynomial representations of the output bits, this is computationally infeasible in all but toy examples. With division properties we use an approximation instead that guarantees to only find valid distinguishers but might fail to find all distinguishers.

In this approximation, we continually track which bits of the state would need to be multiplied to generate a bit whose polynomial representation can contain terms of all active bits. Let us consider an initial state of four bits \((x_0, x_1, x_2, x_3)\) where we activate bits \(x_1\) and \(x_2\), i.e., we are interested in which state bits we would need to multiply to create a term that contains both bits. For this initial state the minimal way of generating such a term is by multiplying those two bits directly. We write this combination as the choice vector (0, 1, 1, 0).Footnote 1

If we now add \(x_1\) to \(x_3\), we get the new state \((x_0, x_1, x_2, x_3+x_1)\). Now we can generate a term that contains both \(x_1\) and \(x_2\) in two different minimal ways: first again by multiplying the second and third bit or by multiplying the third and the last bit. These correspond to the choice vectors (0, 1, 1, 0) and (0, 0, 1, 1).Footnote 2 The only original choice vector (0, 1, 1, 0) has thus been transformed to two choice vectors by the application of the addition.

If we now applied another operation to this state, each of the choice vectors is transformed to other minimal choice vectors, and by iterating this process a tree of minimal choice vectors is spanned whose final nodes are the minimal choice vectors of output bits whose multiplication can create a term that contains all active input bits.

To determine whether a minimal choice vector can be reached from the initial choice vector of active bits, we need to determine whether a path exists in this tree from the initial choice vector to the output choice vector. We will refer to such path as a division trail. In particular, to determine whether a specific output bit is zero when evaluating the derivative with respect to the active bits, we need to determine whether the choice vector that only chooses this output bit is reachable. If it is not reachable, we know that this output bit cannot have terms in its polynomial representation that contain all active bits simultaneously and thus the derivative has to evaluate to zero. Should the choice vector be reachable though, nothing definite can be said about the derivative.

2.3 Rules of Choice Vector Propagation

To trace a division trail of minimal choice vectors, we need to know how these minimal choice vectors of state bits are transformed to new choice vectors under the application of operations. In the following we will shortly discuss the application of XOR, AND, bit-copying and S-boxes. As the influence of the operations is local, it is sufficient to restrict the discussion to those bits involved in the operation.

Bit-Copying. Let us take a look at the scenario where we have two state bits, and the value of the first bit is copied to the second bit. There are four possible original choice vectors: (0, 0), (1, 0), (0, 1), and (1, 1). The first choice vector implies that to generate a term that can contain all active bits, we don’t need to multiply any of the two bits. So clearly we still do not need to multiply any of the bits after copying the first bit onto the second, leading to the transition \((0,0)\rightarrow (0,0)\).

In the case of (1, 0), we need the first bit in the product to generate a term with all active bits but the second one is not required. Thus after copying, we can choose either the first or the second bit (both would also be possible but not minimal). We thus have the two transitions: \((1,0)\rightarrow (1,0)\) and \((1,0)\rightarrow (0,1)\).

Now in the case of (1, 0) and (1, 1), the second bit is needed in the product to create a term with all active bits. As it is copied over, it is no longer possible after copying to create this term and thus no valid transitions exist.

XOR. Now for the case where there are two state bits and the first is XORed onto the second. Again we have to look at the four cases (0, 0), (1, 0), (0, 1), and (1, 1). As with bit copying, in the case of (0, 0), the bits are not necessary in the product, so they are not necessary after the addition as well. This leads to the transition \((0,0)\rightarrow (0,0)\).

In the case of (1, 0), the first bit value is needed in the product. After the addition, the bit value is also present as part of the sum in the second bit. We can thus either choose the first or the second bit in the product, leading to the transitions \((1,0)\rightarrow (1,0)\) and \((1,0)\rightarrow (0,1)\).

When we have the case (0, 1), the second bit value is needed in the product. As it is still only present in the second bit after the addition, the only valid transition here is \((0,1)\rightarrow (0,1)\).

Finally, in the case of (1, 1), the product of both bits is needed to create a term with all active bits. Although the second bit contains both original bit values after the addition, it only does so as a sum while we need the product of both. Thus also after the addition, we have to choose both bits, leading to the transition \((1,1)\rightarrow (1,1)\).

AND. If we now have again two state bits and we multiply the first onto the second, the situation is analogous to the case of the XOR except if the choice vector before the multiplication is (1, 1). In this case the product of both bit values is needed to create a term of all active bits. As the multiplication creates exactly this product in the second bit, the only minimal transition here is \((1,1)\rightarrow (0,1)\).

S-Boxes. The easiest way to see how choice vectors are transformed by an S-box is to look at the polynomial representation of the S-box, i.e., the algebraic normal form (ANF). It is tedious but straightforward to deduce the valid output choice vectors for a given input choice vector using the ANF. It can hence be easily automated and we only need to do this once for an S-box.

3 Solvatore - Automated Finding of Integral Properties

Finding integral distinguishers using division properties is a difficult task. Especially for bit-based designs the analysis often requires extensive manual work which is prone to errors. Automatic tools can be very useful and simplify the analysis of cryptographic primitives, allowing us to explore a larger set of attack vectors. On the other hand they can also be very useful in the design process of cryptographic primitives, to optimise parameters and quickly test different design strategies.

In the following, we present our automated tool Solvatore , which simplifies the search for bit-based division property distinguishers by providing a framework for implementing a large variety of cryptographic primitives. One of the main focuses of the framework is to not only automate finding the bit-based division property distinguishers, as done in previous work  [XZBL16, SWLW16, SWW17], but also to completely abstract away the need for dealing with generating models for the primitives or requiring any domain specific knowledge. This makes it much simpler and less error-prone compared to other approaches to add new primitives to the framework and in general it is far easier to implement a primitive in our tool than writing a standard C implementation as many details can be omitted.

Currently our framework supports the following operations to construct cryptographic primitives:

  • Bit operations: bit-copying, and, and xor.

  • Arbitrary S-boxes.

  • Linear layers using matrix multiplication over arbitrary fields.

  • Modular Addition.

  • Bit-permutations.

  • Generic cell permutations for ShiftRows or Midori-like constructions.

As an example the full description of Present is given in Appendix A which only requires to define the S-box, bit-permutation and on which bits those are applied. In order to analyse the security of Present against the bit-based division property our tool provides functions for checking whether an output bit is balanced for a given choice vector.

In the following we show how we can reduce the problem of finding a division trail to a satisfiability problem. For this we have to construct a Boolean formula which is satisfiable if and only if it forms a valid division trail.

3.1 Modeling Division Property Propagation with SAT

The Boolean satisfiability problem (SAT) is a well known problem from computer science. The problem is to decide whether there exists an assignment of variables in a Boolean formula in conjunctive normal form (CNF) such that the formula evaluates to true. While the problem is known to be NP-complete, the SAT instances we will construct here are very structured and can often be solved quickly in practice by modern SAT solvers. In the following we show how to reduce the problem of finding division trails to a SAT problem and how this can be useful in the cryptanalysis of cryptographic primitives.

First, we introduce a variable for each bit of the choice vector \(S^i = (s_0, \ldots , s_{n-1})\) after the ith operation applied to the state where n is the size of the state. The next step is to define how the choice vector can propagate through different Boolean functions which occur in the round functions of cryptographic primitives. The rules for this have been explained in Subsect. 2.3 and have also been studied in [Tod15a, Tod15b]. We therefore focus here on how we can construct a Boolean formula in CNF which is SAT if and only if the assignment of the variables forms a valid transition of choice vectors.

Bit-Copying. The copy operation copies a bit a to an output bit b, and all valid transitions of choice vectors are given by

$$\begin{aligned} {\mathbf {copy}}(a_\text {old}, b_\text {old})&\rightarrow \{(a_\text {new}, b_\text {new})\}\\ {\mathbf {copy}}(0, 0)&\mapsto \{(0, 0)\}\\ {\mathbf {copy}}(1, 0)&\mapsto \{(1, 0), (0, 1)\}. \end{aligned}$$

The set of clauses \(C_{\text {copy}}\) which form a Boolean formula which is SAT iff \((a_\text {old}, b_\text {old}) \xrightarrow {\text {copy}} (a_\text {new}, b_\text {new})\) is given by

$$\begin{aligned} \begin{aligned} C_{\text {copy}} = \{&(\lnot b_\text {old}), (\lnot a_\text {old} \vee b_\text {new} \vee a_\text {new}), (a_\text {old} \vee \lnot b_\text {new}),\\&(a_\text {old} \vee \lnot a_\text {new}), (\lnot a_\text {new} \vee \lnot b_\text {new})\}. \end{aligned} \end{aligned}$$
(1)

And. The and operation corresponds to the result of \(a \wedge b \rightarrow b\). The valid transitions are given by

$$\begin{aligned} \mathbf {and}(a_\text {old}, b_\text {old})&\rightarrow \{(a_\text {new}, b_\text {new})\}\\ \mathbf {and}(0, 0)&\mapsto \{(0, 0)\}\\ \mathbf {and}(0, 1)&\mapsto \{(0, 1)\}\\ \mathbf {and}(1, 0)&\mapsto \{(1, 0), (0, 1)\}\\ \mathbf {and}(1, 1)&\mapsto \{(0, 1)\}. \end{aligned}$$

Just as for the copy operation, translating this to a SAT sentence is straightforward and gives the following set of clauses

$$\begin{aligned} \begin{aligned} C_{\text {and}} = \{&(a_\text {old} \vee \lnot a_\text {new}), (\lnot b_\text {old} \vee b_\text {new}), (\lnot b_\text {new} \vee \lnot a_\text {new}),\\&(\lnot a_\text {old} \vee b_\text {new} \vee a_\text {new}), (a_\text {old} \vee b_\text {old} \vee \lnot b_\text {new}). \end{aligned} \end{aligned}$$
(2)

Xor. The xor operation corresponds to the result of \(a \oplus b \rightarrow b\). The valid transitions are given by

$$\begin{aligned} \mathbf {xor}(a_\text {old}, b_\text {old})&\rightarrow \{(a_\text {new}, b_\text {new})\}\\ \mathbf {xor}(0, 0)&\mapsto \{(0, 0)\}\\ \mathbf {xor}(0, 1)&\mapsto \{(0, 1)\}\\ \mathbf {xor}(1, 0)&\mapsto \{(1, 0), (0, 1)\}\\ \mathbf {xor}(1, 1)&\mapsto \{(1, 1)\} \end{aligned}$$

which corresponds to the following clauses

$$\begin{aligned} \begin{aligned} C_{\text {xor}} = \{&(a_\text {old} \vee \lnot a_\text {new}), (\lnot b_\text {old} \vee b_\text {new}), (b_\text {old} \vee \lnot b_\text {new} \vee \lnot a_\text {new}),\\&(\lnot a_\text {old} \vee a_\text {new} \vee b_\text {new}), (b_\text {old} \vee a_\text {old} \vee \lnot b_\text {new}),\\&(\lnot b_\text {old} \vee \lnot a_\text {old} \vee a_\text {new}). \end{aligned} \end{aligned}$$
(3)

S-boxes. As described in Subsect. 2.3, the transition rules for S-boxes can easily be deduced automatically. The rules create a truth table for involved variables which can be transformed to a CNF using standard methods.

Linear Layers. Many popular designs, like the AES, use a complex linear layer in order to get good diffusion. These linear layers are often represented as \(d \times d\) matrices over some field \(\mathbb {F}_2^k\). In order to model the trail propagation we can represent these transformations as \(kd \times kd\) matrices over \(\mathbb {F}_2\), which then can be decomposed into the basic copy and xor operations.

In order to simplify the description of such linear layers in our tool, we implemented this decomposition and it is only required to provide the irreducible polynomial for the field \(\mathbb {F}_2^k\) and the matrix. From the irreducible polynomial it is possible to deduce the \(k\times k\) matrices that represent the elements of \(\mathbb {F}_k\) as matrices over \(\mathbb {F}_2\). Substituting these matrices in the original matrix over \(\mathbb {F}_k\) now creates the \(nk\times nk\) binary matrix.

Modular Addition. Modular addition is used as a non-linear component in ARX-ciphers like HIGHT, LEA, and SPECK. We can use the same approach as [SWLW16] to decompose the modular addition into xor and and. Let z, x, y be n bit-variables with \(z_i,y_i,x_i\) as the ith bits, counting from the least significant bit, and \(z= x\boxplus y\). The modular addition modulo \(2^n\) is given by:

$$\begin{aligned}&z_i = x_i \oplus y_i \oplus c_i\\&\text {where}\\&c_i = x_{i-1}y_{i-1} \oplus (x_{i-1}\oplus y_{i-1})c_{i-1} \text { for } i>0 \\&c_0 = 0 \end{aligned}$$

So far we have assumed that both x, y are variables, however in some ciphers one of them is a constant, e.g. a round key. Since we can ignore xor and and with a constant we get the following expressions.

$$\begin{aligned}&z_i = x_i \oplus c_i\\&\text {where}\\&c_i = x_{i-1} \oplus x_{i-1}c_{i-1} \text { for } i>0 \\&c_0 = 0 \end{aligned}$$

Similar, if we want to find a distinguisher on a cipher like Bel-T or the inverse of an ARX-cipher we also need modular subtraction. To do modular subtraction we can use the fact that

$$\begin{aligned} x\boxminus y = x \boxplus (-y)=x \boxplus (2^n-y) = x \boxplus ((2^n-1)-y)\boxplus 1=x \boxplus \overline{y} \boxplus 1 \end{aligned}$$
(4)

Since the NOT operation has no effect on whether a bit is balanced or not we can omit it to get \(x\boxminus y = x \boxplus y \boxplus 1\). This means that we can do modular subtraction with one modular addition and one constant addition.

3.2 Finding Integral Distinguishers

In order to find useful integral properties of a cipher, we have to propagate an initial choice vector \(S^0\) and check whether it is impossible to reach certain choice vectors \(S^{r}\) after r rounds. If we can show that an output choice vector that is everywhere zero except for a single 1 in one bit is unreachable, we know that this bit has to be balanced.

In particular we are often interested in whether any bit in the output will be balanced. This corresponds to showing that at least one of the vectors in the set

$$\begin{aligned} S^{r} \in \{w \in {{\,\mathrm{\mathbb {F}}\,}}_2^n\ |\ {{\,\mathrm{\mathbf {hw}}\,}}(w) = 1\}. \end{aligned}$$
(5)

is unreachable, where \({{\,\mathrm{\mathbf {hw}}\,}}(x)\) is the Hamming weight of the vector.

Contrarily, we can also use this approach to show the absence of a bit-based division property distinguisher in our model. Checking all possible options for the starting choice vector would be (for most primitives) computationally infeasible. Fortunately it is sufficient to show for all starting choice vectors in the set

$$\begin{aligned} S^0 \in \{w \in {{\,\mathrm{\mathbb {F}}\,}}_2^n\ |\ {{\,\mathrm{\mathbf {hw}}\,}}(w) = n - 1\}. \end{aligned}$$
(6)

that all choice vectors in the set in Eq. 5 are reachable. This works because the balancedness of the output bits is preserved when we exchange the input choice vector with any vector greater than it (with respect to the above ordering).

We will use the following notation to simplify the description of the distinguishers found later in the paper. The set of active bits will be denoted as

$$\begin{aligned} A = \{i\ |\ S^0_i = 1,i=0,\ldots ,n-1\} \end{aligned}$$
(7)

and correspondingly the set of constant bits as

$$\begin{aligned} \overline{A} = \overline{\{i\ |\ S^0_i = 1,i=0,\ldots ,n-1\}} = \{i\ |\ S^0_i = 0,i=0,\ldots ,n-1\}. \end{aligned}$$
(8)

The set of bits which are balanced at the output is denoted as B. We can now describe a distinguisher, for a function f, as

$$\begin{aligned} A \xrightarrow {f} B. \end{aligned}$$
(9)

If a valid division trail from A to B exists we will also use the more compact notation \({{\,\mathrm{\mathbf {DP}}\,}}(A) = B\) if the function is clear from context.

Note that while the notation for the set of active bits at the input and the balanced bits at the output looks very similar it conveys a very different meaning in the context of the division property. For a range of bits \(s_i, s_{i+1}, \ldots , s_j\) we will use the notation \(s_{i-j}\).

4 Distinguishers and Bounds

We implemented a variety of cryptographic primitives in Solvatore to demonstrate the versatility of our tool and the ease of adding primitives with different design principles.

  • SPN: Gift, LED, Midori, Photon, Present, Skinny, Spongent

  • ARX: BelT, ChaCha, Chaskey, LEA, HIGHT, Salsa, Sparx, Speck

  • Feistel: DES, LBlock, Misty, Roadrunner, Skipjack, SM4, Twine

  • Reflection: Mantis, Prince, Qarma

  • Bit-sliced: Ascon, Rectangle

  • LFSR-based: Bivium, Trivium, Kreyvium

We will first go over the general methodology and after that over the results on the different primitive classes obtained using Solvatore . This includes both bit-based division property distinguishers and finding the number of rounds at which no such distinguisher exists anymore. All results have been obtained on an Intel Core i7-4770S running Ubuntu 17.10 using the Python interface to CryptoMiniSat 5.0.1. Several examples for distinguishers we found are given in Appendix B.

4.1 Methodology

Finding a Bound. As a first step we try to find the number of rounds \(r^*\) at which no bit-based division property distinguisher in our model exists. This is done by testing all set of active bits of type

$$\begin{aligned} A_j = \{i\ |\ i \in {{\,\mathrm{\mathbb {Z}}\,}}_n \setminus {j}\}\quad \forall j \in {{\,\mathrm{\mathbb {Z}}\,}}_n\!. \end{aligned}$$
(10)

This corresponds to all vectors where a single bit is constant. If for all possible choices the set of balanced bits \(B_j = {{\,\mathrm{\mathbf {DP}}\,}}(A_j)\) is empty we know that no such distinguisher exists for \(r^*\) rounds.

Reducing Data Complexity. In order to reduce the data complexity for the distinguishers covering the most rounds we use different strategies. The naive approach would be to increase the number of constant bits c, try out all possible combinations and check whether the resulting set of balanced bits B is not empty. This might work in some cases however the complexity increases very quickly as we have to test all \(\left( {\begin{array}{c}n\\ c\end{array}}\right) \) possible choices.

This can be improved by only testing those combinations of constant bits which can actually lead to non-empty sets B. First, we compute the set of constant bits

$$\begin{aligned} G_1 = \{j\ |\ {{\,\mathrm{\mathbf {DP}}\,}}(A_j) = B_j \wedge (|B_j| > 0)\quad \forall j \in {{\,\mathrm{\mathbb {Z}}\,}}_n\} \end{aligned}$$
(11)

for which at least one of the bits after r rounds is balanced, similar to the case where we try to find the bound. Next, we look at all combinations of two elements of \(G_1\) which share at least one balanced bit

$$\begin{aligned} G_2 = \{\{i, j\}\ |\ (i \ne j) \wedge (|{{\,\mathrm{\mathbf {DP}}\,}}(A_i) \cap {{\,\mathrm{\mathbf {DP}}\,}}(A_j)|) > 0, \forall i, j \in G_1\}. \end{aligned}$$
(12)

We can continue the last step in a similar way until \(G_i\) is empty by testing all combinations of the sets of bits in \(G_i\) repeatedly. Note that in the next step we would not have single indices but sets of indices and we therefore look whether the union of these sets of constant bits lead to a non-empty set B. Another advantage of this approach is that we only need to test those bits for the balancedness property which were already balanced in the last iteration.

In each step the elements in \(G_i\) are a set of constant bits which will have at least one balanced bit in the output after r rounds. This approach improves the complexity of finding distinguishers with lower data complexity significantly, but often it is still computationally infeasible to find an optimal distinguisher. For more structured designs it often helps to look at the word level and only look at maximizing the number of constant words as there are fewer combinations which we have to check.

Table 1. Results from the optimised search for Spongent-88. Combinations are the number of pairs (i, j) in the sets \(G_i\) which share bits in their corresponding sets \(B_i\) and\(B_j\).
Full size table

4.2 SPN

We will use 9 rounds of Spongent-88 as an example to show the benefits of the optimised search for a distinguisher with lower data complexity. In order to estimate the complexity we will count for how many choice vectors we would have to compute the set of balanced bits B. Using the optimised search we only have to test 1819 choice vectors (see Table 1) to find distinguishers with up to 4 constant bits and exclude any distinguisher with 5 constant bits. Using the naive approach we would have to test 679120 choice vectors to find all distinguishers up to 4 bits and check \(\left( {\begin{array}{c}128\\ 5\end{array}}\right) \) combinations to exclude the existence of any further distinguishers.

For Skinny-64 we can find a distinguisher with the same data complexity as the one given by the authors [BJK+16] with one additional balanced bit and show that no distinguishers exist for 11 rounds.

For GIFT-64 we use our optimal approach and no better distinguisher exists. We can find a 9-round distinguisher similar to the one by the authors [BPP+17], but also distinguishers with a lower data complexity. For GIFT-128 finding distinguishers takes significantly longer and we were only able to find a distinguisher with high data complexity similar to the original one.

Table 2. Overview of our distinguishers and bounds for SPN-based designs.
Full size table

For several variants of PHOTON we can find distinguishers with low data complexity by searching for combinations of constant words. However for more rounds the search time increases quickly and we are not able to improve any results. The complex linear layer generates a large number of clauses which seems to be the main limiting reason (Table 2).

4.3 ARX

First we look at the permutation used in the Chaskey MAC [MMH+14]. We can find a distinguisher for 3 rounds with only two constant words, one with high complexity for 4 rounds and show that no bit-based division property distinguishers for 5 rounds exist. This confirms the claim by the authors that Chaskey is likely to resist this type of attacks. Considering the construction used for the MAC it seems infeasible to mount an attack based on the 4-round distinguisher.

The large state of Salsa and ChaCha make it difficult to adopt our approach for reducing the data complexity. We therefore keep whole words constants and try to find the maximum number. For 6 rounds of Salsa the only distinguisher which exists keeps the first word constant and the one for ChaCha has only a single constant bit. In both cases no distinguisher exists for 7 rounds. On the actual mode in which Salsa and ChaCha are used as a stream cipher we can only control the 64-bit nonce in a single block. In this setting there are no bit-based division property distinguisher for 4 rounds of Salsa and 2 rounds of ChaCha.

We can also confirm the results from [SWW17] using our optimal search algorithm for Hight, LEA and Speck. We noticed that Solvatore performs significantly better for finding these distinguishers even though we use the same SAT solver. It only took us 28/195/51 seconds compared to 15/30/6 minutes for finding the optimal distinguishers for Hight/LEA/Speck. This gap could be explained by the slightly different model resp. using a better search strategy.

Bel-T is a block cipher which has been adopted as a national standard in the Republic of Belarus and combines S-boxes with modular addition. There is only a very limited amount of cryptanalysis available [JP15] (also provides an English description of the algorithm). We provide the first analysis with respect to integral attacks for Bel-T and can find a fairly efficient distinguisher for 2 rounds while showing that none exist for 3 rounds.

In the case of Sparx we can confirm the results by the authors [DPU+16]. The full summary of the results for ARX-based primitives can also be found in Table 3.

Table 3. Overview of our distinguishers and bounds for ARX-based designs.
Full size table

4.4 Feistel

For DES we improve the best bit-based division property distinguisher [Tod15b] by one round. The original distinguisher for DES also uses the division property but only word-based which makes this improvement possible.

One of the most successful applications of the division property is the full break of Misty [Tod17]. It is also based on the analysis on the word level so one might suspect that it can be improved by looking at the bit-based division property. We tried to find the same distinguishers as in the original attack automatically however the complexity seems too high without further optimizations. We could only find a distinguisher for 3 rounds.

The best integral distinguisher on SM4 covers 8 rounds [LJH+07]. By using the bit-based division property we can improve those distinguishers to 12 rounds, although at a high complexity. We further can show that no such distinguishers exist for 13 rounds.

In the case of LBlock we are able to extend the distinguisher found with MILP [XZBL16] by one additional round and for Roadrunner we can find a 5-round distinguisher which also covers one more round than the best known distinguisher [BS15].

For all variants of Simon and Simeck we can reproduce the results from [XZBL16], show that these have the lowest data complexity and that there are no distinguisher in our model for more rounds (Table 4).

Table 4. Overview of our distinguishers and bounds for Feistel networks.
Full size table

4.5 Reflection

Block ciphers based on the reflection design strategy, introduced by PRINCE, are a popular choice for low-latency designs. We will denote the number of rounds as \(f + b\), where f are the rounds before the middle layer and b the rounds after the middle layer (see Table 5).

For PRINCE we can find a bit-based division property distinguisher with the same complexity as the best higher-order differential given in [RR16] and show that for one additional round none exist. Very similar distinguisher also exist for MANTIS with the only difference being that one can extend those by one round in forward and backwards direction. The distinguishers for QARMA can cover a similar number of rounds although at a much higher data complexity.

Table 5. Results on reflection ciphers.
Full size table
Table 6. Results on bit-sliced ciphers.
Full size table

4.6 Bit-Sliced

In this category we look at two LS-designs (see Table 6). The permutation used in the authenticated encryption scheme Ascon and the block cipher Rectangle. For Ascon we can improve the data complexity of the 5 round distinguisher [Tod15b] by a factor of 4, however for more rounds we could not improve any results as the computations takes too long. For Rectangle we are able to show that no distinguisher exists for 10 rounds and find the already known 9-round distinguisher from [XZBL16].

4.7 LFSR-Based

We looked at three LFSR-based stream ciphers which share a similar structure. The active bits are taken over the choice of IV and our distinguishers here checks whether the output bit of the key stream is balanced after r rounds. It is very likely that there are more bits balanced in the state, but we can only distinguish the key stream if the resulting key stream bit is also balanced.

While we could find some distinguishers the time it takes to find a balanced output bit of the keystream quickly increases and other approaches seem to be more promising for constructing distinguisher based on the division property for this type of ciphers [TIHM17] (Table 7).

Table 7. Results on LFSR-based stream ciphers.
Full size table
Fig. 1.
figure 1

Overview of the fraction of rounds required before we can show that no bit-based division property distinguishers exist in our model.

Full size image

4.8 Overview

Using Solvatore we were able to demonstrate several new distinguishers, reduce the data complexity and show at which number of rounds a primitive becomes resistant against bit-based division property. In Fig. 1 we give an overview of the number of rounds required before no bit-based division property distinguisher exists in relation to the full number of rounds of the primitive. It can be seen that most ciphers provide a fairly large security margin against these type of attacks and also for many of these designs there are indeed better distinguishers based on other techniques like differential and linear cryptanalysis.

The performance of Solvatore varies a lot from the designs and for some it is not feasible to find good distinguishers. For instance we also implemented both AES and Keccak in our tool, but we could only obtain very limited results which could not improve upon the state-of-the-art.

5 Conclusion and Future Work

In this work we presented a new framework to automatically find division property distinguishers for a large class of cryptographic primitives by reducing the problem to SAT. We also provide a cryptanalysis tool implementing this approach, providing a simple way to describe primitives, allowing both designers and cryptanalysts to evaluate cryptographic primitives against this attack vector.

Using this tool we present several new or improved bit-based division property distinguishers for ChaCha, ChasKey, DES, GIFT, LBlock, Mantis, Qarma, RoadRunner, Salsa and SM4.

Furthermore, we provide an improved algorithm for finding distinguisher with an optimal data complexity and show for several primitives that no bit-based division property distinguisher can exist for more rounds.