一種新的電子郵件協議及其形式化分析

解顏銘，石曙東， 翁艷琴

(1.湖北師范學院 數學與統計學院， 湖北 黃石 435002；2.湖北師范學院 計算機科學與技術學院，湖北 黃石 435002)

0 引言

隨著Internet技術的發展，電子郵件已逐漸代替傳統的郵件得到了很廣泛的應用。現有的電子郵件系統不僅能夠傳送文本信息，而且可以傳送圖片、聲音和動畫等信息，是保證商家和用戶在網上進行正常電子商務活動的基礎，具有保密性、安全性、認證性、完整性以及非否認性和公平性等重要屬性。

近年來，串空間理論[1]迅速發展，成為協議的形式化分析方法[2]的常用技術方法。認證測試理論方法[3]是通過構造測試分量、應用認證測試規則、定義節點等方法來判斷安全協議是否能夠達到其安全目標的一種基于串空間模型的協議的形式化分析方法。

本文對文獻[4]中提出的基于在線的第三方掛號電子郵件協議DKNRP進行了分析，發現其存在安全缺陷，設計出了一個新的公平非否認電子郵件協議。最后通過擴展的串空間模型對新協議進行了形式化的證明。

1 DKNRP協議及其缺陷分析

文獻[4]中提出了一個不可否認電子郵件協議——DKNRP協議。該協議的設計目標是能抵御常見的篡改和重放攻擊，并減少對可信第三方的信賴程序，保證郵件的機密性。

1.1 DKNRP協議的形式化描述

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表示電子郵件發送方與接收方，T為可信的第三方。第一步，K是S隨機生成的會話密鑰。L用于惟一標識一次會話，可以是隨機值也可以是一個時間戳。第二步，R收到S的消息后， 當且僅當R驗證S的簽名{L，H({M}K)，H({{K}R}T)}S-1正確后，R才進行步驟2)。R為了要獲得K，則必須要將{{K}R}T轉給T，同時對已驗證通過的H({M}K)進行數字簽名。第三步，T將雙重加密的密鑰{{K}R}T解密，因為{{K}R}T解密后得{K}R，T沒有R的私鑰，無法解密獲得K。T將解密后的{K}R發送給R.

1.2 DKNRP協議的缺陷分析

1)信道問題：在DKNRP協議中，沒有規定協議所使用的信道。協議主體間的信道可能是不可靠信道。設計協議時應該明確規定協議所使用的信道，這種情況下，假設協議主體之間的信道是機密和安全的。

2)時限性問題：在DKNRP協議中，沒有規定協議運行的限定時間。R接收到M1后可能會故意拖延時間再把M2發給T，之后T才公布證據。但是S有可能因等待時間過長而中止協議并且不會到T的ftp服務器上獲取證據。這樣對S是不公平的。一個解決辦法是在協議中加入限定時間t(表示消息在t時間內有效)，若R同意t，協議將繼續進行，否則協議將結束。

3)重放攻擊[5]：假設R與協議外的另一主體進行合謀，在協議結束的時候，R收到了郵件內容和證據，而S卻由于沒有足夠的證據而無法證實R是否真的收到了郵件。

2 一種新的電子郵件協議

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

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.

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

2.2 協議的仲裁[7]

如果接收者R否認收到報文M，發送者S可請求可信第三方T進行仲裁：T首先檢查發送者S是否在公開了{{K}R}T及其簽名，若沒有則T就可以判定R沒有收到M；否則，如果T在公開數據庫中找到了{{K}R}T及其簽名，則S將K′，M′，{Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1提交給T.

如果以上兩步均成立，就可以證明R在時間t內收到了報文M；否則就沒有收到M.

上述仲裁只在發送者和接收者發生糾紛時才執行。

3 串空間模型及其擴展

3.1 串空間模型相關理論[8]

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

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

定義3h為g的一個子項，即h?g.該子項關系用理想的概念可以等價地定義為g∈IK[h].

定義4 一個節點m是I?A的進入點，當且僅當term(m)為正號，term(m)∈I，且當m′為m在同一個串上的因果前驅時，term(m′) ?I.

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

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

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

3.2 認證測試理論及其擴展

定義5 令C為一個簇，s為一個串，n1，n2∈S，則對于a∈A，若n1為負結點，n2為正結點，則

n1=>+n2是轉換邊；若n1為正結點，n2為負結點，則n1=>+n2是被轉換邊。

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

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

2)t不是任何一個正常結點n′子項，n′Σ.

如果a唯一產生于結點n0，則n0?+n1是a的測試，并且n0?+n1是a的被轉換邊。

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

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

定義8 若t={|h|}K或t=HK(|h|)是任何a在n中的測試分量，且K?KX，則負結點n是t的一個主動測試。

認證測試方法:

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

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

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

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

認證測試規則3(主動測試規則) 令C為一個簇，n∈C，n是t={|h|}K或t=HK(|h|)的一個主動測試，則存在一個正結點m∈C，且t是m的一個分量。

4 新電子郵件協議的形式化分析

4.1 新協議的串空間模型

此協議的串空間包括發起者串 Init、響應者串 Resp、可信第三方串和攻擊者串p的集合，可表示為Σ=Serv∪Init∪Resp∪Ρ.協議運行過程如圖1所示：

圖1 新協議的串空間模型

1)發起者串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>，和某個s∈Init[S，R，Ns，NR，M，K]相關聯的協議主體是S.

2)響應者串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>，和某個s∈Resp [S，R，Ns，NR，M，K]相關聯的協議主體是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>，和某個s∈Serv [S，R，Ns，NR，M，K]相關聯的協議主體是T.

4.2 新協議認證性分析

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

首先證明發起者S能夠驗證響應者R.驗證過程如下：

1)構造測試分量。發起者串Init[S，R，M，Ns，NR，K]，由于Ns唯一產生于結點L0，因此{Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1是Ns的測試分量，L0?+L1構造了Ns在{Ns，{Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1中的輸入測試。

2)應用認證測試規則2:存在正常結點m，m′∈C，{Ns， {Ns，NR，{{K}R}T，H({M}K)}kR-1}kT-1是結點m′的分量，并且m?+m′是NR的轉換邊。

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

5)構造測試分量。由4)可知{Ns，NR，{{K}R}T，H({M}K)}kR-1是結點L0的分量，所以結點L0是{Ns，NR，{{K}R}T，H({M}K)}kR-1關于H({M}K)的一個主動測試。

6)根據認證測試規定3:存在正常結點n∈C并且{Ns，NR，{{K}R}T，H({M}K)}kR-1是結點n的分量。

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

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

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

隨后證明響應者R能夠驗證發起者S.

1)構造測試分量。響應者串Resp[S，R，M，Ns，NR，K]，由于NR唯一產生于結點m2，因此{{K}R，

Ns，NR}kT-1是NR的測試分量，結點m2是{{K}R，Ns，NR}kT-1關于NR的一個主動測試。

2)根據認證測試規則3：存在正常結點n∈C并且{{K}R，Ns，NR}kT-1是結點n的分量。

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

5)構造測試分量。{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1是結點m0的分量，所以結點m0是{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1關于H({M}K)的一個主動測試。

6)根據認證測試規則3:存在正常結點n∈C并且{Ns，S，R，H({M}K)，H({{K}R}T)}kS-1是結點n的分量。

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

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

從以上分析可以得到，由響應者串Resp[S，R，M，Ns，NR，K]可以得到服務者串S= Serv[S，R，*，Ns，NR，K]和發起者串S=Init[S，R，M，Ns，*，K]，服務者串和起者串的參數一致，都有S，R和K，所以R能夠有效的認證S和T.

4.3 新協議秘密性分析

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

證明：證明一個更強的命題：對任意結點m∈C，term(m)?Ik[S].因為S∩Kp=φ，k=k-1，且k=k∪S.由定理2可知，只需證明：不存在正則結點m且m是的Ik[S]的入口點。

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

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]，所以情況不成立。

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

因此，假設不成立，命題得證。

5 結束語

本文對DKNRP協議進行了分析，在前人研究的基礎上指出其設計不足之處，并給出了一個新的公平非否認電子郵件協議。文章基于擴展的串空間模型和認證測試方法，對該新的電子郵件協議進行了形式化分析證明，分析的結果表明該新郵件協議能夠實現協議發起者和響應者的雙向身份認證，即滿足其安全目標。新協議具有保密性、安全性、認證性、完整性以及非否認性和公平性，滿足了電子郵件的特性，是可以用的。

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

[2]薛 銳.安全協議的形式化分析方法及其發展現狀[M].成都：電子工業出版社，2009.

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

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

[5]王 潔.公平不可否認協議設計及其形式化分析[D].重慶：重慶大學，2008.

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

[7]趙自強.基于串空間模型的形式化方法的擴展與應用[D].成都：成都理工大學，2011.

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

[9]方燕萍.串空間模型及其認證測試方法的擴展與應用[D].蘇州：蘇州大學，2009.

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