解顏銘，石曙東， 翁艷琴

(1.湖北師范學(xué)院 數(shù)學(xué)與統(tǒng)計(jì)學(xué)院， 湖北 黃石 435002；2.湖北師范學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，湖北 黃石 435002)

0 引言

隨著Internet技術(shù)的發(fā)展，電子郵件已逐漸代替?zhèn)鹘y(tǒng)的郵件得到了很廣泛的應(yīng)用?，F(xiàn)有的電子郵件系統(tǒng)不僅能夠傳送文本信息，而且可以傳送圖片、聲音和動(dòng)畫(huà)等信息，是保證商家和用戶在網(wǎng)上進(jìn)行正常電子商務(wù)活動(dòng)的基礎(chǔ)，具有保密性、安全性、認(rèn)證性、完整性以及非否認(rèn)性和公平性等重要屬性。

近年來(lái)，串空間理論[1]迅速發(fā)展，成為協(xié)議的形式化分析方法[2]的常用技術(shù)方法。認(rèn)證測(cè)試?yán)碚摲椒╗3]是通過(guò)構(gòu)造測(cè)試分量、應(yīng)用認(rèn)證測(cè)試規(guī)則、定義節(jié)點(diǎn)等方法來(lái)判斷安全協(xié)議是否能夠達(dá)到其安全目標(biāo)的一種基于串空間模型的協(xié)議的形式化分析方法。

本文對(duì)文獻(xiàn)[4]中提出的基于在線的第三方掛號(hào)電子郵件協(xié)議DKNRP進(jìn)行了分析，發(fā)現(xiàn)其存在安全缺陷，設(shè)計(jì)出了一個(gè)新的公平非否認(rèn)電子郵件協(xié)議。最后通過(guò)擴(kuò)展的串空間模型對(duì)新協(xié)議進(jìn)行了形式化的證明。

1 DKNRP協(xié)議及其缺陷分析

文獻(xiàn)[4]中提出了一個(gè)不可否認(rèn)電子郵件協(xié)議——DKNRP協(xié)議。該協(xié)議的設(shè)計(jì)目標(biāo)是能抵御常見(jiàn)的篡改和重放攻擊，并減少對(duì)可信第三方的信賴程序，保證郵件的機(jī)密性。

1.1 DKNRP協(xié)議的形式化描述

1)M1.S→R:L，S， {M}K， {{K}R}T，{L，H({M}K)，H({{K}R}T)}S-1；

2)M2.R→T:L，S，R， {{K}R}T，{L，H({M}K)，H({{K}R}T)}S-1，{L，H({M}K)}R-1;

3)M3.T→R:L，{K}R.

其中，S和R表示電子郵件發(fā)送方與接收方，T為可信的第三方。第一步，K是S隨機(jī)生成的會(huì)話密鑰。L用于惟一標(biāo)識(shí)一次會(huì)話，可以是隨機(jī)值也可以是一個(gè)時(shí)間戳。第二步，R收到S的消息后， 當(dāng)且僅當(dāng)R驗(yàn)證S的簽名{L，H({M}K)，H({{K}R}T)}S-1正確后，R才進(jìn)行步驟2)。R為了要獲得K，則必須要將{{K}R}T轉(zhuǎn)給T，同時(shí)對(duì)已驗(yàn)證通過(guò)的H({M}K)進(jìn)行數(shù)字簽名。第三步，T將雙重加密的密鑰{{K}R}T解密，因?yàn)閧{K}R}T解密后得{K}R，T沒(méi)有R的私鑰，無(wú)法解密獲得K。T將解密后的{K}R發(fā)送給R.

1.2 DKNRP協(xié)議的缺陷分析

1)信道問(wèn)題：在DKNRP協(xié)議中，沒(méi)有規(guī)定協(xié)議所使用的信道。協(xié)議主體間的信道可能是不可靠信道。設(shè)計(jì)協(xié)議時(shí)應(yīng)該明確規(guī)定協(xié)議所使用的信道，這種情況下，假設(shè)協(xié)議主體之間的信道是機(jī)密和安全的。

2)時(shí)限性問(wèn)題：在DKNRP協(xié)議中，沒(méi)有規(guī)定協(xié)議運(yùn)行的限定時(shí)間。R接收到M1后可能會(huì)故意拖延時(shí)間再把M2發(fā)給T，之后T才公布證據(jù)。但是S有可能因等待時(shí)間過(guò)長(zhǎng)而中止協(xié)議并且不會(huì)到T的ftp服務(wù)器上獲取證據(jù)。這樣對(duì)S是不公平的。一個(gè)解決辦法是在協(xié)議中加入限定時(shí)間t(表示消息在t時(shí)間內(nèi)有效)，若R同意t，協(xié)議將繼續(xù)進(jìn)行，否則協(xié)議將結(jié)束。

3)重放攻擊[5]：假設(shè)R與協(xié)議外的另一主體進(jìn)行合謀，在協(xié)議結(jié)束的時(shí)候，R收到了郵件內(nèi)容和證據(jù)，而S卻由于沒(méi)有足夠的證據(jù)而無(wú)法證實(shí)R是否真的收到了郵件。

2 一種新的電子郵件協(xié)議

2.1 針對(duì)上面分析出的安全缺陷，提出一種新的電子郵件協(xié)議，協(xié)議描述如下：

1)M1.S→R:t，S，R，{M}K， {{K}R}T，{Ns，S，R，H({M}K)，H({{K}R}T)}ks-1；

2)M2.R→T:t，S，R，{Ns，S，R，H({M}K)，H({{K}R}T)}KS-1，{Ns，NR，{{K}R}T，H({M}K)}kR-1；

3)M3.T→S: {Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1;

4)M4.T?R:{{K}R，Ns，NR}kT-1.

本協(xié)議中，第一步，S發(fā)送時(shí)間t、S、R、密文、雙重加密密鑰以及簽名給R.第二步，若R不同意最遲期限t，則終止協(xié)議，否則R將檢驗(yàn)簽名是否合法，如果合法，R將發(fā)送時(shí)間t、S的身份標(biāo)識(shí)和簽名以及自己的身份標(biāo)識(shí)和簽名給T；否則R終止協(xié)議。第三步，T首先檢驗(yàn)t，如果時(shí)間已經(jīng)過(guò)了最遲期限t，則終止協(xié)議；否則T在驗(yàn)證消息來(lái)源后，檢驗(yàn)S和R的簽名來(lái)源以及簽名消息是否一致，若正確則將R的簽名及Ns用自己的私鑰加密后發(fā)送給S，以便日后仲裁。第四步，根據(jù)文獻(xiàn)[6]中的協(xié)議思想，T?R表示R通過(guò)多次到T的 ftp 服務(wù)器上獲取證據(jù)從可信第三方T那里獲取消息。

2.2 協(xié)議的仲裁[7]

如果接收者R否認(rèn)收到報(bào)文M，發(fā)送者S可請(qǐng)求可信第三方T進(jìn)行仲裁：T首先檢查發(fā)送者S是否在公開(kāi)了{(lán){K}R}T及其簽名，若沒(méi)有則T就可以判定R沒(méi)有收到M；否則，如果T在公開(kāi)數(shù)據(jù)庫(kù)中找到了{(lán){K}R}T及其簽名，則S將K′，M′，{Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1提交給T.

如果以上兩步均成立，就可以證明R在時(shí)間t內(nèi)收到了報(bào)文M；否則就沒(méi)有收到M.

上述仲裁只在發(fā)送者和接收者發(fā)生糾紛時(shí)才執(zhí)行。

3 串空間模型及其擴(kuò)展

3.1 串空間模型相關(guān)理論[8]

定義1 符號(hào)項(xiàng)是一個(gè)二元組<σ，α>，其中α∈A且σ={+，-}，符號(hào)項(xiàng)表示為+t或-t，+t代表一個(gè)主體發(fā)送一個(gè)項(xiàng)，-t代表一個(gè)主體接收一個(gè)項(xiàng)。(±A)*是符號(hào)項(xiàng)的有限序列集，其中的元素記為<<σ1，α1>，<σ2，α2>，…，<σn，αn>>.

定義2 一個(gè)串空間是指一個(gè)集合Σ以及該集合上的跡映射:tr:Σ→(±A)*.集合Σ中的元素稱為串。項(xiàng)t起源于節(jié)點(diǎn)n∈s，當(dāng)且僅當(dāng)sign(n)=+，且t?term(n)，并且對(duì)?n′?+n，必須滿足t?term(n′).

定義3h為g的一個(gè)子項(xiàng)，即h?g.該子項(xiàng)關(guān)系用理想的概念可以等價(jià)地定義為g∈IK[h].

定義4 一個(gè)節(jié)點(diǎn)m是I?A的進(jìn)入點(diǎn)，當(dāng)且僅當(dāng)term(m)為正號(hào)，term(m)∈I，且當(dāng)m′為m在同一個(gè)串上的因果前驅(qū)時(shí)，term(m′) ?I.

定理1 假定K∈k，S?A，且對(duì)任意s∈S，s都是簡(jiǎn)單的，且s不形如{g}K.若K∈k， {h}K∈k[S]，則K∈k.

定理2 假定C為一個(gè)叢，K=S∪k-1且S∩Kp=Φ.若存在一個(gè)節(jié)點(diǎn)m∈C使得term(m)∈IK[S]，則必然存在一個(gè)正常節(jié)點(diǎn)(即非侵入節(jié)點(diǎn))n∈C使得n為IK[S]的一個(gè)進(jìn)入點(diǎn)。

定理3 假定C為一個(gè)叢，K=S∪k-1且S∩Kp=Φ，且不存在這樣的節(jié)點(diǎn)，該節(jié)點(diǎn)是屬于C的正常節(jié)點(diǎn)且是IK[S]的一個(gè)進(jìn)入點(diǎn)，則對(duì)K∈S，任何形如{g}K的消息項(xiàng)都不起源于一個(gè)侵入者串。

3.2 認(rèn)證測(cè)試?yán)碚摷捌鋽U(kuò)展

定義5 令C為一個(gè)簇，s為一個(gè)串，n1，n2∈S，則對(duì)于a∈A，若n1為負(fù)結(jié)點(diǎn)，n2為正結(jié)點(diǎn)，則

n1=>+n2是轉(zhuǎn)換邊；若n1為正結(jié)點(diǎn)，n2為負(fù)結(jié)點(diǎn)，則n1=>+n2是被轉(zhuǎn)換邊。

定義6t={|h|}K或t=HK(|h|)是a在n上的測(cè)試分量，則：

1)a?t，t是n的分量；

2)t不是任何一個(gè)正常結(jié)點(diǎn)n′子項(xiàng)，n′Σ.

如果a唯一產(chǎn)生于結(jié)點(diǎn)n0，則n0?+n1是a的測(cè)試，并且n0?+n1是a的被轉(zhuǎn)換邊。

定義7 若n0?+n1是對(duì)a的測(cè)試，且K-1?KX，則它是a在t={|h|}K或t=HK(|h|)中的出測(cè)試，其中a僅包含在n0的分量t中，t是a在n0中的測(cè)試分量。

n0?+n1是對(duì)a的測(cè)試，且K?KX，則它是a在t1={|h|}K或t1=HK(|h|)中的入測(cè)試，t1是a在n1中的測(cè)試分量。

定義8 若t={|h|}K或t=HK(|h|)是任何a在n中的測(cè)試分量，且K?KX，則負(fù)結(jié)點(diǎn)n是t的一個(gè)主動(dòng)測(cè)試。

認(rèn)證測(cè)試方法:

認(rèn)證測(cè)試規(guī)則1(出測(cè)試規(guī)則) 令C為一個(gè)簇，n′∈C，n?+n′為a在t中的出測(cè)試，則：

1)存在正常結(jié)點(diǎn)m，m′∈C，使得t是m的分量，且m?+m′是a的變換邊。

2)假設(shè)a僅存在于m′的分量t1={|h1|}K1或t1=HK1(|h1|)中，t1不是任何一個(gè)正常分量的真子集，且K1-1?KX，則存在一個(gè)負(fù)的正常結(jié)點(diǎn)，t1為該結(jié)點(diǎn)分量。

認(rèn)證測(cè)試規(guī)則2(入測(cè)試規(guī)則) 令C為一個(gè)簇，n′∈C，n?+n′為a在t′中的入測(cè)試，則存在正結(jié)點(diǎn)m，m′∈C使得t′是m′的分量且m?+m′是a的轉(zhuǎn)換邊。同上。

認(rèn)證測(cè)試規(guī)則3(主動(dòng)測(cè)試規(guī)則) 令C為一個(gè)簇，n∈C，n是t={|h|}K或t=HK(|h|)的一個(gè)主動(dòng)測(cè)試，則存在一個(gè)正結(jié)點(diǎn)m∈C，且t是m的一個(gè)分量。

4 新電子郵件協(xié)議的形式化分析

4.1 新協(xié)議的串空間模型

此協(xié)議的串空間包括發(fā)起者串 Init、響應(yīng)者串 Resp、可信第三方串和攻擊者串p的集合，可表示為Σ=Serv∪Init∪Resp∪Ρ.協(xié)議運(yùn)行過(guò)程如圖1所示：

圖1 新協(xié)議的串空間模型

1)發(fā)起者串Init[S，R，M，Ns，NR，K]=<+t，S，R，{M}K，{{K}R}T，{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1，- {Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1>，和某個(gè)s∈Init[S，R，Ns，NR，M，K]相關(guān)聯(lián)的協(xié)議主體是S.

2)響應(yīng)者串Resp[S，R，M，Ns，NR，K]=<-t，S，R，{M}K，{{K}R}T，{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1，+t，S，R，{Ns，S，R，H({M}K)，H({{K}R}T)}KS-1，{Ns，NR，{{K}R}T，H({M}K)}kR-1，- {{K}R，Ns，NR}kT-1>，和某個(gè)s∈Resp [S，R，Ns，NR，M，K]相關(guān)聯(lián)的協(xié)議主體是R.

3)可信第三方串Serv[S，R，M，Ns，NR，K]=<-t，S，R，{Ns，S，R，H({M}K)，H({{K}R}T)}KS-1，{Ns，NR，{{K}R}T，H({M}K)}kR-1，+{Ns，{Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1，+ {{K}R，Ns，NR}kT-1>，和某個(gè)s∈Serv [S，R，Ns，NR，M，K]相關(guān)聯(lián)的協(xié)議主體是T.

4.2 新協(xié)議認(rèn)證性分析

設(shè)有如下基本假設(shè):1)kS-1，kR-1，kT-1?Kp；2)Ns，NR以及H({M})K唯一產(chǎn)生；3)Ns≠NR.

首先證明發(fā)起者S能夠驗(yàn)證響應(yīng)者R.驗(yàn)證過(guò)程如下：

1)構(gòu)造測(cè)試分量。發(fā)起者串Init[S，R，M，Ns，NR，K]，由于Ns唯一產(chǎn)生于結(jié)點(diǎn)L0，因此{(lán)Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1是Ns的測(cè)試分量，L0?+L1構(gòu)造了Ns在{Ns，{Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1中的輸入測(cè)試。

2)應(yīng)用認(rèn)證測(cè)試規(guī)則2:存在正常結(jié)點(diǎn)m，m′∈C，{Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1是結(jié)點(diǎn)m′的分量，并且m?+m′是NR的轉(zhuǎn)換邊。

4)比較串的內(nèi)容。比較term(m′)和服務(wù)者串中相應(yīng)的測(cè)試分量，可以得到S=S′，R=R′，M=M′，Ns=Ns′，NR=NR′，K=K′，那么服務(wù)者串S= Serv[S，R，M，Ns，NR，K].

5)構(gòu)造測(cè)試分量。由4)可知{Ns，NR，{{K}R}T，H({M}K)}kR-1是結(jié)點(diǎn)L0的分量，所以結(jié)點(diǎn)L0是{Ns，NR，{{K}R}T，H({M}K)}kR-1關(guān)于H({M}K)的一個(gè)主動(dòng)測(cè)試。

6)根據(jù)認(rèn)證測(cè)試規(guī)定3:存在正常結(jié)點(diǎn)n∈C并且{Ns，NR，{{K}R}T，H({M}K)}kR-1是結(jié)點(diǎn)n的分量。

7)定義結(jié)點(diǎn)n.由6)可知n為某個(gè)響應(yīng)者串S″中的結(jié)點(diǎn)，設(shè)s″=Resp[S″，R″，M″，Ns″，NR″，K″]，{Ns，NR，{{K}R}T，H({M}K)}kR-1是結(jié)點(diǎn)n的分量。

8) 比較串的內(nèi)容。比較term(n)和響應(yīng)者串中相應(yīng)的測(cè)試分量，得到S=S′，R=R′，M=M′，Ns=Ns′，NR=NR′，K=K′，那么響應(yīng)者串S=Resp[S，R，M，Ns，NR，K].

從以上分析可以得到，由發(fā)起者串Init[S，R，M，Ns，NR，K]可以得到服務(wù)者串S= Serv[S，R，M，Ns，NR，K]和響應(yīng)者串s= Resp[S，R，M，Ns，NR，K]，服務(wù)者串和響應(yīng)者串的參數(shù)一致且都收到Ns、NR和K，那么S能夠有效的認(rèn)證R和T并且S認(rèn)為R收到密鑰K.

隨后證明響應(yīng)者R能夠驗(yàn)證發(fā)起者S.

1)構(gòu)造測(cè)試分量。響應(yīng)者串Resp[S，R，M，Ns，NR，K]，由于NR唯一產(chǎn)生于結(jié)點(diǎn)m2，因此{(lán){K}R，

Ns，NR}kT-1是NR的測(cè)試分量，結(jié)點(diǎn)m2是{{K}R，Ns，NR}kT-1關(guān)于NR的一個(gè)主動(dòng)測(cè)試。

2)根據(jù)認(rèn)證測(cè)試規(guī)則3：存在正常結(jié)點(diǎn)n∈C并且{{K}R，Ns，NR}kT-1是結(jié)點(diǎn)n的分量。

4)比較串的內(nèi)容。比較term(m′)和服務(wù)者串中相應(yīng)的分量，可以得到S=S′，R=R′，Ns=Ns′，NR=NR′，K=K′，那么服務(wù)者串S= Serv[S，R，*，Ns，NR，K].

5)構(gòu)造測(cè)試分量。{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1是結(jié)點(diǎn)m0的分量，所以結(jié)點(diǎn)m0是{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1關(guān)于H({M}K)的一個(gè)主動(dòng)測(cè)試。

6)根據(jù)認(rèn)證測(cè)試規(guī)則3:存在正常結(jié)點(diǎn)n∈C并且{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1是結(jié)點(diǎn)n的分量。

7)定義結(jié)點(diǎn)n.由6)可知n為某個(gè)發(fā)起者串S″中的結(jié)點(diǎn)，s″=Init[S″，R″，M″，Ns″，NR″，K″]，{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1是結(jié)點(diǎn)n的分量。

8)比較串的內(nèi)容。比較term(n)和發(fā)起者串中相應(yīng)的分量，可以得到S=S′，R=R′，M=M′，Ns=Ns′，K=K′，那么發(fā)起者串S=Init[S，R，M，Ns，*，K].

從以上分析可以得到，由響應(yīng)者串Resp[S，R，M，Ns，NR，K]可以得到服務(wù)者串S= Serv[S，R，*，Ns，NR，K]和發(fā)起者串S=Init[S，R，M，Ns，*，K]，服務(wù)者串和起者串的參數(shù)一致，都有S，R和K，所以R能夠有效的認(rèn)證S和T.

4.3 新協(xié)議秘密性分析

定理5 假定C是∑中的一個(gè)叢，S，R∈Tname；K是唯一起源的，kS-1，kR-1，kT-1?KP.令S={K，kS-1，kR-1，kT-1}，k=kS.則對(duì)每個(gè)結(jié)點(diǎn)m∈C，term(m)?Ik[K].

證明：證明一個(gè)更強(qiáng)的命題：對(duì)任意結(jié)點(diǎn)m∈C，term(m)?Ik[S].因?yàn)镾∩Kp=φ，k=k-1，且k=k∪S.由定理2可知，只需證明：不存在正則結(jié)點(diǎn)m且m是的Ik[S]的入口點(diǎn)。

運(yùn)用反證法：設(shè)正則結(jié)點(diǎn)m是Ik[S]的入口點(diǎn)，則term(m)?Ik[S]，由定理1和定義3知，K，kS-1，kR-1，kT-1中的某一個(gè)是 term (m) 的子項(xiàng)，而kS-1，kR-1，kT-1并不是任何結(jié)點(diǎn)消息項(xiàng)的子項(xiàng)，故K是term(m) 的子項(xiàng)。若m是一個(gè)正則串s上的一個(gè)符號(hào)為正的正則結(jié)點(diǎn)，若是一個(gè)正則K∈term(m)串上的一個(gè)符號(hào)為正的正則結(jié)點(diǎn)，則意味著：

1)s∈Init且m=；

2)s∈Resp且m=；

3)s∈Serv且m= 或m=.

情形1)，由于K是唯一起源的，故s∈Sinit，所以term (m)=t，Ns，NR，{M}K， {{K}R}T，{Ns，NR，H({M}K)，H({{K}R}T)}kS-1，term (m)∈Ik[S]，由定義1和定理1可知t，Ns，NR，{M}K?k[S]且{M}K， {{K}R}T，{Ns，NR，H({M}K)，H({{K}R}T)}kS-1?Ik[S]，所以情況不成立。

同理，對(duì)于情形2)和情形3)，情況均不成立。

因此，假設(shè)不成立，命題得證。

5 結(jié)束語(yǔ)

本文對(duì)DKNRP協(xié)議進(jìn)行了分析，在前人研究的基礎(chǔ)上指出其設(shè)計(jì)不足之處，并給出了一個(gè)新的公平非否認(rèn)電子郵件協(xié)議。文章基于擴(kuò)展的串空間模型和認(rèn)證測(cè)試方法，對(duì)該新的電子郵件協(xié)議進(jìn)行了形式化分析證明，分析的結(jié)果表明該新郵件協(xié)議能夠?qū)崿F(xiàn)協(xié)議發(fā)起者和響應(yīng)者的雙向身份認(rèn)證，即滿足其安全目標(biāo)。新協(xié)議具有保密性、安全性、認(rèn)證性、完整性以及非否認(rèn)性和公平性，滿足了電子郵件的特性，是可以用的。

[1]Garher L.Denia-of-Servic Attacks Rip the Internet[J].Computer，2000，33(4):12～17.

[2]薛 銳.安全協(xié)議的形式化分析方法及其發(fā)展現(xiàn)狀[M].成都：電子工業(yè)出版社，2009.

[3]Guttman JD，F(xiàn)dbrega FJT.Authentieation tests and the strueture of bundles[J].Theoretical Computer Science，2002，255(2):333～380.

[4]彭紅艷，李肖堅(jiān)，夏春和，等.一種面向電子郵件的不可否認(rèn)協(xié)議及其形式化分析[J].計(jì)算機(jī)研究與發(fā)展， 2006， 43 (11):1914～1919.

[5]王 潔.公平不可否認(rèn)協(xié)議設(shè)計(jì)及其形式化分析[D].重慶：重慶大學(xué)，2008.

[6]蔡永泉，朱 勇.Zhou-Gollmann非否認(rèn)協(xié)議的分析與改進(jìn)[J].計(jì)算機(jī)應(yīng)用研究，2007:24(7):222～245.

[7]趙自強(qiáng).基于串空間模型的形式化方法的擴(kuò)展與應(yīng)用[D].成都：成都理工大學(xué)，2011.

[8]解顏銘，石曙東，翁艷琴.CCITT X.509協(xié)議的形式化分析及其改進(jìn)[J].計(jì)算機(jī)安全，2012，6:50～53.

[9]方燕萍.串空間模型及其認(rèn)證測(cè)試方法的擴(kuò)展與應(yīng)用[D].蘇州：蘇州大學(xué)，2009.

[10]李廷元，秦志光，劉曉東，等.Needham-Schroeder協(xié)議的認(rèn)證測(cè)試方法形式化分析[J].計(jì)算機(jī)工程與應(yīng)用，2010，46(19):100～102.