基于SAT的ARX不可能差分和零相关区分器的自动化搜索

ARX（Addition，Rotation，Xor）算法基于模整数加，异或加和循环移位三种运算，便于软硬件的快速实现.不可能差分分析和零相关分析是攻击ARX的有效方法，攻击的关键是搜索更长轮数、更多数量的不可能差分和零相关区分器.目前很多的搜索方法都没有充分考虑非线性组件的性质，往往不能搜索得到更好、更准确的区分器.本文提出了基于SAT（Satisfiability）的ARX不可能差分和零相关区分器的自动化搜索算法.通过分析ARX算法组件的性质，特别是常规模加和密钥模加这两种非线性运算差分和线性传播的特性，给出了高效简单的SAT约束式.在此基础上，建立SAT模型进行区分器的搜索.作为应用，本文首次给出了Chaskey算法13条4轮不可能差分和1条4轮零相关区分器；首次给出了SPECK32算法10条6轮零相关区分器和SPECK48算法15条6轮零相关区分器；在较短的时间内，给出了HIGHT算法17轮的不可能差分和零相关区分器.与现有结果相比，无论是区分器的条数，还是搜索区分器的时间均有明显的提升.此外，通过重新封装求解器STP的输出接口，建立了自动化的SAT\\SMT分析模型，能够给出ARX算法在特殊输入输出差分和掩码集合下，不可能差分和零相关区分器轮数的上界.

SAT-Based Automatic Search for Impossible Differentials and Zero-Correlation Linear Approximations in ARX

ARX(Addition,Rotation,Xor) algorithms are based on three operations:modular addition,exclusive-OR and bitwise rotation,which execute very fast in both software and hardware.Impossible differential cryptanalysis and zero-correlation linear cryptanalysis are among the most powerful attacks for ARX ciphers.The key problem for the attacks is searching more and longer impossible differentials and zero-correlation linear approximations.Although there are many automatic search algorithms,these approaches do not fully utilize the non-linear component properties,which cannot reach their potential.A SAT(Satisfiability)-based model to automatic search for impossible differentials and zero-correlation linear approximations in ARX is proposed.By exploiting behaviors of every component,especially the differential and linear propagation properties through general modular addition and key modular addition operations,we generate computable and easily implementable constraints and establish the SAT-based model.As applications,we apply our model to Chaskey,SPECK and HIGHT.For Chaskey,we are able to find 13 4-round impossible differentials and 1 4-round zero-correlation linear approximation for the first time.For SPECK,we first find 10 6-round zero-correlation linear approximations of SPECK32 and 15 6-round zero-correlation linear approximations of SPECK48.Besides,we find 4 17-round impossible differentials and zero-correlation linear approximations of HIGHT in a few minutes.Compared with the existing results,both the number and the search time of distinguishers are significantly improved.In addition,by repackaging the output interface of the STP solver,we establish the automated SAT\\SMT model,which can give the upper bound of rounds of impossible differentials and zero-correlation linear approximations under special input and output differential and mask sets for ARX algorithm.