SAT-based Impossible Differential Cryptanalysis

As a variant of differential cryptanalysis,impossible differential analysis utilizes differences with zero probability,as opposed to classical differential cryptanalysis which utilizes high probability differences to recover keys,and its basic idea is to filter out those candidate keys that lead to differences with zero probability.To improve the efficiency of impossible difference analysis,various automated methods have been proposed.The SAT-based automated search method converts the problem to be solved into the form of the conjunctive normal and then solves it.The advantage is that it can directly depict logical operations(e.g,AND,OR,NOT,and XOR),thereby building a more efficient search model.This paper performs the impossible differential analysis of block ciphers with the help of SAT-like automated tools,and the details of the work are as follows.(1)For the structural characteristics of the GRANULE algorithm,the depicted method of the S-box operation is optimized,and an bit-oriented efficient SAT model is constructed.A 10-round distinguisher is obtained by solving the model,and it is verified by an improved SAT-based impossible differential distinguisher verification method.Finally,a13-round key recovery attack is given.compared with the existing results,this paper searches for the highest number of distinguisher rounds and key recovery attack rounds,and the time complexity and data complexity of the attacks are reduced.(2)By observing the structural properties of the Pyjamask algorithm,an efficient depicted model for the Mix Rows operation of the linear component of the algorithm is proposed,and the conventional automatic search strategy is locally optimized.The 4-round impossible differential distinguishers of Pyjamask-96 and Pyjamask-128 are obtained by solving the model.Compared with the existing results,in this paper,Pyjamask-128 has the highest number of distinguisher rounds,and Pyjamask-96 has the same number of distinguisher rounds as the best existing results.(3)Based on the structural properties of the Gimli algorithm,the depicted models of the AND and OR operations and logical left shift operations in the SP box of the nonlinear component of the algorithm are given,and based on these depicted models,the direct depict of the SP box is realized.On this basis,the SAT model of bit-oriented impossible differential distinguisher is established for the Gimli algorithm and the model is solved to obtain a 12-round impossible difference distinguisher of the Gimli algorithm,and finally,the obtained distinguisher is verified.Compared with the existing results,this paper has the highest number of distinguisher rounds.