基于SAT的差分和线性活跃S盒搜索方法  

Sat-Based Differential and Linear Active S-box Search Method

作　　者：苗旭东 董新锋 韩羽[1,2] 穆道光 张文政 MIAO Xudong;DONG Xinfeng;HAN Yu;MU Daoguang;ZHANG Wenzheng(No.30 Institute of CETC,Chengdu Sichuan 610041,China;Science and Technology on Communication Security Laboratory,Chengdu Sichuan 610041,China)

机构地区：[1]中国电子科技集团公司第三十研究所,四川成都610041 [2]保密通信重点实验室,四川成都610041

出　　处：《信息安全与通信保密》2022年第5期10-17,共8页Information Security and Communications Privacy

基　　金：四川省科技计划资助项目(No.2021ZYD0011)。

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

关 键 词：布尔可满足性问题 自动化分析 活跃S盒 分组密码 

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