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

許崢

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

許崢1,2

（1. 中國科學院信息工程研究所信息安全國家重點實驗室，北京 100093；2. 中國科學院大學網絡空間安全學院，北京 100049）

差分分析；差分特征；自動化搜索；SAT求解器

0 引言

20世紀90年代初，Biham和Shamir提出了差分分析[1]。差分分析最初是一種用于評估DES分組密碼安全性的密碼分析方法，后來被用于評估各種分組密碼的安全性。對于對稱密碼原語的密碼分析，差分分析是評估對稱密碼原語安全性的最強技術之一。此外，抗差分分析是現代分組密碼算法的主要設計標準。

對于差分分析，一個關鍵的步驟是找到高概率的差分特征。目前，使用自動化方法搜索差分特征已成為一種新趨勢。在1994年歐密會議上[2]，Matsui提出了一種分支定界算法來自動化搜索基于S盒的分組密碼的最優差分特征。后來，Matsui的算法被用于自動化搜索ARX密碼的差分特征[3-6]。

21世紀初期，自動化工具由于在搜索分組密碼的差分特征方面表現出優越的性能而備受關注。最重要的自動化工具之一是基于混合整數線性規劃（MILP）的方法。Mouha等[7]首次引入了該方法，并用其評估了差分、線性活躍S盒數量的下界。后來，上述方法被改進并應用于搜索面向比特的分組密碼的（相關密鑰）差分特征。此外，MILP方法被進一步應用于搜索各種類型的區分器[8-11]。

另一種備受關注的自動化工具是基于布爾可滿足性問題（SAT）的方法。2013年，Mouha等[12]首次引入了該方法，并將其用于搜索Salsa20的3輪最優差分特征。后來，在2015年美密會議上，K?lbl等[13]使用上述方法搜索SIMON的最優差分和線性特征。此外，SAT方法被進一步應用于搜索各種類型的區分器[14-18]。

為了使用上述自動化工具搜索差分特征，密碼分析者只需要將差分傳播轉化為相應的不等式或約束條件，這極大地簡化了密碼分析者的工作，并最大限度地減少了人為錯誤的可能性。然而，上述兩種自動化工具在搜索階段的執行效率取決于第三方求解器的性能、差分性質的等式/不等式的表示方式以及一些優化策略。

為了提高MILP方法的效率，密碼分析者提出了多種優化策略。2017年，Sasaki和Todo[19]對于描述S盒的差分傳播提出了一種確保不等式數量最少的方法。在2018年ISC會議上，Zhang等[20]通過將Matsui邊界條件加入MILP模型中來加速差分特征的搜索。2019年，Zhou等[21]利用差分特征概率與活躍S盒數量之間的關系優化差分特征的搜索。2020年，Boura和Coggia[22]對于SPN結構的S盒以及線性層提出了高效的MILP模型，以提高搜索效率。

然而，與MILP方法效率的提高相比，使用SAT方法對自動化搜索加速的研究相對滯后。2016 年，Song等[23]提出了一種啟發式的方法搜索ARX密碼更好的差分特征。2021年，Sun等[24]通過將Matsui邊界條件加入SAT方法中來加速差分特征的搜索。

當密碼分析者利用SAT方法搜索分組密碼的最優差分特征時，他們經常使用STP[25]以及CryptoMiniSat[26]。由于CryptoMiniSat支持多線程且STP支持多種詢問條件，本文提出以下兩個問題。①使用多線程是否可以加速搜索？②使用不同的詢問條件是否會影響搜索的耗時？因此，研究線程數和詢問條件的加速效果是十分重要的。

本文改進了文獻[24]中的方法，并且研究了線程數和詢問條件的加速效果，主要貢獻有以下3方面。

（1）改進的邊界條件

在文獻[24]中，Sun等將Matsui邊界條件轉化為合取范式（CNF）的形式并將其加入SAT方法中來加速差分特征的搜索。由于搜索空間可以被進一步減小，他們的方法可以被優化。為了進一步提高搜索效率，本文改進了Matsui邊界條件并提出了一種改進的方法搜索分組密碼的最優差分特征。

（2）選擇線程數以及詢問條件的策略

為了研究線程數和詢問條件的加速效果，本文使用STP和CryptoMiniSat分別搜索SPECK96和HIGHT的差分特征，并比較了在不同線程數和詢問條件下求解SAT/SMT問題的耗時。本文的實驗結果表明，線程數對搜索差分特征的耗時影響較大，而詢問條件對搜索差分特征的耗時影響較小。從而，本文提出了一種如何選擇線程數和詢問條件的策略，并發現STP會影響搜索的整體效率。

（3）自動化搜索HIGHT的11輪最優差分特征

1 符號、預備知識及算法簡介

1.1 符號

本文使用的符號及含義如表1所示。

表1 符號及含義

1.2 預備知識

定義2 模加的異或差分概率[27]

其中

1.3 SPECK簡介

圖1 SPECK輪函數

Figure 1 The round function of SPECK

1.4 HIGHT簡介

2 改進Matsui邊界條件

其中，表示（即輪最優差分特征中第i輪差分特征的概率）的以2為底數的對數的絕對值。下文將式(7)稱為邊界條件。

Figure 2 The round function of HIGHT

2.1 改進邊界條件

算法1 Sun等方法的搜索過程

4) end for

8) end for

9) 將邊界條件以及L-M條件轉化為CNF形式;

11) 調用SAT求解器CaDiCaL來確定是否存在輪最優差分特征;

12) if存在輪最優差分特征then

14) end if

15) if不存在輪最優差分特征then

17) end if

18) end while

算法2 改進后的帶改進的邊界條件的搜索過程

4) end for

9) end for

10) 將改進的邊界條件以及L-M條件轉化為CNF形式;

12) 調用SAT求解器來確定是否存在輪最優差分特征;

13) if存在輪最優差分特征then

15) end if

16) if不存在輪最優差分特征then

18) end if

19) end while

3 線程數和詢問條件的加速效果

當密碼分析者利用SAT方法搜索分組密碼的最優差分特征時，密碼分析者需要將搜索差分特征的問題轉化為布爾可滿足性問題（即SAT問題）。然而，SAT問題僅包含布爾變量以及布爾操作（AND、NOT以及OR），因此上述轉化過程十分復雜。相比之下，可滿足性模理論（即SMT）問題支持比特向量變量以及常用的比特向量操作。此外，SMT問題是SAT問題的推廣且SMT公式可以用更豐富的邏輯表達。因此，密碼分析者通常將搜索差分特征的問題轉化為SMT問題，并使用SMT求解器進行求解，過程如下。

1) 將搜索差分特征的問題轉化為SMT問題。

2) 利用SMT求解器將SMT問題轉化為SAT問題。

3) 利用SMT求解器調用SAT求解器求解SAT問題。

STP[25]是一種典型的SMT求解器，本文利用STP求解所有的SMT問題。

3.1 線程數的加速效果

STP的默認SAT求解器是MiniSAT[30]。然而，STP同樣支持其他的SAT求解器，如CryptoMiniSat[26]。由于CryptoMiniSat支持多線程且支持異或操作以及高斯消元，密碼學者經常利用CryptoMiniSat作為后端SAT求解器來求解SAT問題。因此，使用多線程是否可以加速搜索成為一個很自然的問題。

為了研究線程數的加速效果，本文使用STP和CryptoMiniSat分別搜索SPECK96和HIGHT的差分特征。

3.2 詢問條件的加速效果

為了將搜索差分特征的問題轉化為SMT問題，密碼分析者經常使用CVC語言描述異或差分傳播。當搜索差分特征時，一個常用的搜索策略是詢問在當前概率約束下是否存在有效的差分特征。上述策略所對應的詢問條件為QUERY (FALSE)，COUNTEREXAMPLE。

上述詢問條件被稱為錯誤詢問。當STP返回Invalid以及一條差分特征時，代表在當前概率約束下至少有一條有效差分特征。

直觀上看，使用上述搜索策略是很耗時的，尤其是在當前概率約束下沒有有效差分特征時。因此，替換詢問條件是否可以加速搜索成為一個很自然的問題。

3.3 線程數和詢問條件加速效果的實驗測試

3.3.1 追蹤差分傳播

（1）追蹤SPECK96中的差分傳播

利用如下約束條件追蹤SPECK96中的差分轉播。

（2）追蹤HIGHT中的差分傳播

利用如下約束條件追蹤HIGHT中的差分轉播。

其中，

3.3.2 線程數和詢問條件加速效果的實驗測試

本節分別利用1～30個線程搜索SPECK96以及HIGHT的差分特征并記錄耗時，從而實驗測試線程數的加速效果。此外，分別利用錯誤詢問以及輸入詢問搜索SPECK96以及HIGHT的差分特征并記錄耗時，從而實驗測試詢問條件的加速效果。

3.3.2.1 搜索SPECK96的差分特征

令=8且=24，測試線程數以及詢問條件的加速效果（以單線程+錯誤詢問為基準）。

（1）線程數的加速效果

①當詢問條件是錯誤詢問時

時間消耗隨著線程數增加的變化趨勢是：先減少，再增多，最后減少并趨于平穩。兩個轉折點分別是4線程以及11線程。

②當詢問條件是輸入詢問時

時間消耗隨著線程數增加的變化趨勢是：先減少，再增多并趨于平穩，最后減少并趨于平穩。兩個轉折點分別是5線程以及13線程。

（2）詢問條件的加速效果

當線程數不為5或者8時，利用錯誤詢問搜索差分特征的耗時與利用輸入詢問搜索差分特征的耗時之間沒有明顯的差距。實驗結果如圖3所示。

令=8且=25，測試線程數以及詢問條件的加速效果（以單線程+錯誤詢問為基準）。

（1）線程數的加速效果

①當詢問條件是錯誤詢問時

當線程數不超過11時，時間消耗隨線程數增加沒有明顯變化的規律：時間消耗從減少到增多的轉折點分別為2、4、6和10線程；時間消耗從增多到減少的轉折點分別為3、5和8線程。當線程數超過11且不超過20時，時間消耗隨著線程數的增加而減少。當線程數超過20且不超過30時（除了26），時間消耗隨著線程數的增加幾乎不變。當線程數為26時，時間消耗最少。

圖3 搜索SPECK96的概率為2?24的8輪差分特征的時間消耗比

Figure 3 The time consumption ratio of searching for 8-round differential characteristics with a probability of 2?24of SPECK96

②當詢問條件是輸入詢問時

當線程數不超過13時，時間消耗隨線程數增加沒有明顯變化的規律：時間消耗從減少到增多的轉折點分別為2、6、9和12線程；時間消耗從增多到減少的轉折點分別為4、7和11線程。當線程數超過13且不超過19時，時間消耗隨著線程數的增加先減少后增多，且轉折點為18線程。當線程數超過19且不超過30時，時間消耗隨著線程數的增加幾乎不變。

（2）詢問條件的加速效果

盡管在大多數情況下，利用錯誤詢問搜索差分特征的耗時少于利用輸入詢問搜索差分特征的耗時，然而，耗時之間的差距并不十分明顯。實驗結果如圖4所示。

圖4 搜索SPECK96的概率為2?25的8輪差分特征的時間消耗比

Figure 4 The time consumption ratio of searching for 8-round differential characteristics with a probability of 2?25of SPECK96

令=8且=26，測試線程數以及詢問條件的加速效果（以單線程+錯誤詢問為基準）。

（1）線程數的加速效果

①當詢問條件是錯誤詢問時

時間消耗隨著線程數增加的變化趨勢分為5個階段（減少→增多→減少→增多→減少并趨于平穩）。4個轉折點分別是2、7、10以及13線程。

②當詢問條件是輸入詢問時

當線程數不超過6時，時間消耗隨線程數增加沒有明顯變化的規律：時間消耗從減少到增多的轉折點分別為3線程和5線程；時間消耗從增多到減少的轉折點為4線程。當線程數超過6時，時間消耗隨著線程數增加的變化趨勢是：先減少并趨于平穩，后增多。轉折點為25線程。

（2）詢問條件的加速效果

盡管在大多數情況下，利用錯誤詢問搜索差分特征的耗時少于利用輸入詢問搜索差分特征的耗時，然而，耗時之間的差距并不十分明顯。實驗結果如圖5所示。

圖5 搜索SPECK96的概率為2?26的8輪差分特征的時間消耗比

Figure 5 The time consumption ratio of searching for 8-round differential characteristics with a probability of 2?26of SPECK96

3.3.2.2 搜索HIGHT的差分特征

令=11且=39，測試線程數以及詢問條件的加速效果（以單線程+錯誤詢問為基準）。

（1）線程數的加速效果

①當詢問條件是錯誤詢問時

時間消耗隨著線程數增加的變化趨勢是：先減少并趨于平穩，再增多，最后減少并趨于平穩。兩個轉折點分別是11線程以及12線程。

②當詢問條件是輸入詢問時

時間消耗隨著線程數增加的變化趨勢分為5個階段（減少→增多→減少并趨于平穩→增多→減少并趨于平穩）。4個轉折點分別是2、3、9以及11線程。

（2）詢問條件的加速效果

圖6 搜索HIGHT的概率為2?39的11輪差分特征的時間消耗比

Figure 6 The time consumption ratio of searching for 11-round differential characteristics with a probability of 2?39of HIGHT

根據實驗結果發現，線程數對搜索差分特征的耗時影響較大，而詢問條件對搜索差分特征的耗時影響較小。對于相同的分組密碼，盡管時間消耗隨著線程數增加變化的總體趨勢是減少的，但“使用較多線程數導致較高耗時”的情況并不罕見，因此，盲目地選擇較多的線程數可能會導致更低的搜索效率。并且，對于不同的分組密碼，線程數的加速效果是不同的。此外，利用兩個線程搜索差分特征的耗時基本低于利用單線程搜索差分特征的耗時。因此，對于某個特定的分組密碼，如果密碼分析者在搜索差分特征之前沒有實驗測試線程數的加速效果（如同本文所做的實驗），利用兩個線程搜索差分特征將是一個較好的選擇。

對于上述4組實驗，有對應的4組SMT問題。需要注意的是，每組SMT問題中的兩個SMT問題僅詢問條件不同。利用STP將這8個SMT問題轉化為對應的8個SAT問題。然而，每組SAT問題中的兩個SAT問題是完全相同的。這就意味著，僅改變詢問條件將不會影響CryptoMiniSat的求解效率。因此，利用錯誤詢問搜索差分特征的耗時與利用輸入詢問搜索差分特征的耗時之間的差距是STP引起的。這意味著STP會影響搜索的整體效率。

在上述實驗中，時間消耗隨著線程數的增加先減少后增加的情況多次出現。然而，上述現象出現的線程數位置以及范圍均無明顯規律，可能與以下兩個原因有關：線程增加導致線程調度時間開銷增加；第三方求解器的內部優化邏輯不夠完善。此外，線程數增加到一定數量時，時間消耗趨于平緩而無法進一步降低，可能與以下原因有關：采用多線程進行搜索時，多個線程要操作同一個數據集合，線程狀態將頻繁改變，導致在線程數達到某個閾值時，線程數的增加無法進一步提高程序的性能。

4 自動化搜索HIGHT的11輪最優差分特征

表2 HIGHT的11輪最優差分特征

5 結束語

本文嘗試利用SAT方法進一步加速差分特征的搜索，通過改進邊界條件從而降低搜索空間。密碼分析者經常使用STP以及CryptoMiniSat搜索差分特征，因此本文研究了線程數以及詢問條件的加速效果，并實驗測試了線程數以及詢問條件的加速效果。根據實驗結果發現，線程數對搜索差分特征的耗時影響較大，而詢問條件對搜索差分特征的耗時影響較小。此外，本文提出了一種選擇線程數的策略，利用該搜索策略，首次獲得了HIGHT的11輪最優差分特征的緊致概率，且結果是已有最優的結果。希望本文提出的搜索策略不僅有助于評估分組密碼抗差分分析的安全性，而且有助于分組密碼的設計。

[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]//Inte- rnational 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]//Inter- national 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]//Inte- rnational Conference on Theory and Applications of Satisfiability Testing. 2003: 502-518.

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

XU Zheng1,2

1. State Key Laboratory of Information Security, Institute of Information Engineering, Chinese Academy of Sciences, Beijing 100093, China 2. School of Cyber Security, University of Chinese Academy of Sciences, Beijing 100049, China

differential cryptanalysis, differential characteristics, automatic search, SAT solver

TP309.7

A

10.11959/j.issn.2096?109x.2022066

2021?11?15；

2022?03?30

許崢，xuzheng@iie.ac.cn

國家自然科學基金（61772516，61772517）

The National Natural Science Foundation of China (61772516, 61772517)

許崢.基于SAT方法進一步加速差分特征的搜索[J]. 網絡與信息安全學報, 2022, 8(5): 129-139.

Format: XU Z. 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.

許崢（1992? ），男，河南鄭州人，中國科學院信息工程研究所博士生，主要研究方向為分組密碼的分析與設計。