苗旭東，董新鋒，韓 羽，穆道光，張文政

（1.中國電子科技集團公司第三十研究所，四川 成都 610041；2.保密通信重點實驗室，四川 成都 610041）

0 引 言

差分和線性分析是分組密碼的兩種最基本的安全性分析評估方法，對于分組較大（64 比特以上）且S 盒尺寸較大（4 比特以上）的密碼算法而言，一般通過搜索活躍S 盒的個數(shù)來評估密碼算法抵抗差分和線性分析的能力，目前通常采用基于分支定界[1]和混合整數(shù)線性規(guī)劃[2]（Mixed Integer Linear Programming，MILP）的自動化搜索方法?；诜种Фń绲拿艽a分析技術(shù)的提出時間較早，建模相對復雜，而基于MILP和 布 爾 可 滿 足 性 問 題[3]（Boolean Satisfiability Problem，SAT）的密碼分析技術(shù)是近年來提出的方法，建模相對簡單。兩種方法都屬于約束規(guī)劃問題，算法分析人員只需考慮如何將密碼分析問題轉(zhuǎn)換為兩種約束規(guī)劃問題，不需要考慮如何求解計算的問題。MILP 和SAT 具有自動化集成度高、求解器計算能力強、密碼分析效果好的特點，已成為目前行業(yè)較為通用的兩種密碼自動化分析技術(shù)。

2013 年，Mouha 等 人[3]首 次 提 出 了 基 于SAT 的最優(yōu)差分特征分析技術(shù)，并成功得到了ARX 結(jié)構(gòu)算法Salsa20 的3 輪最優(yōu)差分特征，由于SAT 求解器的計算能力強，SAT 語句（合取范式）的表達能力強，基于SAT 的密碼分析技術(shù)很快被應用到密碼算法的多種安全性分析技術(shù)中[4-6]。截至目前，基于SAT 的密碼自動化分析方法主要包括：比特級的最優(yōu)差分和線性特征分析、比特級和字節(jié)級的積分可分性分析等，還沒有基于SAT 的差分和線性活躍S 盒分析方法?；诖耍疚膶θ绾螌⒉罘趾途€性活躍S盒搜索問題轉(zhuǎn)化為SAT 問題進行研究，目的是使SAT 成為密碼算法安全性分析和評估的一種更為通用的方法。

1 密碼基本部件建模

由于公開文獻中沒有對基于SAT 的差分和線性活躍S 盒分析技術(shù)的研究，唯一可借鑒的是基于MILP 的差分和線性活躍S 盒分析技術(shù)，兩種分析技術(shù)中關(guān)鍵的一步是將密碼基本部件的差分和線性傳播行為用相應的語句刻畫?；赟AT 的密碼分析技術(shù)需要將密碼分析問題轉(zhuǎn)換為SAT 模型，本質(zhì)上是將密碼基本部件的差分和線性傳播行為用合取范式（與、或、非3種操作）表示，由于差分和線性活躍S 盒分析是一種字節(jié)級的建模方法，本文首次提出了字節(jié)級分支、異或、最大距離可分碼（Maximum Distance Separable Codes，MDS）合取范式刻畫，并介紹了具體的刻畫方法。

1.1 字節(jié)級分支操作

字節(jié)級分支操作如圖1 所示，其中，x 為代表輸入差分或掩碼，y 和z 為分成兩支的輸出差分或掩碼。

分支操作的差分傳播模式為(x →y, z)，所有可能的傳播模式的真值表點有：

分支操作的線性掩碼傳播模式為(x →y, z)，所有可能的傳播模式的真值表點有：

用合取范式表達線性掩碼傳播的真值表點為：

1.2 字節(jié)級異或操作

字節(jié)級異或操作如圖2 所示，x 和y 代表輸入差分或掩碼，z 為經(jīng)過異或后的輸出差分或掩碼。

由于差分和線性分析存在對偶特征，字節(jié)異或的差分傳播行為和字節(jié)分支的線性傳播行為是相同的，因此，字節(jié)異或的差分傳播行為的合取范式為：

同上，字節(jié)異或的線性傳播行為和字節(jié)分支的差分傳播行為是相同的，因此，字節(jié)異或的線性傳播行為的合取范式為：

1.3 MDS 矩陣

MDS 矩陣常用于SPN、Feistel 結(jié)構(gòu)密碼算法的線性擴散層中，例如，AES 域構(gòu)造的線性擴散層和Dblock 基于循環(huán)移位的線性擴散層均可按字節(jié)為單位當作4×4 的MDS，如圖3 所示。

假設(shè)MDS矩陣的輸入差分或掩碼為a,b,c,d，經(jīng)過MDS 后的輸出差分或掩碼為e,f,g,h，(a,b,c,d,e,f,g,h)變量的值取0 或1，分別代表相應字節(jié)的差分或掩碼值為0 或非0，由于MDS 矩陣的差分和線性分支數(shù)均為5，在活躍S 盒分析中，僅利用了該性質(zhì)，不會考慮MDS 的具體實施細節(jié)。因此，利用差分和線性活躍S 盒分析方法時，對MDS 的刻畫是相同的，本文僅考慮分支數(shù)為5 的刻畫方法，如下文所述。

考慮所有的輸入輸出可能模式，即當輸入非零時，輸入輸出至少有5 個字節(jié)非零，共種情況；當輸入為零時，輸出為零，僅1 種情況。因此，可能的傳播模式共94 種，而不可能的傳播模式有256-94=162 種，采用邏輯刻畫[6]的方法需要162 個邏輯表達式。利用邏輯表達式優(yōu)化技術(shù)，將所有94 種可能的傳播模式的真值表點輸入到Logic Friday 軟件中，再執(zhí)行Product of Sum 操作，將真值表點轉(zhuǎn)換為SAT 語言的合取范式，共162 條。表達式過多會影響SAT 求解器的求解效率，還需做進一步的優(yōu)化。利用Logic Friday 軟件集成的Quine-McCluskey 和Espresso 算法求解出一個最少數(shù)量的合取范式，最終僅用70 個表達式表示，具體如下：

本節(jié)僅考查了線性擴散層為MDS 矩陣時的一種通用建模方法，當面對幾乎MDS 矩陣、0/1線性擴散矩陣等其他線性擴散層時，均可采用該方法建立模型。

2 搜索策略設(shè)置

本文介紹了密碼基本部件的建模方法，在分析一個具體的密碼算法時，首先，根據(jù)密碼算法中部件的先后順序建立相應的SAT 模型；其次，根據(jù)不同的分析方法，對初始條件、目標值進行設(shè)置；最后，調(diào)用一個求解算法，對SAT 模型進行求解，才能得出最終的分析結(jié)果。

2.1 初始條件設(shè)置

假設(shè)分組密碼的分組長度為m，輸入差分或掩碼為x0,x1,…,xm-1，為避免SAT 問題出現(xiàn)平凡的全零解，須設(shè)置輸入差分或掩碼非零，合取范式為：

2.2 目標條件設(shè)置

假設(shè)待分析算法中S 盒的個數(shù)為n，統(tǒng)計活躍S 盒的變量為x0,x1,…,xm-1，要判定活躍S 盒的個數(shù)總和是否達到一個指定值k，即判定SAT 問題是否有可滿足解，用線性不等式表示：

由于合取范式不支持線性不等式表示，須將線性不等式轉(zhuǎn)換為合取范式，采用序列編碼方法[7]，將該問題轉(zhuǎn)化為合取范式，序列編碼電路如圖4 所示。

將以上電路轉(zhuǎn)換為合取范式表示為[7-8]：

式中：si,j為輔助計數(shù)變量，取值均為0 或1。

將該約束條件寫入SAT 模型即可判斷指定活躍S 盒個數(shù)是否有可滿足解。

2.3 搜索算法

按照本文中密碼基本部件的建模方法和約束條件設(shè)置方法，建立了密碼算法活躍S 盒搜索的SAT 模型，交給SAT 求解，并利用以下算法求解活躍S 盒的個數(shù)，基本方法為先給SAT模型設(shè)置一個較小的目標值，使模型沒有滿足解，再逐漸增大目標值，當SAT 模型有滿足解時，該目標值即為活躍S 盒的個數(shù)。算法1：基于SAT 的活躍S 盒搜索算法輸入：SAT 模型，活躍S 盒個數(shù)初始值k輸出：最小活躍S 盒個數(shù)k

1 將活躍S 盒個數(shù)k 設(shè)定為一個最小值0；

2 將SAT 模型交給CaDiCaL 求解

3 若得到不滿足解

則k=k+1，并返回步驟2

4 若得到滿足解

返回k 的值

3 實際應用效果

為了驗證本文提出的搜索活躍S 盒方法的實際應用效果，對經(jīng)典SPN 結(jié)構(gòu)的AES 算法和Feistel 結(jié)構(gòu)的Dblock 系列算法的活躍S 盒個數(shù)進行搜索，由于兩個算法的差分和線性活躍S盒相同，統(tǒng)一用活躍S 盒表示。實施效果如表1、表2 所示。

表1 AES 活躍S 盒個數(shù)

表2 Dblock-128 活躍S 盒個數(shù)

從表1 和表2 可以看出，利用SAT 技術(shù)對組長度為128 比特的密碼算法活躍S 盒進行搜索時，所需時間較短，通常在幾分鐘內(nèi)就可以給出搜索結(jié)果。但從表1 也可以看出搜索AES算法8 輪活躍S 盒的時間偏長，原因在于7 輪到8 輪的活躍S 盒個數(shù)差值較大，搜索算法需要判斷16 次才能給出一個滿足的解。

從表3 可以看出，利用SAT 技術(shù)對分組長度大于128 比特的密碼算法活躍S 盒進行搜索時，所需時間較長，表3 中“時間”為未采用任何加速方法的搜索結(jié)果，搜索時間相對較長，為了提高搜索效率，本文借鑒文獻[8]中的加速方法，將Matsui 的分支定界搜索策略融入SAT模型中，起到加速作用，表3 中“加速時間”一列為加速后的搜索時間，可以看到，在搜索長輪數(shù)的模型時加速效果顯著。

對于Dblock-256 而言，由于分組長度較大，模型更加復雜，搜索時間過長，利用本文提出的方法結(jié)合加速策略僅搜索到17 輪，如表4 所示。

表3 Dblock-192 活躍S 盒個數(shù)

表4 Dblock-256 活躍S 盒個數(shù)

從整體搜索效果來看，在借助分支定界的加速策略條件下，基于SAT 的活躍S 盒搜索方法基本滿足活躍S 盒搜索需求?？梢运阉鞒龇纸M較大達到安全性輪數(shù)的活躍S 盒個數(shù)。

4 結(jié) 語

本文提出了一種新的基于SAT 的差分和線性活躍S 盒搜索方法，可以用較少的合取范式子句刻畫字節(jié)級分支、異或、MDS 的差分和線性傳播行為，給出了詳細的建模和搜索方法，并利用該方法成功搜索出AES、Dblock 系列算法的活躍S 盒個數(shù)，實際使用效果較好。將基于SAT的密碼分析技術(shù)從比特級擴展到字節(jié)級，使得SAT 成為一種更加通用的密碼分析方法。但面對分組更大（分組長度大于256 比特）的密碼算法活躍S 盒時，該方法也很難計算出完整輪的活躍S 盒，因此，在后續(xù)的研究中將著重優(yōu)化模型和提升本方法的搜索效率。