摘要：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算法在特殊输入输出差分和掩码集合下,不可能差分和零相关区分器轮数的上界.