可分特征的刻画及其自动化分析应用*

胡建勇，穆道光，周 宇，董新锋

（1.中国电子科技集团公司第三十研究所，四川 成都 610041；2.保密通信重点实验室，四川 成都 610041）

0 引 言

随着密码学与计算机、数学等交叉领域的不断发展，密码算法的自动化分析程度越来越高。自动化分析手段逐步替代原来手工推导验证的方式，具有分析能力强、准确性高、容易验证等优点，备受密码研究人员的青睐，被广泛用于密码算法的安全性分析和评估中，从而“反哺”算法设计，对提升密码算法的安全强度具有重要的作用。

密码自动化分析是指将密码分析问题转化为数学求解问题，根据专业数学求解软件的求解情况获得密码分析的结果。常见的数学求解问题有混合整数线性规划问题（Mixed Integer Linear Programming，MILP）和布尔可满足性问题（Boolean Satisfiability Problem，SAT），常用的数学求解软件有Cplex、Gurobi、MIT、SMT 等。根据求解问题的不同，密码自动化分析主要分为基于MILP 的自动化分析和基于SAT 的自动化分析两种类型。它们的区别在于问题的刻画不同，基于MILP 的自动化分析使用线性不等式刻画，而基于SAT 的自动化分析使用布尔逻辑方程刻画。

目前，实现自动化的分析方法主要有差分分析[1-2]、线性分析[2]、不可能差分分析[3-4]、零相关线性分析[5-6]和积分分析[7-12]。其中，自动化积分分析根据可分性质在密码算法中的传播规律和可分特征的刻画，实现了区分器的搜索。根据可分性质定义的不同，自动化积分分析又分为基于两子集可分性质的自动化积分分析[7-9]和基于三子集可分性质的自动化积分分析[10-12]。……