【摘要】 混合整数线性规划和布尔可满足性问题（Boolean Satisfiability Problem,SAT）两种约束规划技术已被广泛应用到密码自动化安全性分析中，但目前并没有基于SAT的差分和线性活跃S盒分析方法。为了使SAT成为密码算法安全性分析和评估的一种更为通用的方法，首次建立了字节级分支、异或、MDS的SAT模型，提出了一种通用的基于SAT的差分和线性活跃S盒搜索方法，能够搜索经典分组密码算法的活跃S盒个数。为了检验本方法的实际应用效果，利用本方法成功搜索出AES、Dblock系列分组密码算法的差分活跃S盒。更多还原

【Abstract】 Two constraint programming techniques, namely mixed integer linear programming and SAT(Boolean Satisfiability Problem), have been widely used in cryptographic automation security analysis.However, there is currently no SAT-based differential and linear active S-box analysis method. In order to make SAT a more general method for security analysis and evaluation of cryptographic algorithms,the SAT model of byte-level branch, XOR, MDS is established for the first time. A general SAT-based differential and linear active S-box search method is proposed, which can search the number of active S-boxes of classical block cipher algorithms. The practical application effect indicates that the differential active S-box of AES and Dblock series block cipher can be successfully searched by using this method.更多还原