SAT-Based Automatic Searching for Differential and Linear Trails:Applying to CRAX  

作　　者：Yiyi HAN Caibing WANG Zhongfeng NIU Lei HU 

机构地区：[1]State Key Laboratory of Information Security,Institute of Information Engineering,Chinese Academy of Sciences,Beijing 100195,China [2]School of Cyber Security,University of Chinese Academy of Sciences,Beijing 100049,China

出　　处：《Chinese Journal of Electronics》2024年第1期72-79,共8页电子学报（英文版）

基　　金：supported by the National Key R&D Program of China(Grant No.2018YFA0704704);the Natural Science Foundation of China(Grant No.61772519);the Chinese Major Program of National Cryptography Development Foundation(Grant No.MMJJ20180102)。

摘　　要：Boolean satisfiability problem(SAT)is now widely applied in differential cryptanalysis and linear cryptanalysis for various cipher algorithms.It generated many excellent results for some ciphers,for example,Salsa20.In this research,we study the differential and linear propagations through the operations of addition,rotation and XOR(ARX),and construct the SAT models.We apply the models to CRAX to search differential trails and linear trails automatically.In this sense,our contnbution can be broadly divided into two parts.We give the bounds for differential and linear cryptanalysis of Alzette both up to 12 steps,by which we present a 3-round differential attack and a 3-round linear attack for CRAX.We construct a 4-round key-recovery attack for CRAX with time complexity289times of 4-round encryption and data complexity 225.

关 键 词：Differential cryptanalysis Linear cryptanalysis Boolean satisfiability problem CRAX 

分 类 号：TN918.1[电子电信—通信与信息系统]