基于混合整數(shù)線性規(guī)劃模型的SPONGENT S盒緊湊約束分析

石一鵬，劉 杰*，祖錦源，張 濤，張國(guó)群

（1.西北工業(yè)大學(xué) 軟件學(xué)院，西安 710129；2.上海機(jī)電工程研究所，上海 201109）

0 引言

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

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

同時(shí)，很多基于差分密碼分析的新的密碼分析方法也逐漸誕生，并廣泛應(yīng)用于多種密碼算法的安全性分析中，如Wei 等［8］對(duì)TWINE 算法展 開了不 可能差 分密碼分析；Moghaddam 等［9］對(duì)Midori、SKINNY 和CRAFT 算法展開了截?cái)嗖罘址治?；Hutahaean 等［10］對(duì)小型PRESENT 算法展開了飛去來(lái)器分析（boomerang attack）；陳少真等［11］對(duì)GOST2 算法展開了密鑰相關(guān)攻擊等。

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

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

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

本文的主要工作為：

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

2）提出了一種評(píng)價(jià)約束條件必要程度的指標(biāo)，并給出了基于該指標(biāo)的約束緊湊性驗(yàn)證算法，用于對(duì)所得到的不等式約束驗(yàn)證緊湊性。針對(duì)所得到的SPONGENT S 盒的約束應(yīng)用該算法，結(jié)果表明，所得到的約束中，每一個(gè)不等式都是不可替代的，即23 個(gè)不等式組成的約束對(duì)于SPONGENT 的S 盒是緊湊的。

1 SPONGENT

1.1 SPONGENT的版本參數(shù)

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

表1 SPONGENT版本參數(shù)Tab.1 SPONGENT version parameters

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

1.2 SONGENT的計(jì)算過(guò)程

對(duì)于輸入的消息，SPONGENT 進(jìn)行以下3 個(gè)階段的操作計(jì)算輸出：

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

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

3）壓縮階段：通過(guò)SPN 結(jié)構(gòu)的輪函數(shù)逐步計(jì)算得到輸出值。

1.3 SONGENT中的輪函數(shù)

在SPONGENT 所用的輪函數(shù)中主要進(jìn)行以下運(yùn)算：

1）state與輪常數(shù)及其反序值進(jìn)行異或運(yùn)算，根據(jù)state的位數(shù)不同，輪常數(shù)相應(yīng)的初值不同。

2）state通過(guò)S 盒完成字節(jié)代換，每一次代換的字節(jié)由4位組成，使用b表示state的位數(shù)，每一輪需要進(jìn)行b/4 個(gè)平行運(yùn)算。表2 為S 盒規(guī)格的16 進(jìn)制表示，x經(jīng)過(guò)代換變?yōu)镾(x)。

表2 S盒規(guī)格的16進(jìn)制表示Tab.2 Hexadecimal representation of S-box specification

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

本文重點(diǎn)分析S 盒的緊湊約束，對(duì)于輪函數(shù)的運(yùn)算過(guò)程不作更多討論。在得到S 盒的緊湊約束之后可以針對(duì)輪函數(shù)的結(jié)構(gòu)建立更加高效的MILP 模型，從而進(jìn)行更高效的差分密碼分析。

2 MILP在最優(yōu)差分路徑搜索中的應(yīng)用

MILP 應(yīng)用于差分路徑搜索之前，已經(jīng)在很多領(lǐng)域發(fā)揮過(guò)重要的作用，它的含義可分為“混合整數(shù)”以及“線性規(guī)劃”兩部分?！熬€性規(guī)劃”即表明這是一種使用變量約束和不等式約束對(duì)目標(biāo)函數(shù)優(yōu)化的數(shù)學(xué)方法；“混合整數(shù)”則強(qiáng)調(diào)其中的一些變量被限制為整數(shù)值，而其他變量可以是二進(jìn)制值或連續(xù)值。對(duì)于最優(yōu)差分路徑的搜索，可以使用相應(yīng)的變量約束和不等式約束描述可能的差分路徑，并將差分路徑的概率作為目標(biāo)函數(shù)，該MILP 模型的解即對(duì)應(yīng)最優(yōu)的差分路徑。

2.1 文獻(xiàn)［12］分析框架

Mouha 等［12］提出將MILP 應(yīng)用到差分路徑分析時(shí)，給出了針對(duì)SPN 結(jié)構(gòu)3 種常見操作的不等式分析。

2.1.1 異或操作不等式分析

使用Xin1、Xin2表示異或運(yùn)算的輸入差分，Xout表示相應(yīng)的輸出差分，3 個(gè)參數(shù)之間的關(guān)系可以表示為：

其中⊕表示異或運(yùn)算?？梢园l(fā)現(xiàn)，當(dāng)且僅當(dāng)Xin1與Xin2值都為0 時(shí)，Xout的值為0，否則3 個(gè)參數(shù)之間至少有兩個(gè)值不為0。使用一個(gè)虛擬變量d∈{0，1}輔助表示這種關(guān)系：

2.1.2 線性操作不等式分析

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

2.1.3 S盒操作不等式分析

對(duì)于雙射的S 盒，當(dāng)且僅當(dāng)輸入差分為0 時(shí)，輸出差分也為0。即滿足以下公式：

2.2 收緊MILP可行域的方法

利用文獻(xiàn)［12］的方法針對(duì)SPN 加密結(jié)構(gòu)建立MILP 模型之后，就可以針對(duì)不等式約束求解，最優(yōu)的差分路徑就是不等式解空間中的一個(gè)解。

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

通過(guò)添加不等式約束條件排除不可能的差分模式，就可以有效排除很多不可能差分路徑，這樣的不等式約束被稱為截?cái)嗖坏仁健?/p>

Sun 等［15］提出了兩種生成截?cái)嗖坏仁降姆椒ǎ横槍?duì)統(tǒng)計(jì)規(guī)律邏輯建模，以及差分模式最小凸集的H-表示。由于受到統(tǒng)計(jì)規(guī)律的限制，針對(duì)統(tǒng)計(jì)規(guī)律邏輯建模的方式并不適用于大多數(shù)加密結(jié)構(gòu)，因此以下主要介紹差分模式最小凸集的H-表示。

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

例如，S 盒的輸入差分為x=1001 時(shí)，可能的輸出差分為y=1001 或y=1100，輸入差分為x=1011 時(shí)，可能的輸出差分為y=1011 或y=1110。使用（x3，x2，x1，x0，y3，y2，y1，y0）表示一個(gè)差分模式，那么所有可能的差分模式組成的點(diǎn)集為｛（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-表示中含有大量有效的截?cái)嗖坏仁健?/p>

2.3 獲取緊湊約束的方法

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

為了盡可能地減少不等式數(shù)量，Sun 等［15］利用貪心算法的思想篩選不等式：依次選擇可以排除更多不可能差分模式的不等式，直到所有的不可能差分都被所選擇的截?cái)嗖坏仁脚懦?/p>

使用該貪心算法可以得到一個(gè)較優(yōu)解，但無(wú)法保證所得到的不等式數(shù)量是最少的；并且對(duì)于可以排除相等數(shù)量不可能差分模式的截?cái)嗖坏仁?，并沒有明確給出選擇的優(yōu)先級(jí)?；谶@種情況，Sasaki 等［16］提出了一種新的約簡(jiǎn)算法，應(yīng)用MILP 選擇最優(yōu)不等式組合，它的基本步驟為：首先計(jì)算每個(gè)不可能的差分模式可以被哪些不等式排除，得到一個(gè)關(guān)于不可能差分模式和截?cái)嗖坏仁街g的指導(dǎo)二維表，如表3 所示，單元值為1 表示它對(duì)應(yīng)的不可能差分模式可以被對(duì)應(yīng)的截?cái)嗖坏仁脚懦?；然后設(shè)定約束條件為每一個(gè)不可能差分模式至少被一個(gè)不等式所排除，同時(shí)設(shè)定每一個(gè)不等式最多可以選擇一次；最后設(shè)定目標(biāo)函數(shù)為最少的不等式數(shù)量，進(jìn)行MILP 求解。

表3 指導(dǎo)二維表樣例Tab.3 Example of 2D guidance table

3 SPONGENT S盒的約束分析

為了尋找S 盒的緊湊約束，本章使用Sasaki 等［16］提出的約簡(jiǎn)算法展開具體分析，主要步驟包括：計(jì)算所有可能的差分模式、求解截?cái)嗖坏仁胶涂s減不等式數(shù)量。

3.1 計(jì)算所有可能的差分模式

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

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

例如，輸入差分x=0001 時(shí)，可能的差分輸出有：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 求解截?cái)嗖坏仁?/h3>

根據(jù)表4 可以得到97 個(gè)可能的差分模式，對(duì)應(yīng)97 個(gè)點(diǎn)，使用SageMath 中的函數(shù)inequality_generator（）計(jì)算得到它的凸集的H-表示，共含有287 個(gè)不等式：

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

3.3 縮減不等式數(shù)量

計(jì)算所有不可能的差分模式，共有256 -97=159 個(gè)，并對(duì)所有的不可能差分模式從0 開始編號(hào)，最后一個(gè)不可能差分模式編號(hào)為158。

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

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

對(duì)全部不可能差分模式進(jìn)行以上步驟，可以得到關(guān)于Ij的159 個(gè)不等式約束，求解得

對(duì)應(yīng)值為1 的不等式為：

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

4 緊湊性驗(yàn)證

4.1 緊湊性驗(yàn)證算法

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

在S 盒所有可能差分模式最小凸集的H-表示中，每一個(gè)截?cái)嗖坏仁娇梢耘懦牟豢赡懿罘帜Ｊ綍?huì)有重合的部分，如表3 中，不等式1 和3 都能排除不可能差分模式1，不等式1、2和N都能排除不可能差分模式2。這種重合的情況在最終所求得的不等式約束集合中同樣存在，而這恰恰是發(fā)現(xiàn)不等式約束集合可能存在冗余的一個(gè)重要突破口。

為了更好地表示這種冗余的情況，本文使用一個(gè)具體的案例說(shuō)明。如表5 所示，使用Qi表示待選擇的截?cái)嗖坏仁?，使用Ij表示需要被排除的不可能差分模式，當(dāng)單元格值為1時(shí)，表示它對(duì)應(yīng)的不可能差分模式可以被對(duì)應(yīng)的截?cái)嗖坏仁脚懦? 中Q1到Q8所能排除的不等式數(shù)量為降序排列。

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

針對(duì)表5 中的數(shù)據(jù)應(yīng)用貪心算法［15］篩選不等式，依次選取可以排除不可能差分模式最多的截?cái)嗖坏仁剑钡剿械牟豢赡懿罘帜Ｊ蕉急慌懦?，得到的篩選結(jié)果為Q1、Q2、Q3、Q4、Q5。不難發(fā)現(xiàn)，Q1排除的不可能差分模式都可以被Q2、Q3、Q4、Q5組成的其他不等式組排除，不等式Q1對(duì)整個(gè)不等式約束集合就是冗余的。刪去Q1對(duì)于不等式約束集合排除不可能差分模式的能力沒有任何影響，但是卻可以減輕運(yùn)算的負(fù)擔(dān)，提高差分路徑搜索的效率。

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

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

4.1.2 緊湊性驗(yàn)證算法

為了驗(yàn)證不等式約束集合的緊湊性，本文首先定義了一個(gè)評(píng)價(jià)約束條件必要程度的指標(biāo)“必要度”，使用參數(shù)Necessity∈{0，1，…}表示，定義如下：

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

當(dāng)一個(gè)不等式的必要度為0 時(shí)，表示該不等式對(duì)于約束組合是非必要存在的。此時(shí)，原不等式約束集合就是不緊湊的，一個(gè)緊湊的不等式約束集合至少不能包含該不等式。

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

算法1 驗(yàn)證約束條件集合緊湊性的算法。

4.1.3 算法的正確性及應(yīng)用

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

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

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

表6 不等式約束集合的優(yōu)化結(jié)果Tab.6 Optimization results of inequality constraint set

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

值得注意的是，對(duì)于一個(gè)不等式約束集合而言，其中各個(gè)不等式的必要度會(huì)相互影響，去除或替換某一個(gè)不等式，其他不等式的必要度很可能也會(huì)發(fā)生變化。如表6 所示，去除Q1之后，Q3的必要度由0 變化為2，這啟示研究者在不等式集合中發(fā)現(xiàn)多個(gè)必要度為0 的不等式時(shí)，不可以直接將它們?nèi)咳コ?，而是?yīng)該每去除一個(gè)不等式重新評(píng)估一次必要度，采用回溯的方式找到去除不等式最多的方案。

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

由于Sasaki 等［16］的約簡(jiǎn)算法是基于線性規(guī)劃的，并且以不等式數(shù)量的最小值作為規(guī)劃目標(biāo)，其所得的不等式約束集合中每一個(gè)不等式的必要度一定不為0。假設(shè)存在一個(gè)必要度為0 的不等式，它一定會(huì)在線性規(guī)劃過(guò)程中因?yàn)椤安坏仁綌?shù)量最小化”這個(gè)優(yōu)化目標(biāo)而被排除，否則可以判定算法的實(shí)現(xiàn)過(guò)程出現(xiàn)了錯(cuò)誤。

綜上，算法1 對(duì)于Sun 等［15］提出的貪心算法具有很好的優(yōu)化效果，當(dāng)出現(xiàn)必要度為0 的不等式時(shí)，可以根據(jù)算法1 指導(dǎo)不等式約束集合的優(yōu)化；對(duì)于Sasaki 等［16］改進(jìn)之后的約簡(jiǎn)算法則具有很好的檢驗(yàn)作用，當(dāng)出現(xiàn)必要度為0 的不等式時(shí)，證明算法的實(shí)現(xiàn)過(guò)程存在錯(cuò)誤，從而及時(shí)矯正。

4.1.4 算法的時(shí)間復(fù)雜度

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

4.2 約束緊湊性驗(yàn)證

4.1節(jié)中說(shuō)明，使用Sasaki 等［16］改進(jìn)之后的約簡(jiǎn)算法得到的約束不等式集合應(yīng)當(dāng)是緊湊的，若得到的不等式集合不是緊湊的，則說(shuō)明算法實(shí)現(xiàn)過(guò)程中出現(xiàn)了錯(cuò)誤。因此針對(duì)3.3 節(jié)中得到的約束應(yīng)用算法1，得到每一個(gè)不等式約束的必要度如表7 所示。由表7 可知，3.3 節(jié)中所得的每一個(gè)不等式約束必要度都不為0，即每一個(gè)不等式都有存在的必要性，算法實(shí)現(xiàn)過(guò)程是正確的，所得的約束不等式集合是SPONGENT S 盒的一個(gè)緊湊約束。

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

5 結(jié)語(yǔ)

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