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

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

Abstract

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

CLC Number:

TP309.7

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.

Figures/Tables 8

符号	含义
$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'$

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

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

Further accelerating the search of differential characteristics based on the SAT method

RichHTML

PDF下载

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 8

References 30

Related Articles 2

Metrics

Recommended 0

[1]	Ya HAN. Automatic method for searching impossible differentials and zero-correlation linear hulls of ARX block ciphers [J]. Chinese Journal of Network and Information Security, 2017, 3(7): 58-63.
[2]	Zheng-bin LIU. Automatic search algorithm for differential characteristics in ARX ciphers [J]. Chinese Journal of Network and Information Security, 2016, 2(5): 56-63.