基于混合整數線性規劃模型的SPONGENT S盒緊湊約束分析

石一鵬，劉 杰*，祖錦源，張 濤，張國群

（1.西北工業大學 軟件學院，西安 710129；2.上海機電工程研究所，上海 201109）

0 引言

SPONGENT［1-2］是一種基于海綿結構的輕量級哈希函數，它的作用是針對可變長度有限位的輸入，通過吸收、壓縮等步驟輸出一個固定位數的哈希值。在SPONGENT 中，使用了類 似PRESENT［3］的基于代換-置換網 絡（Substitution-Permutation Network，SPN）結構的輪函數，該輪函數的輸入是經過有限步簡單處理的原始輸入信息，輸出是最終生成的哈希值。因此，輪函數是SPONGENT 中生成哈希值的關鍵結構，對SPONGENT 的差分密碼分析，最重要的就是針對輪函數分析差分密碼。

差分密碼分析是針對現代分組密碼最有效、最著名的攻擊方法之一，目前已經應用到很多密碼的攻擊中，因此抵抗差分攻擊的能力也逐漸成為評估加密算法安全性能的基本要求。Ankele 等［4］針對Sparx-64/128 分析了15 和16 輪的差分特征；ElSheikh 等［5］針對CRAFT 算法分析了差分密碼；Ji等［6］針對GIFT-64 和GIFT-128 展開了密鑰相關的差分路徑搜索；楊繼林等［7］針對類CLEFIA 動態密碼結構分析了差分特征。

同時，很多基于差分密碼分析的新的密碼分析方法也逐漸誕生，并廣泛應用于多種密碼算法的安全性分析中，如Wei 等［8］對TWINE 算法展 開了不 可能差 分密碼分析；Moghaddam 等［9］對Midori、SKINNY 和CRAFT 算法展開了截斷差分分析；Hutahaean 等［10］對小型PRESENT 算法展開了飛去來器分析（boomerang attack）；陳少真等［11］對GOST2 算法展開了密鑰相關攻擊等。

差分密碼分析的基本思想是通過研究密碼輸入差分和輸出差分之間的關系猜測密鑰，為了提高攻擊成功的概率，需要尋找一條高概率的差分路徑；然而密碼在經過數輪迭代之后產生的差分可能十分復雜，分析處理時可能面臨十分龐大的數據量。

Mouha 等［12］提出將混合整數線性規劃（Mixed Integer Linear Programming，MILP）模型應用于差分路徑的自動搜索，為尋找高概率的差分路徑提供了一種全新的思路，通過這種方法可以有效地找到活動S 盒數量的下限。但最初提出的模型忽略了S 盒自身的差分特性，不能夠用于面向位進行處理的加密算法，如PRESENT［3］、LS-Design（Linear-Sbox-Design）［13］、GIFT［14］等。Sun 等［15］使用描述S 盒可能和不可能差分模式的方法，將Mouha 等［12］提出的模型擴展到了面向位的密碼算法的差分分析中；但是該S 盒描述方法不能保證得出描述S 盒的最優方式。Sasaki 等［16］在文獻［15］的基礎上改進了MILP 模型，提出了一種新的約簡算法，獲得了理論上的最優描述，大幅提高了差分路徑搜索的效率。此后MILP 模型在差分密碼分析中有了更多的應用。如，Zhu 等［17］基于MILP 模型對GIFT-64 展開了12 輪差分特征的研究；Bagherzadeh 等［18］基于MILP 模型對LEA 和HIGHT 分析了差分密碼；Kumar 等［19］基于MILP 模型對WARP 分析了18 輪和19 輪的差分特征。

基于以上的分析，針對SPONGENT 的輪函數應用MILP模型進行差分路徑搜索時，可以較好地解決SPONGENT 差分路徑搜索效率低下的問題。由此，將SPONGENT 差分路徑搜索問題轉變為針對它的輪函數進行MILP 建模的問題；而對于具有典型SPN 結構的輪函數，建立MILP 模型，最重要的步驟就是尋找S 盒的最優描述。所謂“最優”，就是在不違背S盒所規定差分模式的條件下最大限度地減少冗余不等式的數量，即尋找一種“緊湊約束”。本文基于約簡算法［16］分析了SPONGENT 的S 盒的緊湊約束。此外，無法忽略一個事實——即使約簡算法［16］在應用過程中展現了很好的實際效果，但是目前仍沒有一種嚴謹的方法證明所得到約束結果的緊湊性。因此，本文提出了一種可能的方法，從約束條件存在必要性的角度驗證所得到約束的緊湊性。

本文的主要工作為：

1）使用不等式對SPONGENT 中S 盒所有差分模式的最小凸集描述，得到287 個不等式，應用約簡算法［16］在287 個不等式中篩選，首次得到了一組由23 個不等式組成的約束。

2）提出了一種評價約束條件必要程度的指標，并給出了基于該指標的約束緊湊性驗證算法，用于對所得到的不等式約束驗證緊湊性。針對所得到的SPONGENT S 盒的約束應用該算法，結果表明，所得到的約束中，每一個不等式都是不可替代的，即23 個不等式組成的約束對于SPONGENT 的S 盒是緊湊的。

1 SPONGENT

1.1 SPONGENT的版本參數

SPONGENT 是一個基于海綿結構的哈希函數家族，根據不同的散列輸出值的位數（size）、capacity和rate，SPONGENT可以被分為13 個版本，不同的版本對應不同的加密輪數和安全等級。表1 以SPONGENT-size/capacity/rate的參數化形式標識不同的版本，并給出了每一個版本對應的和運算輪數（round）。其中：state是參與SPN 結構輪函數運算部分的位數；rate是state中參與異或運算的位數，也是輸入信息分塊處理的單位；capacity是state中不參與異或運算部分的位數，3 個參數滿足state=rate+capacity。

表1 SPONGENT版本參數Tab.1 SPONGENT version parameters

由表1 可知，SPONGENT 共有5 種長度的散列值輸出，由SPONGENT-size表 示，分別為SPONGENT-88、SPONGENT-128、SPONGENT-160、SPONGENT-224 和SPONGENT-256。

1.2 SONGENT的計算過程

對于輸入的消息，SPONGENT 進行以下3 個階段的操作計算輸出：

1）初始化階段：將輸入信息的位數擴展成為rate的整數倍，再將它分割為若干個rate位的分塊。

2）吸收階段：將初始化階段得到的若干個分塊逐步與state的前rate位異或運算。

3）壓縮階段：通過SPN 結構的輪函數逐步計算得到輸出值。

1.3 SONGENT中的輪函數

在SPONGENT 所用的輪函數中主要進行以下運算：

1）state與輪常數及其反序值進行異或運算，根據state的位數不同，輪常數相應的初值不同。

2）state通過S 盒完成字節代換，每一次代換的字節由4位組成，使用b表示state的位數，每一輪需要進行b/4 個平行運算。表2 為S 盒規格的16 進制表示，x經過代換變為S(x)。

表2 S盒規格的16進制表示Tab.2 Hexadecimal representation of S-box specification

3）state進行P 盒置換運算，這里的P 盒與PRESENT 所用P 盒的置換規則類似，都是一種寬軌跡策略的運算。第i位的值被置換到第P（i）位，運算規則為：

本文重點分析S 盒的緊湊約束，對于輪函數的運算過程不作更多討論。在得到S 盒的緊湊約束之后可以針對輪函數的結構建立更加高效的MILP 模型，從而進行更高效的差分密碼分析。

2 MILP在最優差分路徑搜索中的應用

MILP 應用于差分路徑搜索之前，已經在很多領域發揮過重要的作用，它的含義可分為“混合整數”以及“線性規劃”兩部分。“線性規劃”即表明這是一種使用變量約束和不等式約束對目標函數優化的數學方法；“混合整數”則強調其中的一些變量被限制為整數值，而其他變量可以是二進制值或連續值。對于最優差分路徑的搜索，可以使用相應的變量約束和不等式約束描述可能的差分路徑，并將差分路徑的概率作為目標函數，該MILP 模型的解即對應最優的差分路徑。

2.1 文獻［12］分析框架

Mouha 等［12］提出將MILP 應用到差分路徑分析時，給出了針對SPN 結構3 種常見操作的不等式分析。

2.1.1 異或操作不等式分析

使用Xin1、Xin2表示異或運算的輸入差分，Xout表示相應的輸出差分，3 個參數之間的關系可以表示為：

其中⊕表示異或運算。可以發現，當且僅當Xin1與Xin2值都為0 時，Xout的值為0，否則3 個參數之間至少有兩個值不為0。使用一個虛擬變量d∈{0，1}輔助表示這種關系：

2.1.2 線性操作不等式分析

使用w(x)表示一個向量x的漢明重量，差分分支數BD滿足以下公式：

2.1.3 S盒操作不等式分析

對于雙射的S 盒，當且僅當輸入差分為0 時，輸出差分也為0。即滿足以下公式：

2.2 收緊MILP可行域的方法

利用文獻［12］的方法針對SPN 加密結構建立MILP 模型之后，就可以針對不等式約束求解，最優的差分路徑就是不等式解空間中的一個解。

然而，針對面向位的密碼算法，在龐大的解空間中尋找最優的差分路徑并不比應用MILP 之前更容易；并且，在這個解空間中很多差分路徑是不可能出現的。因此需要尋找到一種收緊MILP 可行域的方法，盡可能多地剔除不可能出現的差分路徑，以縮小最優差分路徑的搜索范圍。

通過添加不等式約束條件排除不可能的差分模式，就可以有效排除很多不可能差分路徑，這樣的不等式約束被稱為截斷不等式。

Sun 等［15］提出了兩種生成截斷不等式的方法：針對統計規律邏輯建模，以及差分模式最小凸集的H-表示。由于受到統計規律的限制，針對統計規律邏輯建模的方式并不適用于大多數加密結構，因此以下主要介紹差分模式最小凸集的H-表示。

定義1將S 盒所有可能的差分模式描述為一個離散點集，這個點集的最小凸集可以表示為若干不等式的公共解，那么稱這一組不等式為S 盒所有可能差分模式最小凸集的H-表示。

例如，S 盒的輸入差分為x=1001 時，可能的輸出差分為y=1001 或y=1100，輸入差分為x=1011 時，可能的輸出差分為y=1011 或y=1110。使用（x3，x2，x1，x0，y3，y2，y1，y0）表示一個差分模式，那么所有可能的差分模式組成的點集為｛（1，0，0，1，1，0，0，1），（1，0，0，1，1，1，0，0），（1，0，1，1，1，0，1，1），（1，0，1，1，1，1，1，0）｝，最小凸集的H-表示為：

S 盒所有可能差分模式最小凸集的H-表示中含有大量有效的截斷不等式。

2.3 獲取緊湊約束的方法

隨著可能差分模式的增多，最小凸集H-表示的不等式會越來越多，例如PRESENT 中S 盒所有可能差分模式最小凸集的H-表示為327 個不等式。這樣龐大的不等式組合極其冗雜，導致MILP 在有限時間內難以完成求解。然而，由于不可能的差分模式是有限的，排除所有不可能的差分模式并不需要如此多的不等式，只需要選擇可以排除所有不可能差分模式的截斷不等式組合就可以達到收緊可行域的目的。因此可以在不影響原有約束有效性的同時盡可能地減少不等式的數量，以便不等式求解，即所謂得到緊湊約束的過程。

為了盡可能地減少不等式數量，Sun 等［15］利用貪心算法的思想篩選不等式：依次選擇可以排除更多不可能差分模式的不等式，直到所有的不可能差分都被所選擇的截斷不等式排除。

使用該貪心算法可以得到一個較優解，但無法保證所得到的不等式數量是最少的；并且對于可以排除相等數量不可能差分模式的截斷不等式，并沒有明確給出選擇的優先級。基于這種情況，Sasaki 等［16］提出了一種新的約簡算法，應用MILP 選擇最優不等式組合，它的基本步驟為：首先計算每個不可能的差分模式可以被哪些不等式排除，得到一個關于不可能差分模式和截斷不等式之間的指導二維表，如表3 所示，單元值為1 表示它對應的不可能差分模式可以被對應的截斷不等式排除；然后設定約束條件為每一個不可能差分模式至少被一個不等式所排除，同時設定每一個不等式最多可以選擇一次；最后設定目標函數為最少的不等式數量，進行MILP 求解。

表3 指導二維表樣例Tab.3 Example of 2D guidance table

3 SPONGENT S盒的約束分析

為了尋找S 盒的緊湊約束，本章使用Sasaki 等［16］提出的約簡算法展開具體分析，主要步驟包括：計算所有可能的差分模式、求解截斷不等式和縮減不等式數量。

3.1 計算所有可能的差分模式

求解SPONGENT 中S 盒所有可能的差分模式，得到輸入-輸出差分表，如表4 所示。

表4 輸入-輸出差分表Tab.4 Input-output difference table

例如，輸入差分x=0001 時，可能的差分輸出有：y=0011，y=0101，y=1011，y=1101，則可能的差分模式包括（0，0，0，1，0，0，1，1），（0，0，0，1，0，1，0，1），（0，0，0，1，1，0，1，1），（0，0，0，1，1，1，0，1）。

3.2 求解截斷不等式

根據表4 可以得到97 個可能的差分模式，對應97 個點，使用SageMath 中的函數inequality_generator（）計算得到它的凸集的H-表示，共含有287 個不等式：

對所有的不等式按照順序從0 開始編號，以便下一步計算，最后一個不等式的編號為286。使用變量Ij∈{0，1}(j∈{0，1，…，286})表示每一個不等式。

3.3 縮減不等式數量

計算所有不可能的差分模式，共有256 -97=159 個，并對所有的不可能差分模式從0 開始編號，最后一個不可能差分模式編號為158。

然后應用約簡算法［16］，得到了類似表3 的159×287 的二維表，如可以排除第20 個不可能差分模式（1，1，1，0，1，0，0，0）的不等式有I23，I28，I41，I193，I223和I242：

令Ij=1 表示選擇保留這個不等式，Ij=0 表示不保留該不等式，則由第20 個不可能差分模式可以得到約束條件為：

對全部不可能差分模式進行以上步驟，可以得到關于Ij的159 個不等式約束，求解得

對應值為1 的不等式為：

上述不等式組即為所求S 盒的約束。

4 緊湊性驗證

4.1 緊湊性驗證算法

4.1.1 約束不等式集合的緊湊性

在S 盒所有可能差分模式最小凸集的H-表示中，每一個截斷不等式可以排除的不可能差分模式會有重合的部分，如表3 中，不等式1 和3 都能排除不可能差分模式1，不等式1、2和N都能排除不可能差分模式2。這種重合的情況在最終所求得的不等式約束集合中同樣存在，而這恰恰是發現不等式約束集合可能存在冗余的一個重要突破口。

為了更好地表示這種冗余的情況，本文使用一個具體的案例說明。如表5 所示，使用Qi表示待選擇的截斷不等式，使用Ij表示需要被排除的不可能差分模式，當單元格值為1時，表示它對應的不可能差分模式可以被對應的截斷不等式排除，表5 中Q1到Q8所能排除的不等式數量為降序排列。

表5 冗余不等式約束案例Tab.5 Case of redundant inequality constraints

針對表5 中的數據應用貪心算法［15］篩選不等式，依次選取可以排除不可能差分模式最多的截斷不等式，直到所有的不可能差分模式都被排除，得到的篩選結果為Q1、Q2、Q3、Q4、Q5。不難發現，Q1排除的不可能差分模式都可以被Q2、Q3、Q4、Q5組成的其他不等式組排除，不等式Q1對整個不等式約束集合就是冗余的。刪去Q1對于不等式約束集合排除不可能差分模式的能力沒有任何影響，但是卻可以減輕運算的負擔，提高差分路徑搜索的效率。

使用MILP 模型進行S 盒約束不等式求解的目標，是希望使用盡可能少的不等式描述S 盒所容許的差分模式，并且排除所有不可能的差分模式。由于求解關注的重點之一是不等式的數量，因此一切可能導致不等式約束集合存在冗余的情況都應當被排除，這對于差分路徑搜索復雜度的提升具有重要的意義。無論使用哪一種算法求解不等式約束集合，都應當保證最終的求解結果自身是緊湊的。為此，需要針對不等式約束集合驗證緊湊性。

遺憾的是，目前尚未有一種方法能夠針對不等式約束集合的緊湊性驗證，為此，本文提出一種可行的方法。

4.1.2 緊湊性驗證算法

為了驗證不等式約束集合的緊湊性，本文首先定義了一個評價約束條件必要程度的指標“必要度”，使用參數Necessity∈{0，1，…}表示，定義如下：

定義2對于一個約束條件，在整個約束條件集合中由該條件唯一排除的不可能差分模式的數量定義為該約束條件的必要度。

當一個不等式的必要度為0 時，表示該不等式對于約束組合是非必要存在的。此時，原不等式約束集合就是不緊湊的，一個緊湊的不等式約束集合至少不能包含該不等式。

基于約束不等式的必要度，本文提出了一種驗證約束條件集合緊湊性的算法，如算法1 所示。

算法1 驗證約束條件集合緊湊性的算法。

4.1.3 算法的正確性及應用

算法1 是基于“必要度”的概念設計的。對于一個不等式約束集合，算法1 能夠計算每一個不等式的必要度，當不等式約束集合中存在必要度為0 的不等式時，則判定該不等式約束集合是不緊湊的；反之，若所有不等式的必要度都不為0，則判定該不等式約束集合是緊湊的。

由于“必要度”代表一個不等式能夠唯一排除的不可能差分模式的數量，當不等式約束集合中存在必要度為0 的不等式時，表明該不等式所排除的每一個不可能差分模式都能被其他不等式所排除，去除這個不等式對于不等式約束集合整體排除不可能差分模式的能力沒有影響，因此當前的不等式約束集合存在冗余不等式，是不緊湊的；同樣，若每一個不等式的必要度都非0，則表明每一個不等式都至少有一個不可能差分模式是其他所有的不等式都不能排除的，若去除其中某個不等式，新的不等式約束集合就無法排除對應的不可能差分模式，因此當前不等式約束中的每一個不等式都有存在的必要，當前的不等式約束集合是緊湊的。由此可以證明，算法1 能夠準確判定一個不等式約束集合的緊湊性。

對于表5 中所示案例，使用Sun 等的貪心算法［15］得到的約束不等式集合與使用本文算法1 優化得到的約束不等式集合如表6 所示。

表6 不等式約束集合的優化結果Tab.6 Optimization results of inequality constraint set

使用貪心算法［15］得到的約束不等式集合為｛Q1，Q2，Q3，Q4，Q5｝。使用算法1 得到其中各個不等式的必要度分別為：0、1、0、1、1。此時可以得知，Q1和Q3對于不等式約束集合而言是冗余的。去除Q1，得到新的不等式約束為Q2、Q3、Q4、Q5，此時各個不等式的必要度分別為2、2、1、1，即新的不等式約束集合是緊湊的。由此可知，算法1 對于鑒別約束不等式集合的緊湊性以及指導約束集合優化具有實際的有效性。

值得注意的是，對于一個不等式約束集合而言，其中各個不等式的必要度會相互影響，去除或替換某一個不等式，其他不等式的必要度很可能也會發生變化。如表6 所示，去除Q1之后，Q3的必要度由0 變化為2，這啟示研究者在不等式集合中發現多個必要度為0 的不等式時，不可以直接將它們全部去除，而是應該每去除一個不等式重新評估一次必要度，采用回溯的方式找到去除不等式最多的方案。

表6 的案例說明，算法1 對于約束不等式可能存在的冗余情況具有很好的鑒別作用，對于不等式約束的改進和優化也具有很好的指導意義。對于應用Sun 等［15］提出的貪心算法進行差分分析相關研究遇到的問題［18］，或許可以使用算法1 解決；而對于Sasaki 等［16］改進之后的約簡算法而言，使用算法1 可以驗證其所得到結果的正確性。

由于Sasaki 等［16］的約簡算法是基于線性規劃的，并且以不等式數量的最小值作為規劃目標，其所得的不等式約束集合中每一個不等式的必要度一定不為0。假設存在一個必要度為0 的不等式，它一定會在線性規劃過程中因為“不等式數量最小化”這個優化目標而被排除，否則可以判定算法的實現過程出現了錯誤。

綜上，算法1 對于Sun 等［15］提出的貪心算法具有很好的優化效果，當出現必要度為0 的不等式時，可以根據算法1 指導不等式約束集合的優化；對于Sasaki 等［16］改進之后的約簡算法則具有很好的檢驗作用，當出現必要度為0 的不等式時，證明算法的實現過程存在錯誤，從而及時矯正。

4.1.4 算法的時間復雜度

對于擁有m個不等式、n個不可能差分模式的不等式約束，使用驗證算法緊湊性驗證，首先需要計算每一個不等式的必要度，這一過程的時間復雜度為O（mn）；之后需要檢查是否存在必要度為0 的不等式，這一過程的最壞時間復雜度為O（m）。綜上，本文驗證算法的時間復雜度為O（mn）。

4.2 約束緊湊性驗證

4.1節中說明，使用Sasaki 等［16］改進之后的約簡算法得到的約束不等式集合應當是緊湊的，若得到的不等式集合不是緊湊的，則說明算法實現過程中出現了錯誤。因此針對3.3 節中得到的約束應用算法1，得到每一個不等式約束的必要度如表7 所示。由表7 可知，3.3 節中所得的每一個不等式約束必要度都不為0，即每一個不等式都有存在的必要性，算法實現過程是正確的，所得的約束不等式集合是SPONGENT S 盒的一個緊湊約束。

表7 不等式約束的必要度Tab.7 Necessities of inequality constraints

5 結語

隨著MILP 在差分密碼分析中的地位日漸升高，尋找建立高效不等式約束的方式也變得更加重要。本文使用MILP模型針對SPONGENT 中S 盒的緊湊約束展開了分析，得到了緊湊的23 個不等式約束；同時定義了評價約束條件必要程度的參數“必要度”，并在此基礎上提出了一種約束緊湊性驗證的算法。結果表明本文提出的基于MILP 的SPONGNET 的S 盒緊湊約束分析方法可實現高效、緊湊的差分路徑自動搜索。未來的研究工作主要包括以下兩個方面：基于本文所得到的S 盒緊湊約束，針對SPONGENT 的輪函數結構建立更加高效的MILP 模型，嘗試對SPONGENT 的輪函數自動搜索差分路徑，以求得到更好的分析結果；依據本文的分析方法，對其他密碼算法進行緊湊約束分析，并利用本文的緊湊性驗證算法驗證所得到約束條件的緊湊性，建立SPONGENT 類加密算法的通用MILP 差分分析模型。