Alzette 的安全性分析*

許 崢， 李永強， 王明生

1. 中國科學院 信息工程研究所 信息安全國家重點實驗室， 北京 100093

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

1 引言

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

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

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

為了更好地過濾無效差分路徑， 密碼學家研究了差分比特之間的關系并部分解決了上述問題. 在2005年的歐密會議和美密會議上， Wang 等人利用符號差分發(fā)現(xiàn)了MD4、MD5 和SHA-1 的碰撞[22-24]. 隨后， Leurent 對于連續(xù)的異或差分比特提出了多比特限制的概念并提出了一種搜索有效差分路徑的自動化工具: 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 的自動化工具只能捕捉到連續(xù)比特之間的關系而無法捕捉非連續(xù)比特之間的關系， 因此該工具依然無法成功過濾部分無效的差分路徑. 然而， Mouha 等人的方法是自動化與手動推導相結合的方法， 無法完全自動化地過濾無效的差分路徑， 因此不適用于搜索不可能差分區(qū)分器.

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

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

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

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

2.1 符號

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

2.2 預備知識

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

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

2.3 Alzette 簡介

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

圖1 Alzette 實例AcFigure 1 Alzette instance Ac

算法1 Alzette 實例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輪的輸出如下計算:

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

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

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

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

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

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

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

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

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

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

其中， 0≤i ≤n-1.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 結論

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