NeuroGIFT: Using a Machine Learning Based Sat Solver for Cryptanalysis

Abstract

A recent trend in machine learning is the implementation of machine learning based solvers, such as the sat solver NeuroSat. The main limitation of NeuroSat is its scaling to large problems. We conjecture that this lack of scaling is due to learning an all-purpose SAT solver, and that learning to solve specialized SAT problems instead should yield better results. In this article, we evaluate our hypothesis by training and testing NeuroSat on SAT problems for differential cryptanalysis on the block cipher GIFT, and present the resulting classifier NeuroGift. We show that on these highly structured problems, our models are able to perform orders of magnitude better than the original NeuroSat, potentially paving the way for the use of specialized solvers for cryptanalysis problems.

Appendices

Appendix

A Clauses for the S-Box of GIFT

The 36 clauses are provided as follows

$$\begin{aligned} \left\{ \begin{array}{l} \overline{x_{0}} \vee \overline{x_{1}} \vee \overline{x_{2}} \vee x_{3} \vee \overline{y_{2}} = 1\\ x_{0} \vee \overline{x_{1}} \vee \overline{x_{2}} \vee \overline{x_{3}} \vee \overline{y_{1}} \vee \overline{y_{2}} = 1\\ x_{0} \vee \overline{x_{1}} \vee x_{2} \vee \overline{y_{0}} \vee y_{1} \vee \overline{y_{2}} = 1\\ x_{1} \vee x_{2} \vee \overline{y_{0}} \vee \overline{y_{1}} \vee \overline{y_{2}} \vee y_{3} = 1\\ x_{1} \vee \overline{x_{2}} \vee \overline{x_{3}} \vee y_{1} \vee \overline{y_{2}} \vee y_{3} = 1\\ x_{0} \vee x_{1} \vee x_{2} \vee \overline{y_{0}} \vee \overline{y_{1}} \vee y_{2} \vee \overline{y_{3}} = 1\\ x_{0} \vee x_{1} \vee \overline{x_{2}} \vee \overline{x_{3}} \vee y_{1} \vee y_{2} \vee \overline{y_{3}} = 1\\ \overline{y_{0}} \vee w = 1\\ \overline{y_{1}} \vee w = 1\\ \overline{y_{2}} \vee w = 1\\ \overline{y_{3}} \vee w = 1\\ x_{0} \vee \overline{x_{1}} \vee \overline{x_{2}} \vee x_{3} \vee y_{2} = 1\\ x_{1} \vee \overline{x_{2}} \vee x_{3} \vee \overline{y_{2}} \vee \overline{y_{3}} = 1\\ \overline{x_{1}} \vee x_{3} \vee \overline{y_{0}} \vee \overline{y_{2}} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee \overline{x_{1}} \vee y_{0} \vee \overline{y_{2}} \vee \overline{y_{3}} = 1\\ x_{0} \vee \overline{x_{3}} \vee y_{0} \vee \overline{y_{2}} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee x_{2} \vee x_{3} \vee y_{2} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee y_{0} \vee \overline{y_{1}} \vee y_{2} \vee \overline{y_{3}} = 1\\ x_{0} \vee \overline{x_{1}} \vee x_{2} \vee x_{3} \vee y_{3} = 1\\ \overline{x_{0}} \vee x_{1} \vee x_{2} \vee x_{3} \vee y_{3} = 1\\ \overline{x_{1}} \vee y_{0} \vee \overline{y_{1}} \vee \overline{y_{2}} \vee y_{3} = 1\\ x_{1} \vee \overline{x_{2}} \vee x_{3} \vee y_{2} \vee y_{3} = 1\\ x_{1} \vee \overline{x_{3}} \vee y_{0} \vee y_{2} \vee y_{3} = 1\\ x_{0} \vee y_{0} \vee \overline{y_{1}} \vee y_{2} \vee y_{3} = 1\\ \overline{x_{1}} \vee y_{0} \vee y_{1} \vee y_{2} \vee y_{3} = 1\\ x_{0} \vee x_{1} \vee x_{2} \vee x_{3} \vee \overline{w} = 1\\ x_{0} \vee y_{0} \vee y_{1} \vee y_{2} \vee \overline{w} = 1\\ x_{1} \vee y_{0} \vee y_{1} \vee y_{3} \vee \overline{w} = 1\\ x_{0} \vee \overline{x_{1}} \vee x_{2} \vee \overline{x_{3}} \vee y_{1} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee x_{1} \vee \overline{x_{3}} \vee \overline{y_{0}} \vee \overline{y_{2}} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee x_{2} \vee \overline{y_{0}} \vee y_{1} \vee y_{2} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee \overline{x_{1}} \vee \overline{x_{3}} \vee \overline{y_{0}} \vee y_{2} \vee y_{3} = 1\\ \overline{x_{0}} \vee x_{1} \vee \overline{x_{2}} \vee \overline{x_{3}} \vee \overline{y_{0}} \vee \overline{y_{1}} \vee \overline{y_{3}} = 1\\ \overline{x_{1}} \vee \overline{x_{2}} \vee \overline{x_{3}} \vee \overline{y_{0}} \vee \overline{y_{1}} \vee y_{2} \vee \overline{y_{3}} = 1\\ \overline{x_{0}} \vee \overline{x_{1}} \vee x_{2} \vee \overline{x_{3}} \vee \overline{y_{0}} \vee \overline{y_{1}} \vee y_{3} = 1\\ \overline{x_{0}} \vee \overline{x_{1}} \vee \overline{x_{2}} \vee \overline{x_{3}} \vee \overline{y_{0}} \vee y_{1} \vee y_{3} = 1 \end{array} \right. . \end{aligned}$$

Fig. 8.

Confidence for 6-round Samples. The horizontal axis corresponds to the number of iterations, and the vertical axis is the value of $y^{(T)}$. The circles show a characteristic feature of the UNSAT samples.

B Impact of the Samples with Low Hamming Weight

In order to evaluate the impact of samples where the difference has low hamming weight, we plot the confidence of the network after each message passing iteration during the test phase of NeuroGift-V1, while keeping track of the structure of the input and output difference. Figure 8 illustrates the confidence of the network for 6-rounds samples. We can observe that the curves for all SAT samples of the same length are similar. But the curves of the UNSAT samples are different. We think that two parameters result in the difference. One reason is the Hamming weight of the input/output differences. Another one is the differential effect. We analyse the 60 pairs of samples in the test set. The Hamming weight of the UNSAT samples are provided in the figures. The samples with the same Hamming weight are illustrated with same color. It can be found that the curves with same color are similar. An interesting example is the UNSAT sample of the 20-th pair of 6-round samples, this is the unique sample that is wrongfully classified by the network. Firstly, the Hamming weight of the input/output differences of this sample is 4, which is even smaller than the value of the optimal trail. Another fact is that the corresponding differential only have one trail with 16 active S-boxes. Since NeuroGift-V1 is designed to identify the topology structure of the figure, the dominant trail property causes the network to make the wrong decision.