基于密鑰循環的通用可復合符號分析?

付浩肖建新

基于密鑰循環的通用可復合符號分析?

付浩肖建新

（長沙師范學院教育技術中心長沙410100）

針對目前越來越復雜的安全協議，在建立計算可靠的安全協議符號分析方法的深入研究，提出了一種解決該問題的新方法，即通用可復合符號分析方法。通過擴展現有通用可復合符號分析方法，使其可以分析基于雙線性對的密鑰交換協議，并在保證計算可靠性的同時，還可以保證可復合安全性。將符號模型中的密碼學抽象操作與UC模型中的理想功能進行了結合，并且證明了如果協議在符號模型下滿足了相應的安全性質，則在UC模型下一定安全的實現了相應的理想功能。

安全協議；密鑰循環；通用可復合；雙線性對

Class NumberTP391

1引言

進入21世紀以來，隨著互聯網網絡信息技術的飛速發展，信息網絡的廣泛應用已成為人們工作和生活不可或缺的一部分。計算機網絡給人們生活帶來巨大便利，同時也對網絡上信息的安全保護提出了更高的要求。如果計算機網絡的安全問題不能切實有效地解決，那么它的應用和發展必定會受到一定的影響。

安全協議是解決網絡安全問題最有效的手段之一。構建安全網絡環境一般采用密碼技術的安全協議，安全協議的目標既是為了實現信息的加密傳輸，也是為解決網絡中的安全問題，它的正確性和安全性對于網絡安全極其重要。符號方法用形式化語言和符號推理對協議進行分析和驗證，更容易實現自動化分析。但是由于對密碼學原語和攻擊者能力的理想建模，使得這類分析方法的肯定性結論往往并不直接具有現實意義，被認為沒有真正建立起密碼學的可靠性。

為了簡化安全協議的設計和分析，傳統的安全協議任務通常假設某個確定協議運行在一個獨立的計算環境中，即孤立（stand-alone）模型。由Ca?netti提出的通用可復合（Universally Composable，UC）模型［1］可以保證協議的通用可復合安全，即在UC模型下證明安全的協議，在與其它協議并發運行的情況下，或者作為一個系統的組件時，仍能保證協議的安全性。UC模型利用“子程序替換（Sub?routine substitution）”技術將嵌套的順序算法轉化為并行運行的分布式安全協議，實現了安全協議的UC安全可復合操作。通用可復合安全的協議是協議模塊化設計和實現的基礎。

通用可復合符號分析（Universally Composable Symbolic Analysis，UCSA）方法［2］將符號模型與UC模型結合起來，給出了證明一類協議密碼學可靠性的一般方法。將符號模型中密碼學抽象操作和安全屬性與UC模型中的理想功能進行了結合，證明了如果符號模型下協議滿足了相應的安全性質，則UC模型下的現實協議一定UC安全的實現了相應的理想功能。結合UC模型對協議進行分析，一方面可以只分析單個協議運行實例，另一方面可以根據不同的理想功能對不同的密碼學操作進行抽象。然而，UCSA方法在能夠分析的協議類型上有一定限制，目前僅適用于基于公鑰加密和簽名的雙方密鑰交換協議。為此，本文通過擴展該方法，使得其可以適用于多參與者基于公鑰加密、簽名和雙線性對的認證密鑰交換協議，并證明擴展后的方法依然具有密碼學可靠性。

2通用可復合安全模型

通用可復合（UniversalComposable，UC）安全模型［3］是Canetti在2001年提出的基于模擬的通用安全協議設計與分析框架，根據真實協議和理想協議模擬不可區分來定義協議安全性。

2.1協議建模

在UC模型中，協議被建模成一個由交互式圖靈機和控制函數組成的系統，即交互式圖靈機系統（ITMs）。

理想功能與理想協議，理想功能是UC模型中非常重要的概念，用來描述安全協議所應具有的功能，或者規范。

定義1實現理想功能

給定協議π和理想功能，如果稱協議π安全地實現了理想功能，則對于任意概率多項式時間內的攻擊者A，都存在一個理想攻擊者S，使得對于任意環境Z

也就是說，執行協議π與使用理想功能是一樣安全的。任何在現實模型下協議執行發生的攻擊行為，在理想模型下也是可行的。

2.2通用可復合安全

除了現實模型和理想模型外，Canetti引入了混合模型（hybrid model），并描述了混合模型中的協議，即混合協議。

定理1通用可復合安全定理（UC安全定理）

給定-混合協議π，如果稱協議r安全地實現了理想功能，則對于任意概率多項式時間內的混合協議攻擊者H，都存在一個理想攻擊者S，使得對于任意環境Z

根據定理1，可以直接得出如下推論：

如果-混合協議π安全實現了理想功能，而且協議r安全地實現了理想功能，則復合協議πr一定安全地實現了理想功能。

根據UC理論，只需要分析協議在單個實例運行情況下的安全性，就能夠將其推廣到無限多實例并發的情形。因為UC理論中的環境Z代表了任意多協議并發執行的情況，所以不需要單獨考慮協議并發運行的情況，簡化了復雜的分析過程。其次，可以模塊化的構建安全協議。可以將相關的密碼學原語或者簡單子協議通過理想功能表示。在構建復雜協議的時候就能夠采用混合模型下的協議，并且調用上述理想功能。這樣可以簡化復雜協議的描述與分析。當將所采用的理想功能全部替換成相應UC安全的協議時，就能夠直接得到在現實模型下具有安全性的協議。

3簡單協議

由于UC模型中協議參與者是由任意的交互式圖靈機所表示的，而符號模型中所支持的操作種類有限，例如加密、解密、消息對等，所以并不是所有的協議都能在符號模型中表示出來。在UC模型中限制一類只使用特定動作的安全協議，即簡單協議。簡單協議的結構與符號模型中所支持的協議結構類似，因此可以將特定的簡單協議分別給出計算語義和符號語義，以便于對應進行分析。

3.1語法

定義2簡單協議

簡單協議Π是一個n元組程序Π=(Π1，Π2，…，Πn)，分別描述協議不同角色的行為。其中每個程序Πi的語法定義如下所示，其中v，v1，v2，v3，v4表示變量，vc，vc1，vc2，vc3，vc4表示常量。

3.2計算語義

定義3協議的計算語義

在UC模型下，協議Π=(Π1，Π2，…，Πn)是一組交互式圖靈機MΠ。狀態集STA TEM={init}∪S T AT E1∪ST ATE2∪…∪S T A T En，其中init表示初始狀態，STA TEi=(Πi，Δi，Γi)，Πi是協議對應參與者pi的執行程序，Δi將Πi中的變量名映射到工作紙帶的對應位置，Γi是指向當前命令的程序計數器，狀態遷移函數定義如下：

MΠ在初始狀態，若當前指令initialize（SID，PID0，PID1，…，PIDn），則從安全參數紙帶讀取安全參數k，從輸入紙帶讀取會話標識符SID、以及參與者標識符集合｛PID0，PID1，…，PIDn｝，初始化工作紙帶并分別將〈“sid”，SID〉，〈“pid”，PID0〉，〈“pid”，PID1〉，…，〈“pid”，PIDn〉存入變量MySID，MyID，PeerID1，…，PeerIDn中。Γ1指向下一條指令執行。狀態遷移到S TA T E1=(Π1，Δ1，Γ1)。

3.3符號語義

定義4協議的符號語義

在符號模型下，協議Π=(Π1，Π2，…，Πn)對應符號協議Πs。狀態集S T AT E=(Γ，Δ)，Γ是一個計數器，指向下一條將要執行的指令，Δ將Π中的變量名映射到消息項中的相應符號，狀態遷移函數定義如下：

Πs在初始狀態，若當前指令initialize（SID，PID0，PID1，…，PIDn），則將參與者初始知識集存入Δ中相應的變量名，包括所有參與者的標識符pi以及公鑰。Γ指向下一條指令執行。

4理想功能

在符號模型中，加密操作，簽名操作都是完善的。為了在UC模型中分析與符號模型中所對應的協議，給定任意協議，將其中相應的密碼學操作和算法替換成調用相應的理想功能，得到相應的-混合協議。下面給出對應的認證公鑰加密理想功能CPKE，認證數字簽名理想功能CSIG，雙線性對算法理想功能BILI的定義。

4.1認證數字簽名

同公鑰加密類似，在符號模型中，所有參與者的驗證密鑰都包含在參與者的初始知識中，也是通過可信第三方預先分配好的。因此，配合符號模型中的相應特性，將標準數字簽名理想功能擴展到了認證數字簽名理想功能CERT。

理想功能CERT

給定消息域M，簽名函數S：M→{0，1}*，驗證函數V:{0，1}*→M∪error。函數S為統計不可預測，函數V為確定函數。SID應為一個對偶，SID=（PID，SID′），PID是該實例的所有者。

簽名當收到本實例的所有者p發送的（Sign，SID，m），則

1）如果m?M，向p返回error；

2）如果m∈M，則

計算σ=S(m)；

記錄(m，σ，1)，并返回(S ignature，SID，m，σ)給參與者p。

驗證當收到參與者pi發送的(Verify，S ID，m，σ)，則

1）如果存在記錄(m，σ，b′)，則令b=b′；

2）否則，如果參與者pi沒有被攻擊者控制，則令b=0，并且記錄(m，σ，0)；

3）否則，令b=V(m，σ)，并且記錄(m，σ，b)；

向pi返回(Verified，SID，m，σ)。

當需要對消息進行簽名的時候，因為簽名是否泄漏消息內容并不會影響簽名體制的安全性，所以可以直接使用S(m)產生簽名消息σ。當簽名者被攻擊者控制的時候，由攻擊者決定消息簽名對是否有效。文獻［4］指出，EUF-ACMA安全的數字簽名算法UC安全地實現了標準的數字簽名理想功能SIG，并且通過SIG結合證書認證理想功能CA可以安全的實現CERT。

4.2雙線性對

理想功能BILI［5］

給定雙線性映射實例生成器IG，即輸入安全參數k，輸出五元組(q，G1，G2，g1，e)。q是一個大素數，G1是一個階為q的加法循環群，g1為G1中的生成元，G2是一個階為q的乘法循環群，雙線性對e：G1×G1→G2。

模冪算法當收到參與者pi發送的(Exponent，SID，x)，則

1）如果x?Zq，向pi返回error；

2）如果x∈Zq，則

若pi被攻擊者控制，則將x轉發給攻擊者，并從攻擊者處接收gx；

否則計算gx=gr

1，其中r←Zq；

記錄(x，gx)，返回gx給參與者pi（若已被記錄則返回error）。

雙線性對算法當收到參與者pi發送的(Bilinear，S ID，g y，gz，x)，則

1）如果存在記錄（y，gy），（z，gz），則計算k=gxyz2，并返回k給pi；

2）否則計算k=e(g y，gz)x，并返回k給pi。

當收到某參與方的計算模冪請求時，若該參與方沒有被攻擊者控制，則選擇一個隨機數r并計算，并保存模冪計算記錄。計算雙線性對的時候，由于正常計算的模冪一定在理想功能中有記錄，因此可以獲得對應秘密值。沒有計算過模冪的gy，gz，由于在理想功能中沒有記錄，則通過對運算計算。當被攻擊者控制的時候，由攻擊者來計算其模冪消息。若實例生成器IG滿足DBDH假設，則pIG安全實現BIL［

I6］。

5映射算法

映射引理是UCSA分析方法［7］中重要的技術工具。為了使得所定義的符號模型對于UC模型來說是可靠的，必須要證明符號模型中的攻擊者能力不弱于UC模型。UCSA方法通過將協議語法給出對應計算語義和符號語義，將UC模型下的協議執行與符號模型下的協議執行對應。

將首先定義UC模型下協議的計算跡，然后給出從計算跡到符號跡的映射算法，并證明其有效性。該映射算法是證明通用可復合符號分析方法具有計算可靠性的基礎［8］。

定義5計算跡

計算跡TR ACEΠ，A，Z(k，z)是當安全參數為k，環境Z輸入為z時，攻擊者A和環境Z執行-混合協議Π所觸發的事件序列H1，H2，…，Hs，其中Hs是

1）環境事件

["input"，si，{pj}]：表示啟動參與者{pj}一起執行協議Π的一個會話si。

2）攻擊者事件

["adversary"，m，{pj}]：表示攻擊者將消息m發送給參與者{pj}。

3）協議參與者事件

["message"，m，{pj}]：表示參與者pj將消息m發送給參與者集合｛pk｝。

["output"，m，si，{pj}]：表示參與者pj產生了一個本地輸出m。

在此，將{TRA C EΠ，A，Z(k，z)}k∈N，z∈{0，1}*簡寫為E XE CΠ，A，Z。

下面給出映射算法的具體定義，并且在映射引理中證明計算跡以壓倒性概率能夠被映射到對應有效的符號跡。

引理1映射引理

令TR ACEΠ，A，Z(k，z)是當安全參數為k，環境Z輸入為z時，攻擊者A和環境Z執行協議Π產生的計算跡。Πs表示對應的符號協議，ts表示計算跡t通過映射算法δ對應的符號跡。對于所有的簡單協議Π，有：

Pr[t←EX ECΠ，A，Z：ts不是Πs的一個有效符號跡]≤negl(k)［9］

證明分兩步進行。首先證明ts中包含［“fail”，δ(m)］的概率是可以忽略不計的。其次，證明如果ts中不包含［“fail”，δ(m)］，則ts是Πs的一個有效符號跡。

構造以任意消息項δ(m)為根的語法分析樹。語法樹的根節點是消息項δ(m)，語法樹的其他節點表示消息代數集合S中用于組成消息δ(m)的元素，邊表示集合S上的函數運算。ClosureiAdv表示符號化攻擊者根據TR ACEΠ，A，Z(k，z)前i個事件中的消息可以生成的攻擊者知識閉包。在此基礎上，下面證明按照映射算法δ，將TR ACEΠ，A，Z(k，z)映射為ts時，［“fail”，δ(m)］出現的概率可以忽略不計。

然而，攻擊者A在執行Π的過程中輸出了串m映射到消息項δ(m)，可以通過攻擊者A來構造攻擊者A′輸出串m′映射到消息項δ(m′)，其中δ(m′)是δ(m)到δ(m1)路徑上的一個節點。A′模擬A的運行輸出m，然后通過m的語法分析樹遞歸往下進行產生m′。

若δ(mi)=pair(m1，m2)，則A′將mi拆分，繼續往下走。

若δ(mi)=spk(m1)或者δ(mi)=svk(m1)，則A′可取出m1，繼續往下走。

若δ(mi)=encrypt(m1，m2)，如果PKE中存儲了明密文對(m1，mi)，則一定是攻擊者A合法的使用PKE進行的加密操作，所以A′可以直接取出m1，繼續往下走。如果PKE中沒有明密文對(m1，mi)，則解密操作是通過攻擊者提供的解密函數Dec進行的，A′可以運行Dec(mi)獲得m1，繼續往下走。

若δ(mi)=verify(m1，m2，m3)，A′可取出m1，繼續往下走。

若δ(mi)=exp(m1)，A′可取出m1，繼續往下走。

構造的攻擊者A′最終可以輸出m′。m′可以是如下幾種情況：

若δ(m′)=decrypt(m1，m2)，則m′的產生與A′的隨機性是完全獨立的。m′是PKE通過統計不可預測函數使用新鮮隨機性產生的二進制位串。由于加密函數的統計不可預測性質，成功猜對密文對應明文的概率是可忽略不計的；

若δ(m′)=sign(m1，m2)，m′是DS通過統計不可預測函數使用新鮮隨機性產生的二進制位串。由于簽名函數的統計不可預測性質，成功猜對該簽名的概率是可忽略不計的；

若δ(m′)=bili(m1，m2，m3)，m′是BILI通過統計不可預測函數使用新鮮隨機性產生的二進制位串。由于該函數的統計不可預測性質，成功猜對的概率是可忽略不計的；

若δ(m′)=ri，δ(m′)=d ki，δ(m′)=ski，則m′是由誠實參與者產生的k位隨機數，而能夠成功猜對該隨機數的概率是可忽略不計的；

綜上所述，針對攻擊者事件，［“fail”，δ(m)］出現的概率可以忽略不計。

由于ts中不包含［“fail”，δ(m)］，則攻擊者的行為都符合符號模型下的假設。根據定義1～4，符號協議和簡單協議在結構上是相同的，初始事件和誠實參與者事件也是一個有效的符號跡，所以如果攻擊者事件中不出現［“Fail”，δ(m)］，那么ts是一個有效的符號跡。

因此，Pr[t←TR ACEΠ，A，Z(k，z)：ts不是Πs的一個有效符號跡］≤negl(k)。

證畢

6計算可靠性

認證密鑰交換協議［10］是安全協議中的基礎協議之一。多個參與者需要在不可靠的通信環境中共同產生一個秘密的會話密鑰，并對通信對方身份具有一定確信度。

本節給出UC認證和密鑰交換的理想功能AU和KE，以及符號模型下的認證和密鑰交換協議的安全判定標準，并證明若符號協議滿足符號模型下的對應安全判定標準，則實際的簡單協議πUC實現了AU或KE。

在UC模型下，身份認證的理想功能AU以及密鑰交換的理想功能KE如下所示。

理想功能AU

1）當從參與者pi收到輸入（Authenticate，SID，pi），

如果不存在記錄（SID，pi），則記錄（SID，pi）；

發送（Authenticate，SID，pi）給攻擊者。

2）當從攻擊者收到（Output，SID，pi），

如果pi屬于會話SID的參與者，則檢查所有關于會話SID記錄（SID，pj），

如果此次會話的所有參與者都有記錄（SID，pj），則輸出（Output，SID，pi）給pi。

理想功能KE

1）當從參與者pi收到輸入（Establish，SID，pi），

發送（Establish，SID，pi）給攻擊者。

2）當從攻擊者收到（Deliverkey，SID，pi，k），如果pi屬于會話SID的參與者，

如果會話SID的所有參與者都沒有被攻擊者控制，且不存在記錄（SID，key），則從密鑰空間隨機選擇密鑰k0，并記錄（SID，k0）；

如果會話SID中有參與者被攻擊者控制，且不存在記錄（SID，key），則令k0=k，并記錄（SID，k0）；

輸出（Deliverkey，SID，pi，k0）給pi。

為了在符號模型下定義與UC理想功能對應的安全屬性，先給出模式的定義。

定義6認證性

協議的符號跡ts滿足：如果［“output”，fin?ished，si，p］∈ts，則對于會話si的任意參與者pj(j∈{1，…，n})都有［“output”，starting，si，pj］∈ts，稱協議滿足認證性。

定義7機密性

令Πrandom表示除了會話密鑰k換成一個隨機數外其他均與Πs相同的協議，如果對任意的攻擊者策略y，都滿足pattern(ψ(Πreal))=pattern(ψ(Πrandom))，稱協議關于k滿足機密性。

下面證明通用可復合符號化分析方法分析密鑰交換協議具有計算可靠性。

定理2計算可靠性定理

令Π為簡單協議，Πs為對應符號協議。如果密鑰交換協議Πs在符號模型下滿足認證性，則Π一定UC安全的實現了AU。如果密鑰交換協議Πs在符號模型下關于會話密鑰k滿足機密性，則Π一定UC安全的實現了KE［11］。

證明：

我們首先證明，如果密鑰交換協議Πs在符號模型下滿足認證性，則給定環境Z和攻擊者A一定存在理想模型下的攻擊者S，使得Z無法區分(Π，A)和（AU，S）。

我們還需要證明，如果密鑰交換協議Πs在符號模型下關于會話密鑰k滿足機密性，給定環境Z和攻擊者A一定存在理想模型下的攻擊者S，使得Z無法區分(Π，A)和（KE，S）。

假設對于所有的S，存在環境Z能以不可忽略的概率區分是在與實際協議Π和實際攻擊者A交互，還是在與理想功能KE和理想攻擊者S交互。即會話密鑰與收到的消息是否具有相關性，或者至少一個參與者的會話密鑰與其他參與者的不一致，或者攻擊者猜對會話密鑰的概率不可忽略。而根據映射引理，所有UC協議的計算跡都能夠以不可忽略的概率映射到符號跡。則相應符號協議Πs一定發生上述情形。因此Πs在符號模型下關于會話密鑰k不滿足機密性的定義，由此推出矛盾。

證畢

本文分析了通用可復合符號方法。

具體包括：1）給出了協議語法，并分別定義了該語法在符號模型與UC模型下的語義；2）給出符號模型下密碼學原語對應UC模型下的理想功能；3）在UC模型下定義了計算跡，給出如何將計算跡映射到符號跡的算法，并證明映射引理；4）給出了符號模型和UC模型下對應安全屬性的定義，并證明了密鑰交換協議的理想功能和符號模型下安全性的等價性。

［1］Canetti R，Krawczyk H.Universally composable notions of key exchange and secure channels［C］//Advances in EUROCRYPT 2012.Springer Berlin Heidelberg，2012：337-351.

［2］Ran Canetti，Jonathan Herzog.Universally composable symbolic analysis of mutual authentication and key-ex?change protocols（extended abstract）.In Proc.3rd Theo?ry of Cryptography Conference（TCC'06），volume 3876 of LNCS，pages 380-403.Springer，2015.Journal of Cryp?tography，2016.

［3］Canetti R.Universally composable security：A new para?digm for cryptographic protocols［C］//Foundations of Com?puter Science，2014.Proceedings 42nd IEEE Symposium on.IEEE，2014：136-145.

［4］A.Patil.On symbolic analysis of cryptographic protocols. Master's thesis，MassachusettsInstitute of Technology，2015.

［5］羅正欽.基于UC框架的安全協議形式化分析［D］.上海：上海交通大學，2012.

LUO Zhengqin.Formal analysis of security protocols based on UC framework［D］.Shanghai：Shanghai jiaotong university，2012.

［6］Cortier V，Kremer S，Warinschi B.A survey of symbolic methods in computational analysis of cryptographic sys?tems［J］.Journal of Automated Reasoning，2014，46：225-259.

［7］Meng B.A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model［J］.Information Technology Journal，2015，10（6）.

［8］Blanchet B.Security protocol verification：Symbolic and computational models［C］//Proceedings of the First inter?national conference on Principles of Security and Trust. Springer-Verlag，2014：3-29.

［9］Canetti R，Goldreich O，Halevi S.The random oracle meth?odology，revisited.Journal of the ACM，2014，51（4）：557-594.

［10］雷飛宇.UC安全多方計算模型及其典型應用研究［D］.上海：上海交通大學，2014.

LEI Feiyu.UC secure multi-party computation model and its typicalapplication research［D］.Shanghai：Shang?haijiaotong university，2014.

［11］Dawn Xiaodong S，Sergey B，Adrian P.Athena：a novel approach to efficient automatic security protocol analysis. Journal of Computer Security.9（1-2）：47-74.January 2011.

Universal Composable Symbolic Analysis Based on Key Circulation

FU Hao XIAO Jianxin
（Education Technology Center，Changsha Normal College，Changsha 410100）

In view of the presentincreasingly complex security protocols，the establishmentofcalculation and reliable securi?ty protocol in-depth study of symbolic analysis method，this paper proposes a new method to solve the problem，namely universal composable symbol analysis method.By extending the existing analysis method of the gm composite symbol，key exchange protocol based on bilinear pairings can be analyzed，and at the same time the reliability of the calculation can be guaranteed，also can en?sure the safety can be complex.The cryptography abstractoperation in the symbolmodelcombined with idealfunction in UC model，and proves thatifthe agreementunder the symbolmodelto meetthe corresponding security properties，is under the UC modelmust be the realization ofthe safety function ofthe corresponding ideal.

security protocols，the key cycle，universalcomposable，bilinear pairings

TP391

10.3969/j.issn.1672-9722.2017.08.027

2017年2月3日，

2017年3月17日

國家自然科學基金青年科學基金項目（編號：41604117）資助。

付浩，男，碩士，助理工程師，研究方向：網絡安全協議。肖建新，男，碩士，講師，研究方向：網絡安全。