全輪超輕量級分組密碼PFP的相關(guān)密鑰差分分析

嚴(yán)智廣; 韋永壯; 葉濤

doi:10.11999/JEIT240782

全輪超輕量級分組密碼PFP的相關(guān)密鑰差分分析

doi: 10.11999/JEIT240782

1.
桂林電子科技大學(xué)廣西密碼學(xué)與信息安全重點實驗室桂林 541000
2.
密碼科學(xué)技術(shù)國家重點實驗室北京 100878

基金項目: 國家自然科學(xué)基金 (62162016, 62402132)

詳細信息

作者簡介:
嚴(yán)智廣：男，碩士，研究方向為密碼學(xué)、信息安全

韋永壯：男，博士，教授，博導(dǎo)，廣西密碼學(xué)與信息安全重點實驗室主任，研究方向為密碼學(xué)與信息安全

葉濤：男，博士，講師，研究方向為對稱密碼算法設(shè)計與分析

通訊作者:
葉濤　yetao@guet.edu.cn

中圖分類號: TN918; TP309
計量
- 文章訪問數(shù): 281
- HTML全文瀏覽量: 58
- PDF下載量: 127
- 被引次數(shù): 0
出版歷程
- 收稿日期: 2024-09-11
- 修回日期: 2024-12-30
- 網(wǎng)絡(luò)出版日期: 2025-01-11

Related-key Differential Cryptanalysis of Full-round PFP Ultra-lightweight Block Cipher

1.
Guangxi Key Laboratory of Cryptography and information Security, Guilin University of Electronic Technology, Guilin 541004, China
2.
State Key Laboratory of Cryptology, Beijing 100878, China

Funds: The National Natural Science Foundation of China (62162016, 62402132)

摘要

摘要: 2017年，PFP作為一種超輕量級分組密碼被提出，而因其卓越的實現(xiàn)性能備受業(yè)界廣泛關(guān)注。該算法不僅硬件開銷需求低(僅需約1355 GE(等效門))、功耗小，而且加解密速度快(其速度甚至比國際著名算法 PRESENT的實現(xiàn)速度快1.5倍)，非常適合在物聯(lián)網(wǎng)環(huán)境中使用。在PFP算法的設(shè)計文檔中，作者聲稱該算法具有足夠的能力抵御差分攻擊、線性攻擊及不可能差分攻擊等多種密碼攻擊方法。然而該算法是否存在未知的安全漏洞是目前研究的難點。該文基于可滿足性模理論(SMT)，結(jié)合PFP算法輪函數(shù)特點，構(gòu)建兩種區(qū)分器自動化搜索模型。實驗測試結(jié)果表明：該算法在32輪加密中存在概率為2^–62的相關(guān)密鑰差分特征。由此，該文提出一種針對全輪PFP算法的相關(guān)密鑰恢復(fù)攻擊，即只需2⁶³個選擇明文和2⁴⁸次全輪加密便可破譯出80 bit的主密鑰。這說明該算法無法抵抗相關(guān)密鑰差分攻擊。
- 輕量級分組密碼算法 /
- 差分密碼分析 /
- 密鑰恢復(fù)攻擊 /
- 可滿足性模理論
Abstract: Objective In 2017, the PFP algorithm was introduced as an ultra-lightweight block cipher to address the demand for efficient cryptographic solutions in constrained environments, such as the Internet of Things (IoT). With a hardware footprint of approximately 1355 GE and low power consumption, PFP has attracted attention for its ability to deliver high-speed encryption with minimal resource usage. Its encryption and decryption speeds outperform those of the internationally recognized PRESENT cipher by a factor of 1.5, making it highly suitable for real-time applications in embedded systems. While the original design documentation asserts that PFP resists various traditional cryptographic attacks, including differential, linear, and impossible differential attacks, the possibility of undiscovered vulnerabilities remains unexplored. This study evaluates the algorithm’s resistance to related-key differential attacks, a critical cryptanalysis method for lightweight ciphers, to determine the actual security level of the PFP algorithm using formal cryptanalysis techniques. Methods To evaluate the security of the PFP algorithm, Satisfiability Modulo Theories (SMT) is used to model the cipher’s round function and automate the search for distinguishers indicating potential design weaknesses. SMT, a formal method increasingly applied in cryptanalysis, facilitates automated attack generation and the detection of cryptographic flaws. The methodology involved constructing mathematical models of the cipher’s rounds, which are tested for differential characteristics under various key assumptions. Two distinguisher models are developed: one based on single-key differentials and the other on related-key differentials, the latter being the focus of this analysis. These models automated the search for weak key differentials that could enable efficient key recovery attacks. The analysis leveraged the nonlinear substitution-permutation structure of the PFP round function to systematically identify vulnerabilities. The results are examined to estimate the probability of key recovery under different attack scenarios and assess the effectiveness of related-key differential cryptanalysis against the full-round PFP cipher. Results and Discussions The SMT-based analysis revealed a critical vulnerability in the PFP algorithm. A related-key differential characteristic with a probability of 2^–62 is identified, persisting through 32 encryption rounds. This characteristic indicates a predictable pattern in the cipher’s behavior under related-key conditions, which can be exploited to recover the secret key. Such differentials are particularly concerning as they expose a significant weakness in the cipher’s resistance to related-key attacks, a critical threat in IoT applications where keys may be reused or related across multiple devices or sessions.Based on this finding, a key recovery attack is developed, requiring only 2⁶³ chosen plaintexts and 2⁴⁸ full-round encryptions to retrieve the 80-bit master key. The efficiency of this attack demonstrates the vulnerability of the PFP cipher to practical cryptanalysis, even with limited computational resources. The attack’s relatively low complexity suggests that PFP may be unsuitable for applications demanding high security, particularly in environments where adversaries can exploit related-key differential characteristics. Moreover, these results indicate that the existing resistance claims for the PFP cipher are insufficient, as they do not account for the effectiveness of related-key differential cryptanalysis. This challenges the assertion that the PFP algorithm is secure against all known cryptographic attacks, emphasizing the need for thorough cryptanalysis before lightweight ciphers are deployed in real-world scenarios.(Fig. 2: Related-key differential characteristic with probability 2^–62 in 32 rounds; Table 1: Attack complexity and resource requirements for related-key recovery.) Conclusions In conclusion, this paper presents a cryptographic analysis of the PFP lightweight block cipher, revealing its vulnerability to related-key differential attacks. The proposed key recovery attack demonstrates that, despite its efficiency in hardware and speed, PFP fails to resist attacks exploiting related-key differential characteristics. This weakness is particularly concerning for IoT applications, where key reuse or related keys across devices is common. These findings highlight the need for further refinement in lightweight cipher design to ensure robust resistance against advanced cryptanalysis techniques. As lightweight ciphers continue to be deployed in security-critical systems, it is essential that designers consider all potential attack vectors, including related-key differentials, to strengthen security guarantees. Future work should focus on enhancing the cipher’s security by exploring alternative key-schedule designs or increasing the number of rounds to mitigate the identified vulnerabilities. Additionally, this study emphasizes the effectiveness of SMT-based formal methods in cryptographic analysis, providing a systematic approach for identifying previously overlooked weaknesses in cipher designs.
- Lightweight block cipher algorithm /
- Differential cryptanalysis /
- Key recovery attack /
- Satisfiability Modulo Theories (SMT)

HTML全文

圖 1 PFP算法加密流程

下載: 全尺寸圖片幻燈片

圖 2 32輪相關(guān)密鑰差分區(qū)分器向后擴展2輪

下載: 全尺寸圖片幻燈片

表 1 PFP算法攻擊結(jié)果對比

攻擊方法	攻擊輪數(shù)	恢復(fù)主密鑰比特數(shù)(bit)	數(shù)據(jù) 復(fù)雜度	時間復(fù)雜度	文獻
不可能差分	6	32	2^37.00	2^65.00	[7]
不可能差分	9	36	2^36.00	2^58.00	[19]
不可能差分	10	52	2^46.00	2^75.00	[20]
積分攻擊	12	40	2^62.39	2^63.12	[21]
差分攻擊	26	48	2^60.00	2^54.30	[22]
差分攻擊	29	73	2^59.00	2^78.14	本文
相關(guān)密鑰差分攻擊	34	80	2^63.00	2^48.00	本文

下載: 導(dǎo)出CSV

表 2 PFP算法的S盒

x	0	1	2	3	4	5	6	7	8	9	A	B	C	D	E	F
S[x]	C	5	6	B	9	0	A	D	3	E	F	8	4	7	1	2

下載: 導(dǎo)出CSV

表 3 S盒的差分分布表

輸入差分	輸出差分
輸入差分	0	1	2	3	4	5	6	7	8	9	A	B	C	D	E	F
0	16	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
1	0	0	0	4	0	0	0	4	0	4	0	0	0	4	0	0
2	0	0	0	2	0	4	2	0	0	0	2	0	2	2	2	0
3	0	2	0	2	2	0	4	2	0	0	2	2	0	0	0	0
4	0	0	0	0	0	4	2	2	0	2	2	0	2	0	2	0
5	0	2	0	0	2	0	0	0	0	2	2	2	4	2	0	0
6	0	0	2	0	0	0	2	0	2	0	0	4	2	0	0	4
7	0	4	2	0	0	0	2	0	2	0	0	0	2	0	0	4
8	0	0	0	2	0	0	0	2	0	2	0	4	0	2	0	4
9	0	0	2	0	4	0	2	0	2	0	0	0	2	0	4	0
A	0	0	2	2	0	4	0	0	2	0	2	0	0	2	2	0
B	0	2	0	0	2	0	0	0	4	2	2	2	0	2	0	0
C	0	0	2	0	0	4	0	2	2	2	2	0	0	0	2	0
D	0	2	4	2	2	0	0	2	0	0	2	2	0	0	0	0
E	0	0	2	2	0	0	2	2	2	2	0	0	2	2	0	0
F	0	4	0	0	4	0	0	0	0	0	0	0	0	0	4	4

下載: 導(dǎo)出CSV

表 4 PFP算法的差分界

輪數(shù)	最大期望差分特征概率		輪數(shù)	最大期望差分特征概率
輪數(shù)	單密鑰	相關(guān)密鑰	輪數(shù)	單密鑰	相關(guān)密鑰
1	2⁰	2⁰	18	2^–44	2^–34
2	2^–2	2⁰	19	2^–46	2^–36
3	2^–4	2⁰	20	2^–48	2^–38
4	2^–6	2⁰	21	2^–51	2^–40
5	2^–8	2⁰	22	2^–54	2^–42
6	2^–12	2^–3	23	2^–56	2^–44
7	2^–16	2^–5	24	2^–58	2^–46
8	2^–18	2^–9	25	2^–61	2^–48
9	2^–21	2^–14	26	2^–64	2^–50
10	2^–24	2^–18	27	2^–66	2^–52
11	2^–26	2^–20	28	2^–68	2^–54
12	2^–28	2^–22	29	2^–71	2^–56
13	2^–31	2^–24	30	2^–74	2^–58
14	2^–34	2^–26	31	2^–76	2^–60
15	2^–36	2^–28	32	2^–78	2^–62
16	2^–38	2^–30	33	2^–81	2^–64
17	2^–41	2^–32	34	2^–84	2^–66

下載: 導(dǎo)出CSV

表 5 差分特征概率為2^–61的25輪差分區(qū)分器

輪數(shù)	左分支差分	右分支差分	輪數(shù)	左分支差分	右分支差分
0	0x00040D00	0x00000900	13	0x00000900	0x00000900
1	0x00000900	0x00000900	14	0x00000900	0x00000D00
2	0x00000900	0x00000D00	15	0x00000D00	0x00000D00
3	0x00000D00	0x00000D00	16	0x00000D00	0x00000900
4	0x00000D00	0x00000900	17	0x00000900	0x00000900
5	0x00000900	0x00000900	18	0x00000900	0x00000D00
6	0x00000900	0x00000D00	19	0x00000D00	0x00000D00
7	0x00000D00	0x00000D00	20	0x00000D00	0x00000900
8	0x00000D00	0x00000900	21	0x00000900	0x00000900
9	0x00000900	0x00000900	22	0x00000900	0x00000D00
10	0x00000900	0x00000D00	23	0x00000D00	0x00000D00
11	0x00000D00	0x00000D00	24	0x00000D00	0x00000900
12	0x00000D00	0x00000900	25	0x00000900	0x00040D00

下載: 導(dǎo)出CSV

表 6 差分特征概率為2^–62的32輪相關(guān)密鑰差分區(qū)分器

輪數(shù)	左右分支差分	相關(guān)密鑰差分	輪數(shù)	左右分支差分	相關(guān)密鑰差分
0	0x8BBBBA22D1111177	0xD111117777444445DDDD	17	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
1	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	18	0x8BBBBA22D1111177	0xD111117777444445DDDD
2	0x8BBBBA22D1111177	0xD111117777444445DDDD	19	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
3	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	20	0x8BBBBA22D1111177	0xD111117777444445DDDD
4	0x8BBBBA22D1111177	0xD111117777444445DDDD	21	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
5	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	22	0x8BBBBA22D1111177	0xD111117777444445DDDD
6	0x8BBBBA22D1111177	0xD111117777444445DDDD	23	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
7	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	24	0x8BBBBA22D1111177	0xD111117777444445DDDD
8	0x8BBBBA22D1111177	0xD111117777444445DDDD	25	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
9	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	26	0x8BBBBA22D1111177	0xD111117777444445DDDD
10	0x8BBBBA22D1111177	0xD111117777444445DDDD	27	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
11	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	28	0x8BBBBA22D1111177	0xD111117777444445DDDD
12	0x8BBBBA22D1111177	0xD111117777444445DDDD	29	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
13	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	30	0x8BBBBA22D1111177	0xD111117777444445DDDD
14	0x8BBBBA22D1111177	0xD111117777444445DDDD	31	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888
15	0xD11111778BBBBA22	0x8BBBBA22222EEEE88888	32	0x8BBBBA22D1111177	-
16	0x8BBBBA22D1111177	0xD111117777444445DDDD

下載: 導(dǎo)出CSV

表 7 相關(guān)密鑰下PFP算法密鑰恢復(fù)階段的復(fù)雜度計算

步數(shù)	猜測密鑰	篩選后剩余明密文對數(shù)量	時間復(fù)雜度
1	${K_{33}}[31,30,29,28]$	${2^{m - 33 - 4}}$	$ 2 \cdot {2^{m - 33}} \cdot {2^4} $
2	${K_{33}}[23,22,21,20]$	${2^{m - 37 - 4}}$	$ 2 \cdot {2^{m - 37}} \cdot {2^8} $
3	${K_{33}}[15,14,13,12]$	${2^{m - 41 - 4}}$	$ 2 \cdot {2^{m - 41}} \cdot {2^{12}} $
4	${K_{33}}[7,6,5,4]$	${2^{m - 45 - 4}}$	$ 2 \cdot {2^{m - 45}} \cdot {2^{16}} $
5	${K_{33}}[27,26,25,24]$	${2^{m - 49 - 3}}$	$ 2 \cdot {2^{m - 49}} \cdot {2^{20}} $
6	${K_{33}}[19,18,17,16]$	${2^{m - 52 - 3}}$	$ 2 \cdot {2^{m - 52}} \cdot {2^{24}} $
7	${K_{33}}[11,10,9,8]$	${2^{m - 55 - 3}}$	$ 2 \cdot {2^{m - 55}} \cdot {2^{28}} $
8	${K_{33}}[3,2,1,0]$	${2^{m - 58 - 3}}$	$ 2 \cdot {2^{m - 58}} \cdot {2^{32}} $
9	${K_{32}}[31,30,29,28]$	${2^{m - 61 - 4}}$	$ 2 \cdot {2^{m - 61}} \cdot {2^{32}} $
總和			${2^{m - 24}} + {2^{m - 26}}$

下載: 導(dǎo)出CSV

參考文獻(30)

[1]	National Institute of Standards and Technology, DWORKIN M J, BARKER E, et al. Advanced encryption standard[R]. 197, 2001. doi: 10.6028/NIST.FIPS.197.
[2]	WU Wenling and ZHANG Lei. LBlock: A lightweight block cipher[C]. The 9th International Conference on Applied Cryptography and Network Security, Nerja, Spain, 2011: 327–344. doi: 10.1007/978-3-642-21554-4_19.
[3]	GUO Jian, PEYRIN T, POSCHMANN A, et al. The LED block cipher[C]. The 13th International Workshop on Cryptographic Hardware and Embedded Systems, Nara, Japan, 2011: 326–341. doi: 10.1007/978-3-642-23951-9_22.
[4]	BANIK S, PANDEY S K, PEYRIN T, et al. GIFT: A small present: Towards reaching the limit of lightweight encryption[C]. The 19th International Conference on Cryptographic Hardware and Embedded Systems, Taipei, China, 2017: 321–345. doi: 10.1007/978-3-319-66787-4_16.
[5]	BEAULIEU R, TREATMAN-CLARK S, SHORS D, et al. The SIMON and SPECK lightweight block ciphers[C]. Proceedings of the 52nd ACM/EDAC/IEEE Design Automation Conference, San Francisco, USA, 2015: 1–6. doi: 10.1145/2744769.2747946.
[6]	BOGDANOV A, KNUDSEN L R, LEANDER G, et al. PRESENT: An ultra-lightweight block cipher[C]. The 9th International Workshop, Vienna, Austria, 2007: 450–466. doi: 10.1007/978-3-540-74735-2_31.
[7]	黃玉劃, 代學(xué)俊, 時陽陽, 等. 基于Feistel結(jié)構(gòu)的超輕量級分組密碼算法(PFP)[J]. 計算機科學(xué), 2017, 44(3): 163–167. doi: 10.11896/j.issn.1002-137X.2017.03.036. HUANG Yuhua, DAI Xuejun, SHI Yangyang, et al. Ultra-lightweight block cipher algorithm (PFP) based on Feistel structure[J]. Computer Science, 2017, 44(3): 163–167. doi: 10.11896/j.issn.1002-137X.2017.03.036.
[8]	BIHAM E and SHAMIR A. Differential cryptanalysis of DES-like cryptosystems[J]. Journal of Cryptology, 1991, 4(1): 3–72. doi: 10.1007/BF00630563.
[9]	MATSUI M. Linear cryptanalysis method for DES cipher[C]. The Workshop on the Theory and Application of Cryptographic Techniques on Advances in Cryptology (EUROCRYPT’93), Lofthus, Norway, 1993: 386–397. doi: 10.1007/3-540-48285-7_33.
[10]	HADIPOUR H, SADEGHI S and EICHLSEDER M. Finding the impossible: Automated search for full impossible-differential, zero-correlation, and integral attacks[C]. The 42nd Annual International Conference on the Theory and Applications of Cryptographic Techniques on Advances in Cryptology (EUROCRYPT 2023), Lyon, France, 2023: 128–157. doi: 10.1007/978-3-031-30634-1_5.
[11]	HADIPOUR H, GERHALTER S, SADEGHI S, et al. Improved search for integral, impossible differential and zero-correlation attacks[J]. IACR Transactions on Symmetric Cryptology, 2024, 2024(1): 234–325. doi: 10.46586/tosc.v2024.i1.234-325.
[12]	LAI Xuejia. Higher order derivatives and differential cryptanalysis[M]. BLAHUT R E, COSTELLO D J, MAURER U, et al. Communications and Cryptography: Two Sides of One Tapestry. Boston: Springer, 1994: 227–233. doi: 10.1007/978-1-4615-2694-0_23.
[13]	AHMADIAN Z, KHALESI A, M’FOUKH D, et al. Truncated differential cryptanalysis: New insights and application to QARMAv1-n and QARMAv2–64[J]. Designs, Codes and Cryptography, 2024, 92(12): 4549–4591. doi: 10.1007/s10623-024-01486-8.
[14]	BIHAM E. New types of cryptanalytic attacks using related keys[J]. Journal of Cryptology, 1994, 7(4): 229–246. doi: 10.1007/BF00203965.
[15]	ROHIT R and SARKAR S. Reconstructing s-boxes from cryptographic tables with MILP[J]. IACR Transactions on Symmetric Cryptology, 2024, 2024(3): 200–237. doi: 10.46586/tosc.v2024.i3.200-237.
[16]	CHAKRABORTY D, HADIPOUR H, NGUYEN P H, et al. Finding complete impossible differential attacks on AndRX ciphers and efficient distinguishers for ARX designs[J]. IACR Transactions on Symmetric Cryptology, 2024, 2024(3): 84–176. doi: 10.46586/tosc.v2024.i3.84-176.
[17]	WANG Dachao, WANG Baocang, and SUN Siwei. SAT-aided automatic search of boomerang distinguishers for ARX ciphers[J]. IACR Transactions on Symmetric Cryptology, 2023, 2023(1): 152–191. doi: 10.46586/tosc.v2023.i1.152-191.
[18]	ERLACHER J, MENDEL F, and EICHLSEDER M. Bounds for the security of ascon against differential and linear cryptanalysis[J]. IACR Transactions on Symmetric Cryptology, 2022, 2022(1): 64–87. doi: 10.46586/tosc.v2022.i1.64-87.
[19]	沈璇, 王欣玫, 何俊, 等. PFP算法改進的不可能差分分析[J]. 計算機科學(xué), 2020, 47(7): 263–267. doi: 10.11896/jsjkx.200200034. SHEN Xuan, WANG Xinmei, HE Jun, et al. Revised impossible differential cryptanalysis of PFP block cipher[J]. Computer Science, 2020, 47(7): 263–267. doi: 10.11896/jsjkx.200200034.
[20]	趙光耀, 沈璇, 余波, 等. 縮減輪的超輕量級分組密碼算法PFP的不可能差分分析[J]. 計算機應(yīng)用, 2023, 43(9): 2784–2788. doi: 10.11772/j.issn.1001-9081.2022091395. ZHAO Guangyao, SHEN Xuan, YU Bo, et al. Impossible differential cryptanalysis of reduced-round ultra-lightweight block cipher PFP[J]. Journal of Computer Applications, 2023, 43(9): 2784–2788. doi: 10.11772/j.issn.1001-9081.2022091395.
[21]	劉道瞳, 袁征, 魏錦鵬, 等. 輕量級分組密碼算法PFP和SLIM的積分分析[J]. 密碼學(xué)報, 2023, 10(3): 609–621. doi: 10.13868/j.cnki.jcr.000617. LIU Daotong, YUAN Zheng, WEI Jinpeng, et al. Integral cryptanalysis of lightweight block cipher PFP and SLIM[J]. Journal of Cryptologic Research, 2023, 10(3): 609–621. doi: 10.13868/j.cnki.jcr.000617.
[22]	李艷俊, 李寅霜, 楊明華, 等. 輕量級PFP算法的差分攻擊[J]. 計算機工程與應(yīng)用, 2023, 59(21): 296–302. doi: 10.3778/j.issn.1002-8331.2305-0193. LI Yanjun, LI Yinshuang, YANG Minghua, et al. Differential attack on lightweight PFP algorithm[J]. Computer Engineering and Applications, 2023, 59(21): 296–302. doi: 10.3778/j.issn.1002-8331.2305-0193.
[23]	COOK S A. The complexity of theorem-proving procedures[C]. The Third Annual ACM Symposium on Theory of Computing (STOC’71), Shaker Heights, USA, 1971: 151–158. doi: 10.1145/800157.805047.
[24]	DE MOURA L and BJ?RNER N. Z3: An efficient SMT solver[C]. The 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Budapest, Hungary, 2008: 337–340. doi: 10.1007/978-3-540-78800-3_24.
[25]	BARRETT C, CONWAY C L, DETERS M, et al. CVC4[C]. The 23rd International Conference on Computer aided verification (CAV 2011), Snowbird, USA, 2011: 171–177.
[26]	CIMATTI A, GRIGGIO A, SCHAAFSMA B J, et al. The MathSAT5 SMT solver[C]. The 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, 2013: 93–107. doi: 10.1007/978-3-642-36742-7_7.
[27]	BRUMMAYER R and BIERE A. Boolector: An efficient SMT solver for bit-vectors and arrays[C]. The 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), York, UK, 2009: 174–177. doi: 10.1007/978-3-642-00768-2_16.
[28]	GANESH V and DILL D L. A decision procedure for bit-vectors and arrays[C]. The 19th International Conference on Computer Aided Verification (CAV 2007), Berlin, Germany, 2007: 519–531. doi: 10.1007/978-3-540-73368-3_52.
[29]	STUMP A, BARRETT C W, and DILL D L. CVC: A cooperating validity checker[C]. The 14th International Conference on Computer Aided Verification (CAV 2002), Copenhagen, Denmark, 2002: 500–504. doi: 10.1007/3-540-45657-0_40.
[30]	SEL?UK A A. On probability of success in linear and differential cryptanalysis[J]. Journal of Cryptology, 2008, 21(1): 131–147. doi: 10.1007/s00145-007-9013-7.