許 崢， 李永強(qiáng)， 王明生

1. 中國科學(xué)院 信息工程研究所 信息安全國家重點(diǎn)實(shí)驗(yàn)室， 北京 100093

2. 中國科學(xué)院大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院， 北京 100049

1 引言

認(rèn)證加密算法(authenticated-encryption， AE) 是指能同時(shí)實(shí)現(xiàn)數(shù)據(jù)加密和真實(shí)性認(rèn)證功能的算法，是密碼學(xué)家在研究加密算法和認(rèn)證算法的基礎(chǔ)之上， 根據(jù)現(xiàn)實(shí)應(yīng)用需求提出的對稱密碼算法. 隨著物聯(lián)網(wǎng)的發(fā)展， 密碼算法越來越多地被應(yīng)用在資源受限的環(huán)境中. 由于現(xiàn)有的認(rèn)證加密算法以及Hash 函數(shù)不適用于資源受限的環(huán)境中，美國國家標(biāo)準(zhǔn)與技術(shù)研究所(NIST)啟動(dòng)了一項(xiàng)進(jìn)程，以征集、評估并標(biāo)準(zhǔn)化適用于資源受限環(huán)境中的帶關(guān)聯(lián)數(shù)據(jù)的認(rèn)證加密(AEAD) 算法以及Hash 函數(shù)[1]. 2019 年4 月18 日， NIST共收到57 個(gè)算法， 其中的56 個(gè)被接收為第一輪候選算法. 經(jīng)過公開反饋以及內(nèi)部評定， NIST 于2019 年8 月30 日公布了32 個(gè)第二輪候選算法. 經(jīng)過更加嚴(yán)格的安全性評估， 2021 年3 月29 日， NIST 公布了10 個(gè)決賽候選算法: ASCON、Elephant、GIFT-COFB、Grain-128AEAD、ISAP、PHOTON-Beetle、Romulus、SPARKLE、TinyJambu 以及Xoodyak. 在這10 個(gè)決賽候選算法之中， SPARKLE 算法由于使用了新的64 比特S 盒(Alzette) 而備受關(guān)注.

Alzette[2]是由Beierle 等人在2020 年美密會上提出的一種ARX (模加、循環(huán)移位、異或) 結(jié)構(gòu)的64 比特S 盒. ARX 結(jié)構(gòu)的安全性是通過分析其抗各種攻擊的魯棒性來評估的. 對于ARX 結(jié)構(gòu)最成功的攻擊之一是差分類攻擊(差分攻擊[3]和不可能差分攻擊[4，5]). 由于Alzette 是SPARKLE 算法唯一的非線性來源， 而模加又是Alzette 唯一的非線性來源， 因此評估模加的差分性質(zhì)對評估Alzette 以及SPARKLE 抗差分類分析的安全性是十分關(guān)鍵的.

模加的差分性質(zhì)已經(jīng)被研究了幾十年. 在2001 年的FSE 會議上， Lipmaa 和Moriai 提出了一種計(jì)算具有兩個(gè)可變輸入的模加的差分概率的對數(shù)時(shí)間算法[6]. 在2010 年的SAC 會議上， Mouha 等人引入了S 函數(shù)的概念并利用S 函數(shù)來評估具有任意數(shù)量輸入分支模加的差分概率[7]. 在2020 年的亞密會議上， Azimi 等人提出了一種針對具有一個(gè)常量輸入的模加的比特向量差分模型[8]. 為了更好地評估分組密碼抗差分分析的安全性， Lai 等人在1991 年的歐密會議上提出了Markov 密碼的概念[9]. 在Markov 假設(shè)下， 一條差分路徑的概率可以通過將每一輪的差分傳播的概率相乘得到. 事實(shí)上， Markov 假設(shè)被用于幾乎所有對分組密碼的差分攻擊以及不可能差分攻擊中. 在近二十年中， 利用自動(dòng)化工具搜索差分路徑以及不可能差分區(qū)分器成為了一種新的趨勢. 這些自動(dòng)化工具主要分為三類: 利用Matsui 算法類的分支定界搜索算法[10-13]、利用混合整數(shù)線性規(guī)劃(MILP) 模型[14，15]以及利用SAT/SMT 求解器[16-21]. 這些方法都是基于Markov 假設(shè)的. 在Markov 假設(shè)下， ARX 結(jié)構(gòu)的差分路徑的概率等于每一輪中的每個(gè)模加的差分概率的乘積. 然而， 由于Alzette 中沒有任何的密鑰注入， 利用基于Markov 假設(shè)的自動(dòng)化搜索方法來搜索Alzette 的差分路徑以及不可能差分區(qū)分器， 可能會將無效的差分路徑識別為有效并遺漏一些有效的不可能差分區(qū)分器， 從而導(dǎo)致對Alzette 抗差分類分析的安全性評估不夠準(zhǔn)確. 因此， 提出一種能夠更好地過濾無效的差分路徑的方法是十分重要的.

為了更好地過濾無效差分路徑， 密碼學(xué)家研究了差分比特之間的關(guān)系并部分解決了上述問題. 在2005年的歐密會議和美密會議上， Wang 等人利用符號差分發(fā)現(xiàn)了MD4、MD5 和SHA-1 的碰撞[22-24]. 隨后， Leurent 對于連續(xù)的異或差分比特提出了多比特限制的概念并提出了一種搜索有效差分路徑的自動(dòng)化工具: ARX Toolkit. 利用該工具， Leurent[25]發(fā)現(xiàn)了Yu 等人[26]只利用符號差分找到的一條Skein 算法的差分路徑是無效的. 在2013 年， Mouha 等人[20]利用Lipmaa-Moriai 限制條件以及符號差分搜索3輪Salsa20 的最優(yōu)差分路徑. 他們發(fā)現(xiàn)了一條ARX Toolkit 無法過濾的差分路徑， 證明Leurent 的自動(dòng)化工具只能捕捉到連續(xù)比特之間的關(guān)系而無法捕捉非連續(xù)比特之間的關(guān)系， 因此該工具依然無法成功過濾部分無效的差分路徑. 然而， Mouha 等人的方法是自動(dòng)化與手動(dòng)推導(dǎo)相結(jié)合的方法， 無法完全自動(dòng)化地過濾無效的差分路徑， 因此不適用于搜索不可能差分區(qū)分器.

本文研究了Alzette 抗差分類分析的安全性. 對于模加操作上的有效異或差分， 通過利用符號差分的概念， 本文給出了符號差分比特之間關(guān)系的比特向量表示. 通過將Lipmaa-Moriai 限制條件以及符號差分比特約束條件轉(zhuǎn)化為可滿足性模理論(satisfiability modulo theories， SMT) 問題， 本文提出了一種基于SAT/SMT 求解器的ARX 結(jié)構(gòu)不可能差分區(qū)分器自動(dòng)化搜索工具. 該自動(dòng)化工具是首個(gè)利用Lipmaa-Moriai 限制條件以及符號差分搜索ARX 結(jié)構(gòu)不可能差分區(qū)分器的自動(dòng)化工具. 通過利用符號差分， 該自動(dòng)化工具可以捕捉連續(xù)比特以及非連續(xù)比特之間的關(guān)系; 通過利用Lipmaa-Moriai 限制條件，該自動(dòng)化工具可以有效地過濾僅滿足符號差分比特約束條件而不滿足Lipmaa-Moriai 限制條件的無效差分路徑. 因此， 利用該自動(dòng)化工具可以發(fā)現(xiàn)被傳統(tǒng)搜索方法忽略的有效的不可能差分區(qū)分器. 將本文提出的自動(dòng)化工具用于搜索具有常數(shù)c= 0xb7e15162 的Alzette (即A0xb7e15162) 的不可能差分區(qū)分器: 在輸入差分漢明重量為1、輸出差分漢明重量為1 的條件下， 我們發(fā)現(xiàn)了4096 個(gè)不可能差分區(qū)分器; 在輸入差分漢明重量為2、輸出差分漢明重量為1 的條件下， 我們發(fā)現(xiàn)了128 993 個(gè)不可能差分區(qū)分器. 然而，在輸入差分漢明重量為2、輸出差分漢明重量為1 的條件下， 利用傳統(tǒng)方法搜索Alzette 的不可能差分區(qū)分器， 我們發(fā)現(xiàn)了128 767 個(gè)不可能差分區(qū)分器， 證明本文提出的自動(dòng)化工具能夠更好地過濾無效差分路徑. 因此， 利用本文提出的方法， 密碼分析者可以更好地評估ARX 結(jié)構(gòu)抗不可能差分分析的安全性， 從而給出ARX 結(jié)構(gòu)更加精確的安全性評估結(jié)果. 同時(shí)， 由于Alzette 是一個(gè)SPECK 類結(jié)構(gòu)， 我們分別利用本文提出的自動(dòng)化搜索工具以及傳統(tǒng)方法搜索4 輪無密鑰注入SPECK64[27]的不可能差分區(qū)分器. 在輸入差分漢明重量為2、輸出差分漢明重量為1 的條件下， 我們分別發(fā)現(xiàn)了128 976 個(gè)以及128 018 個(gè)不可能差分區(qū)分器.A0xb7e15162與4 輪無密鑰注入SPECK64 的不可能差分區(qū)分器的數(shù)量如表1 所示. 據(jù)我們所知， 這是首次利用不可能差分性質(zhì)評估Alzette 的安全性.

表1 一步A0xb7e15162 與4 輪無密鑰注入SPECK64 不可能差分區(qū)分器的數(shù)量Table 1 Numbers of impossible differential characteristics for A0xb7e15162 and 4-round no-key SPECK64

本文結(jié)構(gòu)安排如下: 第2 節(jié)簡要介紹本文中所用到的符號、Lipmaa-Moriai 限制條件、符號差分、Alzette 的結(jié)構(gòu)以及SPECK 算法等預(yù)備知識; 第3 節(jié)介紹如何利用Lipmaa-Moriai 限制條件以及符號差分比特約束條件， 構(gòu)建基于SAT/SMT 求解器的ARX 結(jié)構(gòu)不可能差分區(qū)分器自動(dòng)化搜索工具; 第4 節(jié)將新的自動(dòng)化工具以及傳統(tǒng)的搜索方法應(yīng)用于搜索Alzette 和4 輪SPECK64 的不可能差分區(qū)分器;第5 節(jié)總結(jié)本文工作.

2 符號、預(yù)備知識及算法簡介

2.1 符號

本文中使用的符號如下所示:

2.2 預(yù)備知識

其中mask(n-1) 表示0‖1n-1. 在下文中， 稱公式(1) 和公式(2) 為Lipmaa-Moriai 限制條件.

定義3 (符號差分[22-24]) 符號差分Δ±x可以將異或差分分為三種情況:

2.3 Alzette 簡介

在2020 年美密會議上， Beierle 等人[2]提出了一種名為Alzette 的64 比特基于ARX 的S 盒. 它是一種具有兩個(gè)分支的4 輪SPECK 類結(jié)構(gòu)， 并且由一個(gè)任意的常數(shù)c ∈F322來參數(shù)化. Alzette 的描述如算法1、圖1 所示.

圖1 Alzette 實(shí)例AcFigure 1 Alzette instance Ac

算法1 Alzette 實(shí)例Ac Input: (x，y) ∈F32 2 ×F322 Output: (u，v) ∈F322 ×F322 1 x ←x ?(y ?31);2 y ←y ⊕(x ?24);3 x ←x ⊕c;4 x ←x ?(y ?17);5 y ←y ⊕(x ?17);6 x ←x ⊕c;7 x ←x ?(y ?0);8 y ←y ⊕(x ?31);9 x ←x ⊕c;10 x ←x ?(y ?24);11 v ←y ⊕(x ?16);12 u ←x ⊕c;13 return (u，v);

2.4 SPECK 簡介

美國國家安全局(NSA) 于2013 年發(fā)布了SPECK 族輕量分組密碼算法[27]. 根據(jù)算法的分組長度(32、48、64、96 以及128 比特)，共包括5 類分組密碼算法: SPECK32、SPECK48、SPECK64、SPECK96以及SPECK128. 通常， SPECK2n/mn表示具有2n比特分組長度以及mn比特密鑰長度的SPECK 算法， 其中n ∈{16，24，32，48，64}、m ∈{2，3，4}且依賴于n的取值. 令(Li-1，Ri-1) 表示第i輪的輸入，則第i輪的輸出如下計(jì)算:

其中Ki表示輪密鑰. 當(dāng)分組長度是32 比特時(shí)， (α，β) = (7，2)， 否則(α，β) = (8，3). SPECK 的輪函數(shù)如圖2 所示.

圖2 SPECK 輪函數(shù)Figure 2 Round function of SPECK

3 基于SAT/SMT 求解器的ARX 結(jié)構(gòu)不可能差分區(qū)分器自動(dòng)化搜索工具

在本節(jié)中， 我們提出了一種新的基于SAT/SMT 求解器的ARX 結(jié)構(gòu)不可能差分區(qū)分器自動(dòng)化搜索工具. 由于該自動(dòng)化工具不僅包含了傳統(tǒng)搜索方法所包含的約束條件(Lipmaa-Moriai 限制條件)， 還包含了傳統(tǒng)搜索方法未包含的約束條件(符號差分比特約束條件)， 因此， 該自動(dòng)化工具能夠更好地過濾無效的差分路徑， 并找到被傳統(tǒng)搜索方法所遺漏的有效的不可能差分區(qū)分器。

3.1 構(gòu)建基于SAT/SMT 求解器的ARX 結(jié)構(gòu)不可能差分區(qū)分器自動(dòng)化搜索工具

在文獻(xiàn)[20] 中， Mouha 等人利用SAT/SMT 求解器自動(dòng)化搜索3 輪Salsa20 的最優(yōu)差分路徑. 盡管他們發(fā)現(xiàn)了一些差分路徑是無效的， 但他們的搜索模型中僅包含了Lipmaa-Moriai 限制條件以及異或差分的傳播， 這意味著他們的模型無法自動(dòng)地過濾那些滿足Lipmaa-Moriai 限制條件以及異或差分傳播的無效差分路徑.

為了自動(dòng)地過濾這些特殊的差分路徑， 本文提出的自動(dòng)化搜索工具不僅包含了傳統(tǒng)搜索方法所包含的約束條件， 還包含了符號差分的傳播以在異或差分傳播中添加值傳播的信息.

本文將搜索不可能差分區(qū)分器的問題轉(zhuǎn)化為布爾可滿足性問題(Boolean satisfiability problem，SAT)， 然后利用SAT 求解器進(jìn)行求解. 然而， ARX 結(jié)構(gòu)所包含的都是n比特向量上的操作， 但是SAT問題僅能包含布爾變量以及與(AND)、或(OR)、非(NOT) 操作. 由于SMT 問題支持比特向量變量以及比特向量操作， 且SMT 問題是SAT 問題的推廣， 因此本文使用SMT 問題來代替SAT 問題. 一旦一個(gè)SMT 問題被建立， SMT 求解器可將SMT 問題轉(zhuǎn)化為SAT 問題， 并利用SAT 求解器進(jìn)行求解. STP求解器[28]是一個(gè)典型的SMT 求解器， 我們利用STP 求解器求解本文中所有的SMT 問題.

對于一個(gè)變量分支與一個(gè)常數(shù)的異或操作的符號差分傳播， 由于輸出符號差分的取值依賴于常數(shù)， 本文用定理1 處理這種情況.

定理1 令x，x′，y，y′，z，z′∈Fn2. 對于z=x ⊕C以及z′=x′⊕C， 假設(shè)C是常數(shù)， 則有Δz=Δx以及如下符號差分比特之間的關(guān)系:

其中， 0≤i ≤n-1.

我們可以用公式(4) 來描述一個(gè)變量分支與一個(gè)常數(shù)的異或操作的符號差分傳播.

使用上述方法， 可以構(gòu)建一個(gè)描述Lipmaa-Moriai 限制條件、異或差分傳播以及符號差分傳播的SAT/SMT 求解模型. 如果對ARX 結(jié)構(gòu)的輸入差分(InD) 以及輸出差分(OutD) 進(jìn)行賦值， 則可以得到指定輸入差分到指定輸出差分是否是一個(gè)可能的映射， 即: InD ?OutD 或者InD?OutD. 通過在本文提出的搜索模型中添加以下兩條命令， 即可完成該映射的可能性判斷:

當(dāng)STP 返回Valid 時(shí)， 則InD ?OutD， 即找到一個(gè)不可能差分區(qū)分器; 當(dāng)STP 返回一條差分路徑時(shí)， 則InD?OutD， 且該差分路徑是有效的.

至此， 我們可以通過以上完整的架構(gòu)來構(gòu)建用于搜索ARX 結(jié)構(gòu)不可能差分區(qū)分器的自動(dòng)化工具. 該自動(dòng)化工具可以有效地過濾不符合Lipmaa-Moriai 限制條件以及符號差分比特約束條件的無效差分路徑.

4 自動(dòng)化搜索Alzette 和無密鑰注入的SPECK64 不可能差分區(qū)分器

在本節(jié)中， 我們將第3 節(jié)中提出的自動(dòng)化工具用于搜索Alzette 和無密鑰注入的SPECK64 不可能差分區(qū)分器， 并找到了被傳統(tǒng)搜索方法忽略的不可能差分區(qū)分器.

在文獻(xiàn)[2] 中， Alzette 的設(shè)計(jì)者宣稱， Alzette 的設(shè)計(jì)安全性指標(biāo)之一是兩步Alzette (即8 輪) 的差分界與線性界要強(qiáng)于8 輪SPECK64. 在Alzette 以及SPARKLE 的設(shè)計(jì)文檔中， 設(shè)計(jì)者僅通過搜索不同步數(shù)Alzette 的最優(yōu)(或次優(yōu)) 差分路徑來評估其抗差分分析的安全性. 除了上述設(shè)計(jì)文檔外， 唯一對Alzette 的安全性分析結(jié)果發(fā)表在2021 年歐密會議上[29]. 然而， 文獻(xiàn)[29] 中的安全性分析是關(guān)于差分-線性密碼分析的. 到目前為止， 還沒有任何對Alzette 不可能差分區(qū)分器的公開分析結(jié)果. 由于Alzette 是一個(gè)S 盒， 因此最直接的分析其抗差分類分析安全性的方法是計(jì)算它的差分分布表(difference distribution table， DDT). 然而， 由于Alzette 是操作在64 比特上的S 盒， 計(jì)算其DDT 是無法實(shí)現(xiàn)的. 因此， 需通過間接的方法評估其差分的分布情況. 對于任意操作在n比特上的S 盒， 對于任意給定的輸入差分， 有如下性質(zhì):

其中OutDi表示OutD =i. 因此， 若一個(gè)S 盒的DDT 中為0 的項(xiàng)越少， 該S 盒的差分呈現(xiàn)較為均勻分布的概率越高， 則該S 盒能夠較好抗差分類分析的概率越高. 由此可見， 搜索Alzette 的不可能差分區(qū)分器對評估Alzette 抗差分類分析的安全性是十分有意義的.

由于Alzette 沒有密鑰注入， 為了更好地對比Alzette 與SPECK64 的安全性， 本文搜索無密鑰注入的SPECK64 不可能差分區(qū)分器. 其次， 由于每一步Alzette 使用不同的常數(shù)進(jìn)行實(shí)例化， 而無論幾輪的無密鑰注入SPECK64 都相當(dāng)于使用全0 密鑰進(jìn)行實(shí)例化， 因此搜索一步Alzette 與4 輪SPECK64 的不可能差分區(qū)分器能夠更好地對比Alzette 與SPECK64 的安全性.

4.1 自動(dòng)化搜索Alzette 不可能差分區(qū)分器

在搜索一步Alzette 不可能差分區(qū)分器時(shí)， 本文選擇常數(shù)c= 0xb7e15162 (SPARKLE 使用的8 個(gè)常數(shù)之一) 來實(shí)例化Alzette.

(1) 在wt(InD) = 1 且wt(OutD) = 1 的限制條件下， 利用本文提出的自動(dòng)化工具， 我們找到了4096個(gè)不可能差分區(qū)分器; 利用傳統(tǒng)搜索方法， 我們同樣找到了4096 個(gè)不可能差分區(qū)分器.

(2) 在wt(InD) = 2 且wt(OutD) = 1 的限制條件下， 利用本文提出的自動(dòng)化工具， 我們找到了128 993 個(gè)不可能差分區(qū)分器; 利用傳統(tǒng)搜索方法， 我們僅找到128 767 個(gè)不可能差分區(qū)分器.

上述結(jié)果說明， 利用僅包含Lipmaa-Moriai 限制條件以及異或差分傳播的傳統(tǒng)方法搜索ARX 結(jié)構(gòu)不可能差分區(qū)分器， 可能會遺漏一些有效的不可能差分區(qū)分器; 然而， 利用本文提出的自動(dòng)化工具， 我們可以搜索到這些區(qū)分器.

4.2 自動(dòng)化搜索無密鑰注入SPECK64 不可能差分區(qū)分器

為了更好地對比Alzette 與SPECK64 的安全性， 本文搜索4 輪無密鑰注入SPECK64 的不可能差分區(qū)分器.

在wt(InD)=2 且wt(OutD)=1 的限制條件下， 利用本文提出的自動(dòng)化工具， 我們找到了128 976 個(gè)不可能差分區(qū)分器; 利用傳統(tǒng)搜索方法， 我們僅找到128 018 個(gè)不可能差分區(qū)分器.

我們發(fā)現(xiàn)， 無論利用本文提出的自動(dòng)化工具還是利用傳統(tǒng)方法， 一步Alzette 不可能差分區(qū)分器的數(shù)量都多于4 輪無密鑰注入SPECK64 不可能差分區(qū)分器的數(shù)量. 因此， 如果從搜索不可能差分區(qū)分器的角度來評估ARX 結(jié)構(gòu)的差分分布， Alzette 抗差分分析的安全性可能弱于SPECK64， 這與Alzette 設(shè)計(jì)者的結(jié)論相反. 盡管Alzette 的設(shè)計(jì)者利用兩步Alzette 最優(yōu)差分路徑的概率小于8 輪SPECK64 來證明Alzette 抗差分分析的安全性強(qiáng)于SPECK64， 但是由于Alzette 是一個(gè)S 盒， 因此， 只能通過差分的概率而不是差分路徑的概率來評估其安全性. 然而， Alzette 與SPECK64 的差分概率之間的大小關(guān)系無法由最優(yōu)差分路徑概率之間的大小關(guān)系導(dǎo)出. 因此， Alzette 設(shè)計(jì)團(tuán)隊(duì)的安全性評估是不夠全面的. 據(jù)我們所知， 這是首次利用不可能差分性質(zhì)評估Alzette 的安全性.

5 結(jié)論

本文研究了Alzette 抗差分類分析的安全性. 對于模加操作上的有效異或差分， 通過利用符號差分的概念， 本文給出了符號差分比特之間關(guān)系的比特向量表示. 通過將Lipmaa-Moriai 限制條件以及符號差分比特約束條件轉(zhuǎn)化為SMT 問題， 本文提出了一種基于SAT/SMT 求解器的ARX 結(jié)構(gòu)不可能差分區(qū)分器自動(dòng)化搜索工具. 該自動(dòng)化工具是首個(gè)利用Lipmaa-Moriai 限制條件以及符號差分搜索ARX 結(jié)構(gòu)不可能差分區(qū)分器的自動(dòng)化工具. 利用該工具可以發(fā)現(xiàn)被傳統(tǒng)搜索方法忽略的有效的不可能差分區(qū)分器. 利用上述自動(dòng)化工具以及傳統(tǒng)方法搜索Alzette 的不可能差分區(qū)分器， 我們發(fā)現(xiàn)， 該自動(dòng)化工具能夠發(fā)現(xiàn)更多的不可能差分區(qū)分器， 證明該自動(dòng)化工具能夠更好地過濾無效差分路徑. 此外， 將該自動(dòng)化搜索工具用于搜索4 輪無密鑰注入SPECK64 不可能差分區(qū)分器， 我們發(fā)現(xiàn)4 輪無密鑰注入SPECK64 不可能差分區(qū)分器的數(shù)量少于Alzette 不可能差分區(qū)分器的數(shù)量， 說明Alzette設(shè)計(jì)團(tuán)隊(duì)的安全性評估是不夠全面的. 據(jù)我們所知， 這是首次利用不可能差分性質(zhì)評估Alzette 的安全性. 我們希望本文提出的方法有助于評估ARX 結(jié)構(gòu)抗差分類分析的安全性并有助于ARX 密碼的設(shè)計(jì).