胡亞希

摘要：針對(duì)目前越來(lái)越復(fù)雜的安全協(xié)議，在計(jì)算可靠的安全協(xié)議符號(hào)分析方法的基礎(chǔ)上，提出了一種計(jì)算可靠且支持雙線性對(duì)、對(duì)稱加密以及密鑰循環(huán)的安全協(xié)議符號(hào)模型，該模型明確指定雙線性對(duì)實(shí)例生成器和加密算法需要滿足的安全屬性，并證明了在滿足這些安全屬性的條件下，符號(hào)方法分析的不可區(qū)分屬性蘊(yùn)含計(jì)算方法分析的不可區(qū)分屬性，這保證了該模型具有計(jì)算可靠性。同時(shí)，該模型通過(guò)增強(qiáng)攻擊者對(duì)密鑰循環(huán)的控制能力去除了無(wú)密鑰循環(huán)的限制。

關(guān)鍵詞：安全協(xié)議;符號(hào)方法;計(jì)算可靠性;通用可復(fù)合;雙線性對(duì)

中圖分類號(hào)：TP393 ? ? ?文獻(xiàn)標(biāo)識(shí)碼：A

文章編號(hào)：1009-3044（2021）32-0040-04

人類邁入21世紀(jì)，隨著信息技術(shù)的蓬勃發(fā)展，計(jì)算機(jī)網(wǎng)絡(luò)逐漸成為人們工作和生活不可或缺的一部分。在互聯(lián)網(wǎng)上，每天交換著巨量的數(shù)據(jù)，如何保證這些數(shù)據(jù)的安全，成為當(dāng)下網(wǎng)絡(luò)安全研究者們的關(guān)注焦點(diǎn)。

密碼協(xié)議是保障通信系統(tǒng)安全的重要手段，其本身的安全性和可靠性直接關(guān)系到網(wǎng)絡(luò)與通信系統(tǒng)的安全[1]。對(duì)于網(wǎng)絡(luò)安全協(xié)議的形式化分析，一直存在兩類不同的方法：計(jì)算方法和符號(hào)方法。計(jì)算方法是在概率論和計(jì)算復(fù)雜性理論基礎(chǔ)上的一種“歸約”方法，其結(jié)果更具密碼學(xué)可靠性，但是證明過(guò)程是高度創(chuàng)造性的手工數(shù)學(xué)式證明，這對(duì)于目前越來(lái)越復(fù)雜的安全協(xié)議，不僅證明本身越來(lái)越復(fù)雜，而且證明的正確性也越來(lái)越不容易[2]。符號(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é)的可靠性[3]。

Abadi和Rogaway[4]于2000年首次結(jié)合計(jì)算方法和符號(hào)方法，研究了不可區(qū)分屬性的計(jì)算可靠性，提出在無(wú)密鑰循環(huán)且對(duì)稱加密算法滿足type-0安全的條件下，如果消息在符號(hào)模型下具有不可區(qū)分性，則它們?cè)谟?jì)算模型下對(duì)應(yīng)的二進(jìn)制位串同樣具有不可區(qū)分性。Abadi和Rogaway的研究雖然揭示了符號(hào)模型和計(jì)算模型之間關(guān)聯(lián)，但其要求消息中只能包含對(duì)稱加密原語(yǔ)，且不包含密鑰循環(huán)。為此，本文通過(guò)擴(kuò)展該方法，提出了包含雙線性對(duì)和對(duì)稱加密等原語(yǔ)的符號(hào)模型，去除了無(wú)密鑰循環(huán)的限制，并證明了擴(kuò)展后的方法依然具有計(jì)算可靠性。

1 符號(hào)模型

在符號(hào)模型中，消息通過(guò)符號(hào)表達(dá)式表示。Data，Keys和Nonce是互不相交的可數(shù)集合，分別表示協(xié)議中所有的數(shù)據(jù)、密鑰和新鮮值的符號(hào)集合。d，d1，d2，…通常表示集合Data中的元素，k， k1， k2，…通常表示集合Keys中的元素，x， x1， x2，…通常表示集合Nonce中的元素。g1和g2分別表示雙線性對(duì)中加法循環(huán)群G1和乘法循環(huán)群G2的生成元。p表示形如ax1x2x3+ bx4x5x6+…的多項(xiàng)式（Ploy），a， b等均為任意實(shí)數(shù)。

定義1-1：消息。消息的語(yǔ)法可由如下BNF規(guī)則給出：

msg∷=keys |d |x |g1x|（msg，msg） |{msg}keys

keys∷=k | g2p

消息（M，N）表示消息M和N的連接。{M}k表示用密鑰k加密消息M。g1x，g2p分別表示群G1和群G2中的元素。表達(dá)式中的項(xiàng)都是符號(hào)，而不是實(shí)際應(yīng)用中的二進(jìn)制位串。例如，（M，N）=（M′，N′）當(dāng)且僅當(dāng)M=M′且N=N′;（M，N）必定和{M′}k不相等;類似地，{M}k={M′}k′當(dāng)且僅當(dāng)M=M′且k=k′。通常（（M1，M2）， M3）簡(jiǎn)寫成（M1，M2， M3），{（M1，M2）}k簡(jiǎn)寫成{M1，M2}k。

為了表示攻擊者不能解密的消息，引入模式的定義，增加了符號(hào)“?”。直觀上，模式是表達(dá)式集合的擴(kuò)展，增加了攻擊者不能解密的消息表達(dá)式類型。但消息的模式比消息本身的結(jié)構(gòu)要簡(jiǎn)單。

定義1-2：模式。模式的語(yǔ)法可由如下BNF規(guī)則給出：

pat∷=keys |d |x |g1x|（pat，pat） |{pat}keys| ?

keys∷=k | g2p

在給出安全性定義之前，需要先定義攻擊者獲取信息的能力，即推演關(guān)系“?”。M ?t表示在沒(méi)有任何先驗(yàn)知識(shí)的情況下，攻擊者通過(guò)消息集合M可以推斷得到t。

定義1-3：推演關(guān)系。推演關(guān)系“?”是一種最小關(guān)系，需滿足以下三個(gè)條件：

1） 若t?M，則M?t， M?l;

2） 若M?x，則M? g1x;

若M?x且M? g1y， M? g1z，則M? g2xyz;

若M?g2p且M?g2q，則M? g2lp+q， l?Z;

3） 若M?t1且M?t2，則M?（t1，t2）;

若M?（t1，t2），則M?t1且M?t2;

若M?t且M?k，則M?{t}k;

若M?{t}k且M ?k，則M?t;

為了表示消息和消息模式之間的對(duì)應(yīng)關(guān)系，定義模式函數(shù)p（M，T）。將給定密鑰集合T和消息M映射到一個(gè)模式P，直觀上，該模式就是攻擊者在擁有密鑰集合T的情況下從M能獲得的信息。

定義1-4：模式函數(shù)。模式函數(shù) p（M，T）定義如下：

1） p（k，T）=k （k?Keys）

2） p（d，T）=d （d?Data）

3） p（x，T）=x （x?Nonces）

4） p（g1x，T）= g1x （x?Nonces）

5） p（g2p，T）= g2p （p?Poly）

6） p（（M，N），T）=（p（M，T），p（N，T））

7） 若k?T，則p（{M}k，T）={p（M，T）}k

8） 若k?T，則p（{M}k，T）=struct（{M}k）

其中struct（M）定義如下：

1） struct（k）= ? （k?Keys）

2） struct（d）= ? （d?Data）

3） struct （x）= ? （x?Nonces）

4） struct （g1x）=? （x?Nonces）

5） struct （M，N）=（struct （M），struct （N））

6） struct （{M}k）={struct （M）}?

定義1-5 ：消息模式。消息M的模式，用pattern（M）表示，定義為：

pattern（M）=p（M，F(xiàn)IX（áM））。

其中áM（T）= r（p（M，T）），而r（P）={k?Keys |parts（P）?k}，parts（P）定義如下：

1） parts（k）= k ?（k?Keys）

2） parts （d）= d （d?Data）

3） parts （x）= x （x?Nonces）

4） parts （g1x）= g1x （x?Nonces）

5） parts （P，Q）=parts （P）èparts （Q）

6） parts （{P}k）= {P}èparts （P）

parts（P）表示在模式P中出現(xiàn)的所有子表達(dá)式的集合，除去其中僅作為對(duì)稱加密用的密鑰。r（P）表示模式P的可恢復(fù)密鑰集合。FIX（áM）=?0láMi（Keys），l=|Keys（M）|，在這里Keys（M）表示消息表達(dá)式M中出現(xiàn)的所有密鑰的集合。在定義攻擊者擁有的密鑰集合T時(shí)使用了求最大不動(dòng)點(diǎn)的方式，使得攻擊者可以獲得消息中的循環(huán)密鑰。

例1：M= （， ）

áM（Keys） = r（p（M，Keys））

= r （，）

= {k1，， }

áM2（Keys） =r（p（M，{k1，， }））

= r（， ）

= {， }

áM3（Keys） =r（p（M，{， }））

= r（， ）

= {， }

FIX（áM） ={， }

pattern（M）=p（M，F(xiàn)IX（áM））=（ ， ）

消息之間的不可區(qū)分通過(guò)等價(jià)關(guān)系定義，表示在沒(méi)有預(yù)知相關(guān)密鑰的情況下，兩條消息在攻擊者看來(lái)是等價(jià)的。例如，攻擊者不能僅僅通過(guò)密文{0}k1和{1}k2獲得密鑰，因此攻擊者不能解密和區(qū)分這些密文，所以{0}k1和{1}k2是等價(jià)的。類似地，對(duì)偶（0，{0}k1）和（0，{1}k2）也是等價(jià)的。但是，（k1，{0}k1）和（k2，{1}k2）就不是等價(jià)的了，因?yàn)楣粽呖梢詮钠浍@知密鑰，并解密{0}k1和{1}k2得到0和1，以此區(qū)分這兩條消息。

定義1-6：等價(jià)。兩條消息等價(jià)當(dāng)且僅當(dāng)存在密鑰替換s1和s2使得他們對(duì)應(yīng)的消息模式相同，即M@N當(dāng)且僅當(dāng) pattern（M） = pattern（Ns1s2）

其中密鑰替換s1是密鑰集合Keys上的雙射函數(shù)。密鑰替換s2是保持線性關(guān)系的多項(xiàng)式換名，即對(duì)g2p中指數(shù)p的換名，對(duì)消息中出現(xiàn)的若干多項(xiàng)式pi以及攻擊者可獲得的mj，"ai?Z，"bj?Z，s2滿足?aipi=?bjmj當(dāng)且僅當(dāng)?ai（pis2）=?bjmj，其中mj={xyz|x，y，z?Nonces且M? g2mj}。

例2：M=， N=，

pattern（M）=

pattern（N）=

M@N

例3：M=，N=，

pattern（M）=

pattern（N）=

M[?]N

2 計(jì)算模型

在計(jì)算模型中，消息就是{0，1}*上的二進(jìn)制位串。

定義2-1：可忽略函數(shù)。negl（）為可忽略函數(shù)，若對(duì)于任意一個(gè)多項(xiàng)式p，都存在一個(gè)N（自然數(shù)），使得當(dāng)n>N時(shí)，都能滿足negl（n） <1/p（n）。

定義2-2：計(jì)算不可區(qū)分。兩個(gè)概率總體D={Dh}和D′={D′h}。A代表任意概率多項(xiàng)式時(shí)間攻擊者，h代表安全參數(shù)，存在可忽略函數(shù)negl（h），使得：

|Pr[x←Dh：A（h，x）=1]-Pr[x←D′h：A（h，x）=1]|￡negl（h）

則稱D和D′是計(jì)算不可區(qū)分的，記作D≈D′。

定義2-3：對(duì)稱加密算法。對(duì)稱加密算法（SE）由密鑰生成算法（Gen）、加密算法（Enc）和解密算法（Dec）三個(gè)關(guān)于安全參數(shù)h的多項(xiàng)式時(shí)間算法組成，即SE=（Gen，Enc，Dec）。

定義2-4：不可區(qū)分選擇明文攻擊安全。對(duì)于任意安全參數(shù)h，任意概率多項(xiàng)式時(shí)間圖靈機(jī)攻擊者A的優(yōu)勢(shì)：

Adv（A）= Pr[AOL（h）=1]-Pr[AOR（h）=1]

如h為可忽略函數(shù)，則可認(rèn)為SE=（Gen，Enc，Dec）滿足不可區(qū)分選擇明文攻擊安全。

攻擊者是一個(gè)圖靈機(jī)，它和預(yù)言機(jī)商定了一個(gè)目標(biāo)密碼體制SE，預(yù)言機(jī)通過(guò)Gen生成隨機(jī)密鑰k，攻擊者可以選擇兩條不同的消息m0和m1發(fā)送給預(yù)言機(jī)。該預(yù)言機(jī)有OL和OR兩種方式：用Enck及新鮮隨機(jī)硬幣加密詢問(wèn)m0或者加密m1。攻擊者的優(yōu)勢(shì)就是預(yù)言機(jī)以第一種方式實(shí)現(xiàn)時(shí)攻擊者輸出1的概率和預(yù)言機(jī)以第二種方式實(shí)現(xiàn)時(shí)攻擊者輸出1的概率差。若攻擊者的最大優(yōu)勢(shì)是一個(gè)關(guān)于攻擊者的計(jì)算資源慢增長(zhǎng)的函數(shù)，則認(rèn)為該加密算法是IND-CPA安全的。

定義2-5：雙線性映射和雙線性對(duì)。令q是一個(gè)大素?cái)?shù)，G1是一個(gè)階為q的加法循環(huán)群，g1為G1中的生成元，G2是一個(gè)階為q的乘法循環(huán)群。定義在（G1 ，G1）上的一個(gè)雙線性對(duì)是一個(gè)映射關(guān)系e：G1×G1? G2，滿足下面的三條性質(zhì)[5]：

雙線性：對(duì)于任意P， Q1， Q2?G1，x，y?Zq*，有：

e（Q1x，Q2y）=e（Q1，Q2）xy，

e（P，Q1+Q2）=e（P，Q1）e（P，Q2），

e（Q1+Q2，P）=e（Q1，P）e（Q2，P），

非退化性：e（g1，g1）是G2的生成元，用g2表示，g211G2。

可計(jì)算性：對(duì)于任意Q1， Q2? G1，存在一種有效的算法能夠快速計(jì)算e（Q1，Q2）。

雙線性對(duì)實(shí)例生成器IG是一個(gè)概率多項(xiàng)式時(shí)間算法，給定安全參數(shù)h，輸出五元組（q，G1，G2，g1，e）。

定義2-6：判定雙線性Diffie-Hellman假設(shè)（DBDH假設(shè)）。對(duì)于任意安全參數(shù)h，任意概率多項(xiàng)式時(shí)間圖靈機(jī)攻擊者A的優(yōu)勢(shì)：

Adv（A）=Pr[（q，G1，G2，g1，e）?IG（h）， x，y，z?Zq： A（g1，g1x，g1y，g1z，g2xyz）=1]

-Pr[（q，G1，G2，g1，e）?IG（h），x，y，z，r?Zq： A（g1，g1x，g1y，g1z，g2r）=1]

是h的可忽略函數(shù)，則稱實(shí)例生成器IG滿足DBDH假設(shè)，即攻擊者在只有g(shù)1x，g1y，g1z的情形下，區(qū)分g2xyz和隨機(jī)群元素的概率是可忽略的。

為了獲得符號(hào)模型消息不可區(qū)分的計(jì)算可靠性，首先需要通過(guò)一個(gè)映射算法將消息的符號(hào)表達(dá)式轉(zhuǎn)換為計(jì)算模型中的二進(jìn)制位串。

定義2-7：符號(hào)表達(dá)式的計(jì)算解釋。給定對(duì)稱加密算法SE=（Gen，Enc，Dec）和雙線性對(duì)實(shí)例生成器IG，以及安全參數(shù)h，消息符號(hào)表達(dá)式M在計(jì)算模型中有其對(duì)應(yīng)計(jì)算解釋，即概率總體[M]SE，IG，h，可以通過(guò)如下兩個(gè)步驟得到：

首先初始化，使用雙線性對(duì)實(shí)例生成器IG（h）生成五元組得到t（g1）和t（g2），對(duì)消息M中出現(xiàn)的每個(gè)符號(hào)k，通過(guò)密鑰生成算法Gen（h）隨機(jī)生成位串t（k）與之對(duì)應(yīng)，對(duì)消息M中出現(xiàn)的每個(gè)符號(hào)d，從位串{0，1}n中隨機(jī)選擇值t（d）與之對(duì)應(yīng)，對(duì)消息M中出現(xiàn)的每個(gè)符號(hào)x，從Zq中隨機(jī)選擇值t（x）與之對(duì)應(yīng);

其次，根據(jù)消息的語(yǔ)法定義使用算法Convert遞歸解釋M中的每個(gè)項(xiàng)：

1） 若M=k則返回<t（k），”key”>，

2） 若M=d則返回<t（d），”data”>，

3） 若M=x則返回<t（x），”nonce”>，

4） 若M= g1x則計(jì)算模冪e=t（g1）t（x）并返回<e，”exponent”>，

5） 若M= g2p則在Zq中計(jì)算t（p），以及模冪b=t（g2）t（p）并返回<b，”bilinear”>，

6） 若M=（M1，M2）則返回<（Convert（M1），Convert（M2）），”pair”>，

7） 若M={M1}k則計(jì)算x←Convert（M1），y←Enct（k） （x），并返回<y，”ciphertext”>。

2.1 計(jì)算可靠性

定理2-1：計(jì)算可靠性定理。

給定消息符號(hào)表達(dá)式M和N，且對(duì)稱加密算法SE=（Gen，Enc，Dec）是IND-CPA安全的，雙線性對(duì)實(shí)例生成器IG滿足DBDH假設(shè)，則：M@NT[M] SE，IG≈[N] SE，IG。

證明：

前文已經(jīng)說(shuō)明符號(hào)表達(dá)式等價(jià)蘊(yùn)含了計(jì)算不可區(qū)分，也就是如果有兩條消息在符號(hào)方法中等價(jià)，則它們?cè)谟?jì)算解釋下對(duì)應(yīng)的概率分布總體也是計(jì)算不可區(qū)分的。為了證明該定理，首先引入3個(gè)引理。

引理1：給定消息符號(hào)表達(dá)式M，若對(duì)稱加密算法SE=（Gen，Enc，Dec）滿足IND-CPA安全，雙線性對(duì)實(shí)例生成器IG滿足DBDH假設(shè)，s1是密鑰集合Keys上的雙射函數(shù)，則[M] SE，IG≈[Ms1] SE，IG。

證明根據(jù)消息符號(hào)表達(dá)式的計(jì)算解釋的定義，消息符號(hào)表達(dá)式在計(jì)算模型中給出對(duì)應(yīng)計(jì)算解釋時(shí)，消息M中出現(xiàn)的每個(gè)密鑰符號(hào)通過(guò)密鑰生成算法Gen（h）隨機(jī)生成位串與之對(duì)應(yīng)。因此密鑰根據(jù)s1的換名不影響其計(jì)算解釋的分布，所以不會(huì)影響消息的分布。引理1得證。

引理2：給定消息符號(hào)表達(dá)式M，若對(duì)稱加密算法SE=（Gen，Enc，Dec）是IND-CPA安全的，雙線性對(duì)實(shí)例生成器IG滿足DBDH假設(shè)，s2是保持線性關(guān)系的多項(xiàng)式換名，則[M]SE，IG≈[Ms2] SE，IG。

證明由于s2是對(duì)g2p中指數(shù)p的換名，因此滿足?aipi=?bjmj當(dāng)且僅當(dāng)?ai（pis2）=?bjmj，mj={xyz|x，y，z?Nonces且M?g2mj}。下面分兩種情況討論。

第一種情況：若替換項(xiàng)xyz中某個(gè)指數(shù)在消息項(xiàng)中有出現(xiàn)，則必有一個(gè)指數(shù)不在消息項(xiàng)或者g1的指數(shù)出現(xiàn)。否則M? g2xyz，此時(shí)必然存在ai，bj使得?aipi=?bjmj但?ai（pis2）1?bjmj。因此，xyz對(duì)其他項(xiàng)沒(méi)有影響。由于指數(shù)的計(jì)算解釋也是隨機(jī)選取的，所以對(duì)其的替換不會(huì)影響消息的分布。

第二種情況：若替換項(xiàng)xyz中每個(gè)指數(shù)在消息項(xiàng)中都沒(méi)有出現(xiàn)，則區(qū)分[M] SE，IG和[Ms2] SE，IG的概率與解決DBDH問(wèn)題的概率相同，由于IG滿足DBDH假設(shè)，因此[M] SE，IG≈[Ms2] SE，IG。引理2得證。

引理3：給定消息符號(hào)表達(dá)式M，若對(duì)稱加密算法SE=（Gen，Enc，Dec）是IND-CPA安全的，雙線性對(duì)實(shí)例生成器IG滿足DBDH假設(shè)，則[M] SE，IG≈[pattern（M）] SE，IG。

證明根據(jù)模式函數(shù)的定義，有：

若k?T，則p（{M}k，T）={p（M，T）}k，

若k?T，則p（{M}k，T）= {struct（M）}k，

而M中出現(xiàn)的所有k都滿足k?Keys，因此，有：

p（M，Keys）=M， ? ? ?（1）

同時(shí)，不難得到：

p（p（M，S），T）=p（M，S?T）。 （2）

又r（M）={k?Keys |parts（M）?k}，有：

r（p（M，T））ír（M）。 （3）

由等式（1），有：

[M]SE，IG=[p（M，Keys）]SE，IG=[p（M，áM0（Keys））]SE，IG，

而根據(jù)消息模式的定義，有：

pattern（M） =p（M，F(xiàn)IX（áM）），

FIX（áM）=?0láMi（Keys）， l=|Keys （M）|，

áM（K）=r（p（M，K））。

所以，由等式（2）（3），有：

若K1íK2í Keys，則

áM（K1）=r（p（M，K1））

=r（p（M，K1? K2））

=r（p（p（M，K2）， K1））

ír（p（M， K2））

=áM（K2），

即áM（K1） íáM（K1）。

因此，áM是單調(diào)函數(shù)，且FIX（áM）= áMl（Keys （M）），l= |Keys （M）|。

所以，有：

[pattern（M）]SE，IG=[p（M，F(xiàn)IX（áM））]SE，IG=[p（M， áMl（Keys））]SE，IG。

因此，若能證得"i，有：

[p（M，áMi（Keys））]SE，IG≈[p（M，áMi+1（Keys））]SE，IG ? ? ? （4）

則根據(jù)傳遞性，有：

[p（M，áM0（Keys））]SE，IG≈[p（M，áMl（Keys））]SE，IG。

下面證明等式（4）。

令T=áMi（Keys），

M′=p（M，T）=p（M，áMi（Keys）） ? ?（5）

對(duì)模式p（M′，r（M′））進(jìn)行分層。根據(jù)r（M′）定義，Keys（M′）-r（M′）={k1，k2，…，kn}為M′中沒(méi)有在加密的消息中出現(xiàn)，而僅作為對(duì)稱加密用的密鑰。因此，{k1，k2，…，kn}中沒(méi)有密鑰循環(huán)。令M′i= p（M′， r（M′）è { k1， k2，…，kn}），其中若M′i中有子消息項(xiàng)是ki對(duì)kj加密，則i>j。根據(jù)安全性定義，若存在區(qū)分器D可區(qū)分[M′i]SE，IG和[M′i+1] SE，IG，則可構(gòu)造攻破對(duì)稱加密算法SE=（Gen，Enc，Dec）的IND-CPA安全的攻擊者A，且攻擊者A的優(yōu)勢(shì)不可忽略，與已知矛盾。

因此，有：

[M′ i] SE，IG i≈[M′i+1] SE，IG。

根據(jù)傳遞性，有

[M′0] SE，IG i≈[M′n] SE，IG。

而

M′0= p（M′，r（M′）），M′n=M′，

所以[M′]SE，IG≈[p（M′，r（M′））]SE，IG。

又，由等式（5）（2）以及áM的單調(diào)性，有

p（M′，r（M′）） =p（p（M，T），áM（T））

=p（M，T?áM（T））

=p（M，áM（T）），

因此[M′]SE，IG≈[p（M′，r（M′））]SE，IG≈[p（M，áM（T））]SE，IG。

由于p（M，áMi+1（Keys）） =p（M，áM（T）），

從而[p（M，áMi（Keys））]SE，IG=[M′]SE，IG

≈[p（M，áM（T））]SE，IG

≈[p（M，áMi+1（Keys））]SE，IG，

等式（4）得證。

因此，有：

[M]SE，IG≈[pattern（M）] SE，IG。

引理3得證。

下面開始證明定理1。

由引理3可得

[M]SE，IG≈[pattern（M）]SE，IG

[pattern（N）]SE，IG≈[N]SE，IG，

由引理1可得

[pattern（M）]SE，IG≈[pattern（Ms1）]SE，IG

由引理2可得

[pattern（Ms1）]SE，IG≈[pattern（Ms1s2）]SE，IG

由于M@N，則根據(jù)等價(jià)關(guān)系的定義

pattern（N）=pattern（Ms1s2），

綜上所述，可得

[M]SE，IG≈[pattern（M）]SE，IG

≈[pattern（Ms1）]SE，IG

≈[pattern（Ms1s2）]SE，IG

≈[pattern（N）]SE，IG

≈[N]SE，IG，

即[M]SE，IG≈[N] SE，IG。

定理1得證。

參考文獻(xiàn)：

[1] 雷新鋒，宋書民，劉偉兵，等.計(jì)算可靠的密碼協(xié)議形式化分析綜述[J].計(jì)算機(jī)學(xué)報(bào)，2014，37（5）：993-1016.

[2] 付浩.基于雙線性對(duì)的蹤跡屬性計(jì)算可靠性分析[J].計(jì)算機(jī)與數(shù)字工程，2017，45（7）：1360-1365.

[3] 付浩，肖建新.基于密鑰循環(huán)的通用可復(fù)合符號(hào)分析[J].計(jì)算機(jī)與數(shù)字工程，2017，45（8）：1586-1591.

[4] Abadi M，Rogaway P.Reconciling two views of cryptography[M]//Theoretical Computer Science：Exploring New Frontiers of Theoretical Informatics.Berlin，Heidelberg：Springer Berlin Heidelberg，2000：3-22.

[5] 付瑋，劉廣亮.一種基于身份的門限盲代理盲簽名方案[J].聊城大學(xué)學(xué)報(bào)（自然科學(xué)版），2012，25（3）：85-88.

【通聯(lián)編輯：謝媛媛】