付浩肖建新

基于密鑰循環(huán)的通用可復(fù)合符號(hào)分析?

付浩肖建新

（長(zhǎng)沙師范學(xué)院教育技術(shù)中心長(zhǎng)沙410100）

針對(duì)目前越來(lái)越復(fù)雜的安全協(xié)議，在建立計(jì)算可靠的安全協(xié)議符號(hào)分析方法的深入研究，提出了一種解決該問(wèn)題的新方法，即通用可復(fù)合符號(hào)分析方法。通過(guò)擴(kuò)展現(xiàn)有通用可復(fù)合符號(hào)分析方法，使其可以分析基于雙線性對(duì)的密鑰交換協(xié)議，并在保證計(jì)算可靠性的同時(shí)，還可以保證可復(fù)合安全性。將符號(hào)模型中的密碼學(xué)抽象操作與UC模型中的理想功能進(jìn)行了結(jié)合，并且證明了如果協(xié)議在符號(hào)模型下滿足了相應(yīng)的安全性質(zhì)，則在UC模型下一定安全的實(shí)現(xiàn)了相應(yīng)的理想功能。

安全協(xié)議；密鑰循環(huán)；通用可復(fù)合；雙線性對(duì)

Class NumberTP391

1引言

進(jìn)入21世紀(jì)以來(lái)，隨著互聯(lián)網(wǎng)網(wǎng)絡(luò)信息技術(shù)的飛速發(fā)展，信息網(wǎng)絡(luò)的廣泛應(yīng)用已成為人們工作和生活不可或缺的一部分。計(jì)算機(jī)網(wǎng)絡(luò)給人們生活帶來(lái)巨大便利，同時(shí)也對(duì)網(wǎng)絡(luò)上信息的安全保護(hù)提出了更高的要求。如果計(jì)算機(jī)網(wǎng)絡(luò)的安全問(wèn)題不能切實(shí)有效地解決，那么它的應(yīng)用和發(fā)展必定會(huì)受到一定的影響。

安全協(xié)議是解決網(wǎng)絡(luò)安全問(wèn)題最有效的手段之一。構(gòu)建安全網(wǎng)絡(luò)環(huán)境一般采用密碼技術(shù)的安全協(xié)議，安全協(xié)議的目標(biāo)既是為了實(shí)現(xiàn)信息的加密傳輸，也是為解決網(wǎng)絡(luò)中的安全問(wèn)題，它的正確性和安全性對(duì)于網(wǎng)絡(luò)安全極其重要。符號(hào)方法用形式化語(yǔ)言和符號(hào)推理對(duì)協(xié)議進(jìn)行分析和驗(yàn)證，更容易實(shí)現(xiàn)自動(dòng)化分析。但是由于對(duì)密碼學(xué)原語(yǔ)和攻擊者能力的理想建模，使得這類分析方法的肯定性結(jié)論往往并不直接具有現(xiàn)實(shí)意義，被認(rèn)為沒(méi)有真正建立起密碼學(xué)的可靠性。

為了簡(jiǎn)化安全協(xié)議的設(shè)計(jì)和分析，傳統(tǒng)的安全協(xié)議任務(wù)通常假設(shè)某個(gè)確定協(xié)議運(yùn)行在一個(gè)獨(dú)立的計(jì)算環(huán)境中，即孤立（stand-alone）模型。由Ca?netti提出的通用可復(fù)合（Universally Composable，UC）模型［1］可以保證協(xié)議的通用可復(fù)合安全，即在UC模型下證明安全的協(xié)議，在與其它協(xié)議并發(fā)運(yùn)行的情況下，或者作為一個(gè)系統(tǒng)的組件時(shí)，仍能保證協(xié)議的安全性。UC模型利用“子程序替換（Sub?routine substitution）”技術(shù)將嵌套的順序算法轉(zhuǎn)化為并行運(yùn)行的分布式安全協(xié)議，實(shí)現(xiàn)了安全協(xié)議的UC安全可復(fù)合操作。通用可復(fù)合安全的協(xié)議是協(xié)議模塊化設(shè)計(jì)和實(shí)現(xiàn)的基礎(chǔ)。

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

2通用可復(fù)合安全模型

通用可復(fù)合（UniversalComposable，UC）安全模型［3］是Canetti在2001年提出的基于模擬的通用安全協(xié)議設(shè)計(jì)與分析框架，根據(jù)真實(shí)協(xié)議和理想?yún)f(xié)議模擬不可區(qū)分來(lái)定義協(xié)議安全性。

2.1協(xié)議建模

在UC模型中，協(xié)議被建模成一個(gè)由交互式圖靈機(jī)和控制函數(shù)組成的系統(tǒng)，即交互式圖靈機(jī)系統(tǒng)（ITMs）。

理想功能與理想?yún)f(xié)議，理想功能是UC模型中非常重要的概念，用來(lái)描述安全協(xié)議所應(yīng)具有的功能，或者規(guī)范。

定義1實(shí)現(xiàn)理想功能

給定協(xié)議π和理想功能，如果稱協(xié)議π安全地實(shí)現(xiàn)了理想功能，則對(duì)于任意概率多項(xiàng)式時(shí)間內(nèi)的攻擊者A，都存在一個(gè)理想攻擊者S，使得對(duì)于任意環(huán)境Z

也就是說(shuō)，執(zhí)行協(xié)議π與使用理想功能是一樣安全的。任何在現(xiàn)實(shí)模型下協(xié)議執(zhí)行發(fā)生的攻擊行為，在理想模型下也是可行的。

2.2通用可復(fù)合安全

除了現(xiàn)實(shí)模型和理想模型外，Canetti引入了混合模型（hybrid model），并描述了混合模型中的協(xié)議，即混合協(xié)議。

定理1通用可復(fù)合安全定理（UC安全定理）

給定-混合協(xié)議π，如果稱協(xié)議r安全地實(shí)現(xiàn)了理想功能，則對(duì)于任意概率多項(xiàng)式時(shí)間內(nèi)的混合協(xié)議攻擊者H，都存在一個(gè)理想攻擊者S，使得對(duì)于任意環(huán)境Z

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

如果-混合協(xié)議π安全實(shí)現(xiàn)了理想功能，而且協(xié)議r安全地實(shí)現(xiàn)了理想功能，則復(fù)合協(xié)議πr一定安全地實(shí)現(xiàn)了理想功能。

根據(jù)UC理論，只需要分析協(xié)議在單個(gè)實(shí)例運(yùn)行情況下的安全性，就能夠?qū)⑵渫茝V到無(wú)限多實(shí)例并發(fā)的情形。因?yàn)閁C理論中的環(huán)境Z代表了任意多協(xié)議并發(fā)執(zhí)行的情況，所以不需要單獨(dú)考慮協(xié)議并發(fā)運(yùn)行的情況，簡(jiǎn)化了復(fù)雜的分析過(guò)程。其次，可以模塊化的構(gòu)建安全協(xié)議?？梢詫⑾嚓P(guān)的密碼學(xué)原語(yǔ)或者簡(jiǎn)單子協(xié)議通過(guò)理想功能表示。在構(gòu)建復(fù)雜協(xié)議的時(shí)候就能夠采用混合模型下的協(xié)議，并且調(diào)用上述理想功能。這樣可以簡(jiǎn)化復(fù)雜協(xié)議的描述與分析。當(dāng)將所采用的理想功能全部替換成相應(yīng)UC安全的協(xié)議時(shí)，就能夠直接得到在現(xiàn)實(shí)模型下具有安全性的協(xié)議。

3簡(jiǎn)單協(xié)議

由于UC模型中協(xié)議參與者是由任意的交互式圖靈機(jī)所表示的，而符號(hào)模型中所支持的操作種類有限，例如加密、解密、消息對(duì)等，所以并不是所有的協(xié)議都能在符號(hào)模型中表示出來(lái)。在UC模型中限制一類只使用特定動(dòng)作的安全協(xié)議，即簡(jiǎn)單協(xié)議。簡(jiǎn)單協(xié)議的結(jié)構(gòu)與符號(hào)模型中所支持的協(xié)議結(jié)構(gòu)類似，因此可以將特定的簡(jiǎn)單協(xié)議分別給出計(jì)算語(yǔ)義和符號(hào)語(yǔ)義，以便于對(duì)應(yīng)進(jìn)行分析。

3.1語(yǔ)法

定義2簡(jiǎn)單協(xié)議

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

3.2計(jì)算語(yǔ)義

定義3協(xié)議的計(jì)算語(yǔ)義

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

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

3.3符號(hào)語(yǔ)義

定義4協(xié)議的符號(hào)語(yǔ)義

在符號(hào)模型下，協(xié)議Π=(Π1，Π2，…，Πn)對(duì)應(yīng)符號(hào)協(xié)議Πs。狀態(tài)集S T AT E=(Γ，Δ)，Γ是一個(gè)計(jì)數(shù)器，指向下一條將要執(zhí)行的指令，Δ將Π中的變量名映射到消息項(xiàng)中的相應(yīng)符號(hào)，狀態(tài)遷移函數(shù)定義如下：

Πs在初始狀態(tài)，若當(dāng)前指令initialize（SID，PID0，PID1，…，PIDn），則將參與者初始知識(shí)集存入Δ中相應(yīng)的變量名，包括所有參與者的標(biāo)識(shí)符pi以及公鑰。Γ指向下一條指令執(zhí)行。

4理想功能

在符號(hào)模型中，加密操作，簽名操作都是完善的。為了在UC模型中分析與符號(hào)模型中所對(duì)應(yīng)的協(xié)議，給定任意協(xié)議，將其中相應(yīng)的密碼學(xué)操作和算法替換成調(diào)用相應(yīng)的理想功能，得到相應(yīng)的-混合協(xié)議。下面給出對(duì)應(yīng)的認(rèn)證公鑰加密理想功能CPKE，認(rèn)證數(shù)字簽名理想功能CSIG，雙線性對(duì)算法理想功能BILI的定義。

4.1認(rèn)證數(shù)字簽名

同公鑰加密類似，在符號(hào)模型中，所有參與者的驗(yàn)證密鑰都包含在參與者的初始知識(shí)中，也是通過(guò)可信第三方預(yù)先分配好的。因此，配合符號(hào)模型中的相應(yīng)特性，將標(biāo)準(zhǔn)數(shù)字簽名理想功能擴(kuò)展到了認(rèn)證數(shù)字簽名理想功能CERT。

理想功能CERT

給定消息域M，簽名函數(shù)S：M→{0，1}*，驗(yàn)證函數(shù)V:{0，1}*→M∪error。函數(shù)S為統(tǒng)計(jì)不可預(yù)測(cè)，函數(shù)V為確定函數(shù)。SID應(yīng)為一個(gè)對(duì)偶，SID=（PID，SID′），PID是該實(shí)例的所有者。

簽名當(dāng)收到本實(shí)例的所有者p發(fā)送的（Sign，SID，m），則

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

2）如果m∈M，則

計(jì)算σ=S(m)；

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

驗(yàn)證當(dāng)收到參與者pi發(fā)送的(Verify，S ID，m，σ)，則

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

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

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

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

當(dāng)需要對(duì)消息進(jìn)行簽名的時(shí)候，因?yàn)楹灻欠裥孤┫?nèi)容并不會(huì)影響簽名體制的安全性，所以可以直接使用S(m)產(chǎn)生簽名消息σ。當(dāng)簽名者被攻擊者控制的時(shí)候，由攻擊者決定消息簽名對(duì)是否有效。文獻(xiàn)［4］指出，EUF-ACMA安全的數(shù)字簽名算法UC安全地實(shí)現(xiàn)了標(biāo)準(zhǔn)的數(shù)字簽名理想功能SIG，并且通過(guò)SIG結(jié)合證書認(rèn)證理想功能CA可以安全的實(shí)現(xiàn)CERT。

4.2雙線性對(duì)

理想功能BILI［5］

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

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

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

2）如果x∈Zq，則

若pi被攻擊者控制，則將x轉(zhuǎn)發(fā)給攻擊者，并從攻擊者處接收gx；

否則計(jì)算gx=gr

1，其中r←Zq；

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

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

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

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

當(dāng)收到某參與方的計(jì)算模冪請(qǐng)求時(shí)，若該參與方?jīng)]有被攻擊者控制，則選擇一個(gè)隨機(jī)數(shù)r并計(jì)算，并保存模冪計(jì)算記錄。計(jì)算雙線性對(duì)的時(shí)候，由于正常計(jì)算的模冪一定在理想功能中有記錄，因此可以獲得對(duì)應(yīng)秘密值。沒(méi)有計(jì)算過(guò)模冪的gy，gz，由于在理想功能中沒(méi)有記錄，則通過(guò)對(duì)運(yùn)算計(jì)算。當(dāng)被攻擊者控制的時(shí)候，由攻擊者來(lái)計(jì)算其模冪消息。若實(shí)例生成器IG滿足DBDH假設(shè)，則pIG安全實(shí)現(xiàn)BIL［

I6］。

5映射算法

映射引理是UCSA分析方法［7］中重要的技術(shù)工具。為了使得所定義的符號(hào)模型對(duì)于UC模型來(lái)說(shuō)是可靠的，必須要證明符號(hào)模型中的攻擊者能力不弱于UC模型。UCSA方法通過(guò)將協(xié)議語(yǔ)法給出對(duì)應(yīng)計(jì)算語(yǔ)義和符號(hào)語(yǔ)義，將UC模型下的協(xié)議執(zhí)行與符號(hào)模型下的協(xié)議執(zhí)行對(duì)應(yīng)。

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

定義5計(jì)算跡

計(jì)算跡TR ACEΠ，A，Z(k，z)是當(dāng)安全參數(shù)為k，環(huán)境Z輸入為z時(shí)，攻擊者A和環(huán)境Z執(zhí)行-混合協(xié)議Π所觸發(fā)的事件序列H1，H2，…，Hs，其中Hs是

1）環(huán)境事件

["input"，si，{pj}]：表示啟動(dòng)參與者{pj}一起執(zhí)行協(xié)議Π的一個(gè)會(huì)話si。

2）攻擊者事件

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

3）協(xié)議參與者事件

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

["output"，m，si，{pj}]：表示參與者pj產(chǎn)生了一個(gè)本地輸出m。

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

下面給出映射算法的具體定義，并且在映射引理中證明計(jì)算跡以壓倒性概率能夠被映射到對(duì)應(yīng)有效的符號(hào)跡。

引理1映射引理

令TR ACEΠ，A，Z(k，z)是當(dāng)安全參數(shù)為k，環(huán)境Z輸入為z時(shí)，攻擊者A和環(huán)境Z執(zhí)行協(xié)議Π產(chǎn)生的計(jì)算跡。Πs表示對(duì)應(yīng)的符號(hào)協(xié)議，ts表示計(jì)算跡t通過(guò)映射算法δ對(duì)應(yīng)的符號(hào)跡。對(duì)于所有的簡(jiǎn)單協(xié)議Π，有：

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

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

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

然而，攻擊者A在執(zhí)行Π的過(guò)程中輸出了串m映射到消息項(xiàng)δ(m)，可以通過(guò)攻擊者A來(lái)構(gòu)造攻擊者A′輸出串m′映射到消息項(xiàng)δ(m′)，其中δ(m′)是δ(m)到δ(m1)路徑上的一個(gè)節(jié)點(diǎn)。A′模擬A的運(yùn)行輸出m，然后通過(guò)m的語(yǔ)法分析樹遞歸往下進(jìn)行產(chǎn)生m′。

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

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

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

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

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

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

若δ(m′)=decrypt(m1，m2)，則m′的產(chǎn)生與A′的隨機(jī)性是完全獨(dú)立的。m′是PKE通過(guò)統(tǒng)計(jì)不可預(yù)測(cè)函數(shù)使用新鮮隨機(jī)性產(chǎn)生的二進(jìn)制位串。由于加密函數(shù)的統(tǒng)計(jì)不可預(yù)測(cè)性質(zhì)，成功猜對(duì)密文對(duì)應(yīng)明文的概率是可忽略不計(jì)的；

若δ(m′)=sign(m1，m2)，m′是DS通過(guò)統(tǒng)計(jì)不可預(yù)測(cè)函數(shù)使用新鮮隨機(jī)性產(chǎn)生的二進(jìn)制位串。由于簽名函數(shù)的統(tǒng)計(jì)不可預(yù)測(cè)性質(zhì)，成功猜對(duì)該簽名的概率是可忽略不計(jì)的；

若δ(m′)=bili(m1，m2，m3)，m′是BILI通過(guò)統(tǒng)計(jì)不可預(yù)測(cè)函數(shù)使用新鮮隨機(jī)性產(chǎn)生的二進(jìn)制位串。由于該函數(shù)的統(tǒng)計(jì)不可預(yù)測(cè)性質(zhì)，成功猜對(duì)的概率是可忽略不計(jì)的；

若δ(m′)=ri，δ(m′)=d ki，δ(m′)=ski，則m′是由誠(chéng)實(shí)參與者產(chǎn)生的k位隨機(jī)數(shù)，而能夠成功猜對(duì)該隨機(jī)數(shù)的概率是可忽略不計(jì)的；

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

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

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

證畢

6計(jì)算可靠性

認(rèn)證密鑰交換協(xié)議［10］是安全協(xié)議中的基礎(chǔ)協(xié)議之一。多個(gè)參與者需要在不可靠的通信環(huán)境中共同產(chǎn)生一個(gè)秘密的會(huì)話密鑰，并對(duì)通信對(duì)方身份具有一定確信度。

本節(jié)給出UC認(rèn)證和密鑰交換的理想功能AU和KE，以及符號(hào)模型下的認(rèn)證和密鑰交換協(xié)議的安全判定標(biāo)準(zhǔn)，并證明若符號(hào)協(xié)議滿足符號(hào)模型下的對(duì)應(yīng)安全判定標(biāo)準(zhǔn)，則實(shí)際的簡(jiǎn)單協(xié)議πUC實(shí)現(xiàn)了AU或KE。

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

理想功能AU

1）當(dāng)從參與者pi收到輸入（Authenticate，SID，pi），

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

發(fā)送（Authenticate，SID，pi）給攻擊者。

2）當(dāng)從攻擊者收到（Output，SID，pi），

如果pi屬于會(huì)話SID的參與者，則檢查所有關(guān)于會(huì)話SID記錄（SID，pj），

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

理想功能KE

1）當(dāng)從參與者pi收到輸入（Establish，SID，pi），

發(fā)送（Establish，SID，pi）給攻擊者。

2）當(dāng)從攻擊者收到（Deliverkey，SID，pi，k），如果pi屬于會(huì)話SID的參與者，

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

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

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

為了在符號(hào)模型下定義與UC理想功能對(duì)應(yīng)的安全屬性，先給出模式的定義。

定義6認(rèn)證性

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

定義7機(jī)密性

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

下面證明通用可復(fù)合符號(hào)化分析方法分析密鑰交換協(xié)議具有計(jì)算可靠性。

定理2計(jì)算可靠性定理

令Π為簡(jiǎn)單協(xié)議，Πs為對(duì)應(yīng)符號(hào)協(xié)議。如果密鑰交換協(xié)議Πs在符號(hào)模型下滿足認(rèn)證性，則Π一定UC安全的實(shí)現(xiàn)了AU。如果密鑰交換協(xié)議Πs在符號(hào)模型下關(guān)于會(huì)話密鑰k滿足機(jī)密性，則Π一定UC安全的實(shí)現(xiàn)了KE［11］。

證明：

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

我們還需要證明，如果密鑰交換協(xié)議Πs在符號(hào)模型下關(guān)于會(huì)話密鑰k滿足機(jī)密性，給定環(huán)境Z和攻擊者A一定存在理想模型下的攻擊者S，使得Z無(wú)法區(qū)分(Π，A)和（KE，S）。

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

證畢

本文分析了通用可復(fù)合符號(hào)方法。

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

［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框架的安全協(xié)議形式化分析［D］.上海：上海交通大學(xué)，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安全多方計(jì)算模型及其典型應(yīng)用研究［D］.上海：上海交通大學(xué)，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日

國(guó)家自然科學(xué)基金青年科學(xué)基金項(xiàng)目（編號(hào)：41604117）資助。

付浩，男，碩士，助理工程師，研究方向：網(wǎng)絡(luò)安全協(xié)議。肖建新，男，碩士，講師，研究方向：網(wǎng)絡(luò)安全。