Research On Method Of Symmetric Cryptanalysis Based On Boolean Satisfiability Problem

With the rapid development of science and technology,people are benefiting from the convenience brought by information technology,but at the same time,they are also facing the risks caused by information security issues.As an important factor in ensuring information security,cryptography has been highly valued by countries around the world.Cryptology can be divided into cryptography and cryptanalysis.Cryptography studies how to efficiently encode information for the purpose of concealing information,while cryptanalysis studies how to decrypt ciphertext and modify messages.Designing efficient and secure ciphers can prevent adversaries from obtaining important information.At the same time,studying cryptanalysis can provide security assessments,improve cipher design techniques,and make better cryptographic primitives come out.All cryptanalysis techniques aim to distinguish between a cryptographic algorithm and a completely random function with low time complexity and data complexity,in order to perform key recovery.For the modern block cipher,the block length and the number of rounds is large enough,and the algebraic degree is high enough,which makes difficult for traditional cryptanalysis techniques to attack more rounds.Therefore,many scholars have innovatively proposed new analysis methods such as differential-linear analysis,high-order differential analysis,rotational analysis and so on.At the same time,during the analysis process,the attacker often looks for the optimal attack route,such as the differential(linear)trace with the highest probability(correlation)in the differential(linear)analysis.Therefore,finding the optimal route is also a major difficulty in the attack..Scholars at home and abroad have proposed that the search for a specific route can be modeled as some mathematical constraints,and then solve such constraints through automatic search tools.With the gradual improvement of computing power in modern computer,searching optimal route automaticly has gradually become mainstream.In the field of cryptanalysis,there are two mathematical tools for searching optimal routes: mixed integer linear programming(MILP)and Boolean satisfiability problem(SAT).This article describes the analysis of message authentication code(Chaskey)and hash function(Xoodyak)using SAT search tools.The main contributions of this paper are as follows:1.Since the message authentication code(MAC)Chaskey does not contain the characteristic of XOR constants,it meets the prerequisites for using rotation analysis,so combined with the difference-linear analysis method,the algorithm is first analyzed using the rotation difference-linear method.At the same time,in the linear part,the SAT solver is used to solve the optimal linear route to reduce the time complexity and data complexity.Ultimately,this paper provides a 9-round Chaskey-rotated differential-linear discriminator with probability 2-113.272.2.In order to obtain the key of the block cipher algorithm,it is necessary to consider multiple linear traces in the linear part to improve the correlation,and use the split point technique to reduce the complexity of key recovery.Finally,we present a key recovery structure for Chaskey using rotational differential-linear analysis and partitioning techniques over 8 rounds with time complexity in 2124.944.3.This article also presents the results of two rounds of preimage attack of hash function Xoodyak using the SAT solver.In order to speed up the solving process of the SAT solver,we try to terminate the search process early by reducing intermediate variables and inverting known bits,thereby reducing the search time and reducing the time complexity.Finally,this article provides the results of 2 rounds Xoodyak preimage attack with a total time complexity of 287,before that there was only 1round of Xoodyak preimage attack results.