基于SAT方法进一步加速差分特征的搜索

doi:10.11959/j.issn.2096-109x.2022066

摘要/Abstract

摘要：

回顾了孙等使用Matsui边界条件加速差分特征搜索的方法，为了进一步提高搜索效率，改进了Matsui 边界条件以及利用 Matsui 边界条件加速差分特征自动化搜索的方法，并提出了一种改进的方法来搜索分组密码的最优差分特征。研究了线程数和询问条件的加速效果并提出了选择线程数以及询问条件的策略。使用STP和CryptoMiniSat分别搜索概率为2^-24、2^-25、2^-26的8轮SPECK96差分特征以及概率为2^-39的 11 轮 HIGHT 差分特征，并比较了在不同线程数和询问条件下求解 SAT/SMT 问题的耗时。研究发现线程数对搜索差分特征的耗时影响较大，而询问条件对搜索差分特征的耗时影响较小，从而提出了一种如何选择线程数和询问条件的策略。根据所提策略，使用改进的边界条件和方法搜索HIGHT的11轮最优差分特征，并首次获得了HIGHT的11轮最优差分特征的紧致概率，即2^-45。现有的 11轮 HIGHT最优差分特征概率的最紧致边界是 $P_{Opt}^{11} \geq 2^{- 45}$ 。这就意味着，利用现有 11轮 HIGHT最优差分特征概率的最紧致边界无法给出11轮HIGHT抗差分分析安全性的精确评估。因此，所提策略的结果是目前已知的最优结果。

关键词: 差分分析, 差分特征, 自动化搜索, SAT求解器

Abstract:

Sun et al.’s method of using Matsui’s bounding conditions to accelerate the search of differential characteristics was reviewed.Matsui’s boundary conditions and Sun et al.’s method of using Matsui’s bounding conditions to accelerate the search of differential characteristics were improved for better search efficiency.Then an improved method to search for the optimal differential characteristics in block ciphers was proposed.Besides, the accelerating effects of the number of threads and the query condition were investigated, and a strategy for choosing the number of threads and the query condition were proposed.STP and CryptoMiniSat were used to search for 8-round SPECK96 differential characteristics with probabilities of 2^{- 24}, 2^{- 25}, 2^{- 26}and 11-round HIGHT differential characteristics with a probability of 2^{- 39}, then the time-consuming of solving SAT/SMT problems under different number of threads and query conditions were compared.It was found that the number of threads has a great effect on the time consumption of searching for differential characteristics, while the query condition may have little effect on the time consumption of searching for differential characteristics.Then, a strategy on how to select the number of threads and the query condition was proposed.Furthermore, it was found that STP can affect the overall efficiency of the search.According to the proposed strategy, the 11-round optimal differential characteristics of HIGHT were searched by using the improved bounding conditions and improved method.A tight bound for the probability of the 11-round optimal differential characteristics of HIGHT was obtained for the first time, i.e.2^{- 45}.To the best of our knowledge, the existing tightest bound of the optimal 11-round HIGHT is $P_{Opt}^{11} \geq 2^{- 45}$ .This means that using the existing tightest bound of the optimal 11-round HIGHT cannot give an accurate evaluation of the security of 11-round HIGHT against differential cryptanalysis.Therefore, the result is the best-known result.

Key words: differential cryptanalysis, differential characteristics, automatic search, SAT solver

中图分类号:

TP309.7

许峥. 基于SAT方法进一步加速差分特征的搜索[J]. 网络与信息安全学报, 2022, 8(5): 129-139.

Zheng XU. Further accelerating the search of differential characteristics based on the SAT method[J]. Chinese Journal of Network and Information Security, 2022, 8(5): 129-139.

图/表 8

表1

符号及含义Table 1 Notations and descriptions"

符号	含义
$x ∥ y$	比特串x与y的集联
$x \land y$	x与y的逐比特逻辑与
$x \oplus y$	x与y的逐比特异或
$x ⊞ y$	X加y加模2ⁿ
$\bar{x}$	x的逐比特取反
$w t (x)$	x的汉明重量
$x [i]$	x的第i比特，其中i=0为最低有效比特
$x ≪ r$	x左移r个比特
$x ≫ r$	x右移r个比特
$x ⋘ r$	x循环左移r个比特
$x ⋙ r$	x循环右移r个比特
$Δ x$	x与x′的异或差分 $Δ x = x \oplus x'$

表1

图1

图2

图3

图4

图5

图6

表2

HIGHT的11轮最优差分特征Table 2 The 11-round optimal differential characteristic of HIGHT"

r	$Δ X_{r}^{7}$	$Δ X_{r}^{6}$	$Δ X_{r}^{5}$	$Δ X_{r}^{4}$	$Δ X_{r}^{3}$	$Δ X_{r}^{2}$	$Δ X_{r}^{1}$	$Δ X_{r}^{0}$	$w_{d}^{r}$
1	0x00	0x00	0x08	0xE5	0x28	0xE9	0x80	0x00	0
2	0x00	0x00	0xE5	0xA8	0xE9	0x80	0x00	0x00	1
3	0x00	0x00	0xA8	0x2C	0x80	0x00	0x00	0x00	8
4	0x00	0x00	0x2C	0x80	0x00	0x00	0x00	0x00	2
5	0x00	0x00	0x80	0x00	0x00	0x00	0x00	0x00	3
6	0x00	0x80	0x00	0x00	0x00	0x00	0x00	0x00	0
7	0x80	0x00	0x00	0x00	0x00	0x00	0x00	0xC3	3
8	0x00	0x00	0x00	0x00	0x00	0x72	0xC3	0x80	4
9	0x00	0x00	0x00	0x0C	0x72	0xE9	0x80	0x00	9
10	0x00	0xA3	0x0C	0xF2	0xE9	0x80	0x00	0x00	3
11	0xA3	0x00	0xF2	0x2A	0x80	0x00	0x00	0x08	7
12	0x00	0x79	0x2A	0x80	0x00	0xC2	0x08	0xA3	5

表2

参考文献 30

[1]	BIHAM E , SHAMIR A . Differential cryptanalysis of DES-like cryptosystems[J]. Journal of Cryptology, 1991,4(1): 3-72.
[2]	MATSUI M , . On correlation between the order of S-boxes and the strength of DES[C]// Workshop on the Theory and Application of Cryptographic Techniques. 1994: 366-375.
[3]	BIRYUKOV A , ROY A , VELICHKOV V . Differential analysis of block ciphers SIMON and SPECK[C]// International Workshop on Fast Software Encryption. 2014: 546-570.
[4]	BIRYUKOV A , VELICHKOV V , LE C Y . Automatic search for the best trails in ARX:application to block cipher speck[C]// International Conference on Fast Software Encryption. 2016: 289-310.
[5]	LIU Z B , LI Y Q , WANG M S . Optimal differential trails in SIMON-like ciphers[J]. IACR Transactions on Symmetric Cryptology, 2017: 358-379.
[6]	LIU Z B , LI Y Q , JIAO L ,et al. A new method for searching optimal differential and linear trails in ARX ciphers[J]. IEEE Transactions on Information Theory, 2020,67(2): 1054-1068.
[7]	MOUHA N , WANG Q J , GU D W ,et al. Differential and linear cryptanalysis using mixed-integer linear programming[C]// Int- ernational Conference on Information Security and Cryptology. 2011: 57-76.
[8]	FU K , WANG M Q , GUO Y H ,et al. MILP-based automatic search algorithms for differential and linear trails for speck[C]// International Conference on Fast Software Encryption. 2016: 268-288.
[9]	XIANG Z J , ZHANG W T , BAO Z Z ,et al. Applying MILP method to searching integral distinguishers based on division property for 6 lightweight block ciphers[C]// International Conference on the Theory and Application of Cryptology and Information Security. 2016: 648-678.
[10]	CUI T T , JIA K T , FU K ,et al. New automatic search tool for impossible differentials and zero-correlation linear approximations[J]. Cryptology ePrint Archive, 2016.
[11]	SASAKI Y , TODO Y . New impossible differential search tool from design and cryptanalysis aspects[C]// Annual International Conference on the Theory and Applications of Cryptographic Techniques. 2017: 185-215.
[12]	MOUHA N , PRENEEL B . Towards finding optimal differential characteristics for ARX:application to Salsa20[J]. IACR Cryptology ePrint Archive, 2013(2013): 328.
[13]	K?LBL S , LEANDER G , TIESSEN T . Observations on the SIMON block cipher family[C]// Annual Cryptology Conference. 2015: 161-185.
[14]	ANKELE R , K?LBL S ,, . Mind the gap-a closer look at the security of block ciphers against differential cryptanalysis[C]// International Conference on Selected Areas in Cryptography. 2018: 163-190.
[15]	ROH D Y , KOO B W , JUNG Y H ,et al. Revised version of block cipher CHAM[C]// International Conference on Information Security and Cryptology. 2019: 1-19.
[16]	韩亚 . 基于SAT/SMT自动搜索三类分组密码区分器研究[D]. 北京:中国科学院大学, 2018.
	HAN Y . Automatically search for three types of block cipher distinguishers based on SAT/SMT solver[D]. Beijing:University of Chinese Academy of Sciences, 2018.
[17]	LIU Y W , WAND Q J , RIJMEN V . Automatic search of linear trails in ARX with applications to SPECK and Chaskey[C]// International Conference on Applied Cryptography and Network Security. 2016: 485-499.
[18]	SUN L , WANG W , WANF M Q . Automatic search of bit-based division property for ARX ciphers and word-based division property[C]// International Conference on the Theory and Application of Cryptology and Information Security. 2017: 128-157.
[19]	SASAKI Y , TODO Y . New algorithm for modeling S-box in MILP based differential and division trail search[C]// International Conference for Information Technology and Communications. 2017: 150-165.
[20]	ZHANG Y J , SUN S W , CAI J H ,et al. Speeding up MILP aided differential characteristic search with Matsui’s strategy[C]// International Conference on Information Security. 2018: 101-115.
[21]	ZHOU C N , ZHANG W T , DING T Y ,et al. Improving the MILP-based security evaluation algorithm against differential/linear cryptanalysis using a divide-and-conquer approach[J]. IACR Transactions on Symmetric Cryptology, 2019: 438-469.
[22]	BOURA C , COGGIA D . Efficient MILP modelings for Sboxes and linear layers of SPN ciphers[C]// IACR Transactions on Symmetric Cryptology. 2020: 327-361.
[23]	SONG L , HUANG Z J , YANG Q Q . Automatic differential analysis of ARX block ciphers with application to SPECK and LEA[C]// Australasian Conference on Information Security and Privacy. 2016: 379-394.
[24]	SUN L , WANG W , WANG M Q . Accelerating the search of differential and linear characteristics with the SAT method[C]// IACR Transactions on Symmetric Cryptology. 2021: 269-315.
[25]	GANESH V , DILL D L . A decision procedure for bit-vectors and arrays[C]// International Conference on Computer Aided Verification. 2007: 519-531.
[26]	SOOS M , NOHL K , CASTELLUCCIA C . Extending SAT solvers to cryptographic problems[C]// International Conference on Theory and Applications of Satisfiability Testing. 2009: 244-257.
[27]	LIPMAA H , MORIAI S . Efficient algorithms for computing differential properties of addition[C]// International Workshop on Fast Software Encryption. 2001: 336-350.
[28]	BEAULIEU R , SHORS D , SMITH J ,et al. The SIMON and SPECK lightweight block ciphers[C]// Proceedings of the 52nd Annual Design Automation Conference. 2015: 1-6.
[29]	HONG D J , SUNG J C , HONG S H ,et al. HIGHT:a new block cipher suitable for low-resource device[C]// International Workshop on Cryptographic Hardware and Embedded Systems. 2006: 46-59.
[30]	EéN N , S?RENSSON N . An extensible SAT-solver[C]// International Conference on Theory and Applications of Satisfiability Testing. 2003: 502-518.