| In Crypto 1990,Biham and Shamir proposed differential attack,and then in Eurocrypt 1993,Matsui proposed linear attack.These two attack methods are very effective and widely used symmetric cryptanalysis methods.The core of differential attack and linear attack is to search for differential feature and linear feature with high probability.This thesis studied the differential and linear automated analysis of block cipher based on SAT problems.The main conclusions of research are as follows:1.SAT-based automatic search algorithm combined with divide-and-conquer strategy.Combining minimum Matsui’s boundings and SAT model with divede-and-conquer strategy for the first time,an accelerated search algorithm for optimal difference characteristics based on SAT model is proposed.Using the information provided by Matsui’s boundings conditions of any part of continuous round,the search space is divided into disjoint subsets.A descending branching search chain model is proposed by analyzing satisfiability relationship between differential SAT models.Furthermore,in the aspect of model optimization,a method to reduce the number of search subsets is proposed.In the aspect of algorithm implementation,the parallel technique is combined to achieve the reduction of model search space.2.Differential and linear automatic analysis of SPECK-48/96/128The SAT automatic search algorithm combined with the idea of divide-and-conquer is applied to the ARX cryptography algorithm SPECK.After selecting the specific partition conditions,the accelerated search algorithm is applied to search for the global optimal difference and linear characteristics of SPECK-48/96/128,which improved the search efficiency and obtained the optimal difference and linear characteristics of higher rounds.3.Differential and linear automatic analysis of FUTURE algorithmThe differential and linear security of FUTURE algorithm is analyzed by using the SATbased automatic search method.Firstly,the difference of all rounds and the minimum number of linear active S-boxes are obtained,which is 5 rounds higher than the result in the algorithm design report.Furthermore,considering the inhomogeneity of S-box difference distribution table and linear approximation table,the 7-round optimal difference and 8-round optimal linear characteristics are obtained by establishing automatic analysis model,and the security of FUTURE algorithm is evaluated more accurately. |