一种新的电子邮件协议及其形式化分析

解颜铭，石曙东， 翁艳琴

(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.