潘　进, 王小明, 谢青松

(1.西安通信学院 信息安全系, 陕西 西安 710106;　2.西安通信学院 12队, 陕西 西安 710106)

WTLS握手协议后向安全性分析及改进

潘进1, 王小明2, 谢青松1

(1.西安通信学院 信息安全系, 陕西 西安 710106;2.西安通信学院 12队, 陕西 西安 710106)

摘要:通过应用π演算建模分析WTLS握手协议，得出其存在密钥泄露的缺陷，并加以改进。在密钥协商过程中使用幂运算处理随机数，并用RSA加密算法对所建立的预主密钥进行加密，以确保在私钥泄露的情况下，攻击者无法获取以后的会话密钥。利用ProVerif工具对改进后的WTLS握手协议进行验证，结果显示其满足后向安全性。

关键词:应用π演算；WTLS握手协议；后向安全性；ProVerif

实际应用的密钥交换协议，如IPSec中的IKEv2、802.11和TLS，在建立会话中都涉及到密钥交换过程,往往要求满足一定的安全属性。无线传输层安全(WirelessTransportLayerSecurity,WTLS)协议是确保无线网络通信的重要环节，其密钥交换过程起着至关重要的作用。

分析WTLS握手协议的密钥交换过程可知：WTLS握手协议容易遭到DoS攻击并存在密钥生成速度慢的缺陷，采用非对称证书方式可对其加以改进[1]；WTLS握手协议存在未知密钥共享攻击和中间人攻击缺陷，基于FS-MAKEP可得一种改进方案[2]；WTLS握手协议缺乏前向安全性，基于XTR公钥密码体制可得一种改进方案[3]；WTLS握手协议服务器证书有效性验证不足，且通信中计算量大，经改进可得基于身份认证的WTLS握手协议[4]。这些改进方案改变了WTLS握手协议密钥协商的算法，但改进过程复杂且通信中计算量大，对无线通信不易实现。

为了降低无线环境中密钥协商过程需要交互的信息量[5]，一种基于ECDH的WTLS握手协议改进方案被提出，但其安全属性仍然存在问题[6]。对ECDH-WTLS握手协议和RSA-WTLS握手协议的相关改进[7]，虽然具有客户端匿名性，但针对RSA-WTLS握手协议的改进方案并不具有前向安全性[8]。

关于WTLS握手协议的前向安全性得到广泛关注，但其后向安全性并没有引起人们足够的重视。本文拟以应用π演算对WTLS协议进行建模，分析其后向安全性，找出其存在的安全性缺陷，并给出一种基于RSA加密算法的改进方案。

1基本概念与工具

1.1后向安全性

后向安全性是在分析前向安全性的基础上提出的，依据前向安全性[9]的定义，对后向安全性定义如下：如果协议参与一方或多方的长期私钥泄露，并不能泄露在此之后建立的会话密钥，则称该协议具有后向安全性。

协议一旦具备后向安全性，则在移动通信和电子商务活动中，即使攻击者得到协议参与方的长期私钥，依然不能通过长期私钥分析出参与方之后建立的会话密钥，协议仍然能够保证传输信息的安全性。

1.2应用π演算

应用π演算[10]是在π演算基础上增加了传值、函数原语和项的代数相等关系扩展而成的。使用应用π演算形式化描述协议是分析协议安全性的一种简单、可靠的形式化分析方法[11]。

应用π演算的语法包括项和进程两部分：项通常用来描述协议参与方之间传递和处理的消息，进程通常用来描述协议参与方交换和处理消息的具体过程。不过，现有语法并不足以分析协议的后向安全性，需要对其扩展。

为区分协议的运行阶段，在应用π演算建模中使用“phase”来区分协议主进程中的阶段，阶段的“phase”关键字语法格式是“phaset;P”，表示先执行阶段“phaset”，再执行进程P。其中，t是一个整数，代表全局时钟。阶段进程的执行过程如下。

首先，执行0阶段下的所有指令，即不在i≥1阶段的所有指令。然后，在0阶段到1阶段的过渡阶段，所有没有达到i≥1阶段的所有进程被丢弃，并且进程执行1阶段的指令，但不是i≥2阶段的。更一般地，当从n阶段到n+1阶段转换时，所有没有达到n+1阶段进程都被丢弃，并且执行n+1阶段而不是i≥n+2阶段的指令。

阶段进程的特点是：进程phaset只在t阶段是活跃的；只有在相同阶段的进程才能通信；在阶段的转换过程中，攻击者保持了它的攻击能力。

1.3ProVerif分析工具

协议形式化分析工具ProVerif[12]是基于Horn逻辑程序开发的,能够验证使用应用π演算描述的密码协议，并能够描述各种密码学原语。这包括共享密钥密码学，公钥密钥密码学，数字签名，Hash函数和Diffie-Hellman密钥交换协议等。

使用ProVerif工具分析协议的安全属性时，将基于应用π演算编写的使用各种密码学原语建立的协议模型自动翻译成基于Horn逻辑的模型，然后依据协议的Horn逻辑模型进行逻辑推导，并给出验证的结果。当不满足某个属性时，会给出攻击序列。ProVerif工具是一种有效的形式化验证工具。

2WTLS握手协议分析

2.1WTLS握手协议建模

在使用应用π演算对WTLS握手协议建模之前，需要对协议的交互过程进行抽象[13]。协议抽象后的交互过程可描述如

MSG1C→S: NC,

MSG2S→C: NS,CertS,CertREQ,

MSG3C→S:CertC,{H(Mess, NC,NS,

MSG4S→C: {H(Mess, NC, NS,MS)}KCS。

用协商好的对称密钥KCS对消息进行加密，双方可验证内容的正确性，表述为

{H(Mess, NC, NS,MS)}KCS。

其中， NI为实体I生成的随机数；CertI为实体I的证书；KCS为客户端与服务器建立的会话密钥；H为哈希函数。

基于上述抽象过程，首先需要建立可信机构TA颁发数字证书的进程宏，以及客户端和服务器的进程宏。

可信机构TA的进程宏为

letTA(skTA:sskey,pkC:pkey,pkS:pkey)=

letCertC=cert(idC,pkC,skTA)inout(c1,CertC);

letCertS=cert(idS,pkS,skTA)inout(c2,CertS).

客户端的进程宏clientC为

letclientC(skC:skey,pkC:pkey,pkTA:spkey)=

in(c1,CertX:bitstring);

newnc:bitstring;

out(c,nc);

in(c, (nx:bitstring,xCertS:bitstring));

ifcheckcert(xCertS,pkTA)=idSthen

evertbeginC(nx,xCertS);

letpkX:pkey=getcert(xCertS,pkTA)in

letkPMS=com(skC,pkX)in

letkMS:key=f(kPMS,(nc,nx))in

letkCS:key=f(kMS,(nc,nx))in

out(c,(CertX,sign(H((m,nc,nx,kMS)),

skey_to_sskey(skC)),

senc(H((m,nc,nx,kMS)),kCS)));

in(c,z:bitstring);

ifsdec(z,kCS)=H((m,nc,nx,kMS))then

eventendC(kCS);

out(c,senc(s,kCS)).

服务器的进程宏serverS为

letserverS(skS:skey,pkS:pkey,pkTA:spkey)=

in(c2,CertY:bitstring);

in(c,ny:bitstring);

eventbeginS(ny);

newns:bitstring;

out(c,(ns,CertY));

in(c,(xCertC:bitstring,

z:bitstring,q:bitstring));

ifcheckcert(xCertC,pkTA)=idCthen

letpkY:pkey=getcert(xCertC,pkTA)in

letkPMS=com(skS,pkY)in

letKMS:key=f(kPMS,(ny,ns))in

letkCS:key=f(kMS,(ny,ns))in

ifH((m,ny,ns,kMS))=

checksign(z,pkey_to_spkey(pkY))then

ifsdec(q,kCS)=H((m,ny,ns,kMS))then

eventendS(kCS);

out(c,senc(H((m,ny,ns,kMS)),kCS));

in(c,y:bitstring);

letmx=sdec(y,kCS)in

0.

协议的主进程由可信机构TA以及客户端和服务器的进程宏并发形成,即

process

newskC:skey;

newskS:skey;

letpkC=ec(skC,p)inout(c,pkC);

letpkS=ec(skS,p)inout(c,pkS);

newskTA:sskey;

letpkTA=spk(skTA)inout(c,pkTA);

(

out(c,skI)|phase1;

(!TA(skTA,pkC,pkS))|

(!clientC(skC,pkC,pkTA))|

(!serverS(skS,pkS,pkTA))

)

2.2WTLS握手协议分析

ProVerif可证明可达性、对应性断言和观察等价，进而通过查询语句来分析协议的秘密性和后向安全性。根据后向安全性的定义可知，协议满足后向安全性的前提是协议首先能够保证会话密钥的秘密性。只有在证明协议满足会话密钥的秘密性后，才能分析协议是否满足后向安全性。

定义1(秘密性)如果M为协议的一个基本项，输入查询语句

queryattacker(M)，

其输出结果为

notattacker(M)istrue，

则称协议保证项M具备秘密性。

attacker(M)表示攻击者能够获取项M。ProVerif工具允许研究查询攻击者能够获得哪些项，如果攻击者不能获取项M，那么协议就保证了项M的秘密性。

定义2(后向安全性)假设A和B为密钥交换协议的参与方，skA和skB分别为A和B的长期私钥，A(M1, M2,…, Mn)和B(M1, M2,…, Mm) 分别为描述A和B的进程宏，k为运行协议所建立的会话密钥,且具备秘密性。将协议的主进程改为

out(c,skI)|phase1;

A(M1, M2,…,Mn)|

B(M1,M2,…, Mm)，

并输入查询语句

queryattacker(k)。

若在I=A,B两种情况下，输出结果都为

notattacker_p1(k)istrue，

则称协议具有后向安全性。

修改后的主进程表示在0阶段协议参与方的私钥泄露后，在1阶段再运行协议。若攻击者在1阶段不能获取k，协议自然满足后向安全性。

2.3WTLS握手协议验证

使用形式化验证工具ProVerif对协议秘密性和后向安全性进行验证。

(1) 秘密性验证

WTLS握手协议建立了会话密钥kCS，协议需要保证会话密钥的秘密性。当s为秘密信息，攻击者无法获取通过会话密钥kCS加密后传输的秘密信息s时，则WTLS握手协议具有秘密性。在用ProVerif工具分析时，通过查询语句

queryattacker(s)

能够进行WTLS握手协议的秘密性分析。

ProVerif的输出如图1所示，ProVerif的验证结果为

notattackers(k)istrue.

这表明攻击者无法获取双方协商出的会话密钥kCS，WTLS握手协议满足秘密性。

图1　秘密性分析结果

(2) 后向安全性验证

由后向安全性定义可知无论密钥的哪一方在阶段0泄露了密钥，在阶段1都不会泄露密钥，则说明该协议满足后向安全性。协议在阶段1的运行结果如图2所示，ProVerif的输出为

notattacker_p1s(k)isfalse.

这表明WTLS握手协议不满足后向安全性。

图2　后向安全性分析结果

3WTLS握手协议的改进及验证

3.1改进后的WTLS握手协议建模

参考基于RSA的WTLS握手协议改进方案[7-8]，在密钥协商过程初始建立会话中使用D-H密钥交换协议对随机数进行一次加密处理，再在握手的第3步消息中使用RSA加密算法对所建立的预主密钥进行加密传输，由此确保即使密钥泄露，攻击者也无法获取以后的会话密钥。

对改进后的WTLS握手协议进行建模，其具体交互过程可描述如下。

(1) 客户端发送ClientHello消息。为了方便分析协议的安全性，此处略去与协议安全性无关的协议版本号等信息，则消息的内容为gNC，其中NC为客户端选择的随机数，且2≤NC≤p-2。

(2) 服务器回应一个ServerHello消息，包括gNS和哈希值H(gNS‖(gNC)skS)。其中NS为服务器选择的随机数，且2≤NS≤p-2；哈希值用来认证服务器。然后，服务器发送自己的证书，CertificateRequest消息和ServerHelloDone消息。

kMS=H(gNCNS‖kPMS)。

然后，客户端发送ClientKeyExchange消息，内容为用服务器RSA公钥加密的预主密钥AencS(kPMS)；客户端发送CertificateVerify消息，内容为用计算出的主密钥加密客户端证书及用来校验证书的签名信息，即

c=SenckM(CertC,SignC(H(m,

NC,NS,kMS)))。

(4) 服务器收到客户端发来的消息后，用RSA私钥解密AencS(kPMS),得到预主密钥kPMS，再计算主密钥

kMS=H(gNCNS‖kPMS)。

用主密钥解密信息c，即

DenckM(c)=CertC‖SignC(H(m)),

得到客户端的证书CertC及其签名信息

SignC(H(m,NC,NS,kMS)),

服务器验证证书及签名信息。

(5)客户端和服务器相互发送ChangeCipherSpec消息和Finished消息，握手结束，开始应用数据的交换。

通过以上描述，协议可抽象为4条消息，即

MSG1C→S:gNC,

MSG2S→C:gNS,H(gNS‖(gNC)skS),

CertS,CertREQ,

MSG3C→S:AencS(kPMS),SenckMS(CertC,

SignC(H(m,kMS))),

SenckCS(H(m,kMS)),

MSG4S→C:SenckCS(H(m,kMS))。

据此抽象交互过程，改进后的WTLS握手协议的系统进程由客户端进程clientC、服务器进程serverS以及颁发证书的可信机构进程TA并发组成。

基于应用π演算建立客户端、服务器和可信机构TA的进程宏。客户端的进程宏clientC为

letclientC(pkC:g,skC:exponent,pkTA:spkey)=

in(c1,CertX:bitstring):

newnc:exponent:out(c,exp(g,nc));

in(c,(gx:g,hx:bitstring,xCertS:bitstring));

ifcheckcert(xCertS,pkTA)=idSthen

letpkX:G=getcert(xCertS,pkTA)in

ifhx=H((gx,exp(pkX,nc)))then

letkMS:key=bitstring_to_key(H((exp(gx,

nc),kPMS)))in

letkCS:key=bitstring_to_key(H((exp(gx,

nc),kMS)))in

out(c,((aenc(kPMS,G_to_pkey(pkX)),

senc((CertX,sign(H((m,kMS)),

exponent_to_sskey(skC))),kMS)),

senc(H((m,kMS)),kCS)));

in(c,y:bitstring);

fisdec(y,kCS)=H((m,kMS))then

out(c,senc(s,kCS)).

服务器的进程宏serverS为

letserverS(pkS:G,skS:exponent,pkTA:spkey)=

in(c2,CertY:bitstring);

in(c,gy:G);

newns:exponent;

out(c,(exp(g,ns),H((exp(g,ns),

exp(gy,skS))),CertY));

in(c,(y:bitstring,x:bitstring,q:bitstring));

letXPMS:bitstring=adec(y,

exponent_to_skey(skS))in

letkMS:key=bitstring_to_key(H((exp(gy,

ns),XPMS)))in

letkCS:key=bitstring_to_key(H((exp(gy,

ns),kMS)))in

let(xCertC:bitstring,z:bitstring)=idCthen

letpkY:G=getcert(xCertC,pkTA)in

ifH((m,kMS))=checksign(z,

G_to_spkey(pkY))then

ifsdec(q,kCS)=H((m,kMS))then

out(c,senc(H((m,kMS)),kMS));

in(c,mx:bitstring);

letmy=sdec(mx,kCS)in

0.

协议的主进程由可信机构TA以及客户端和服务器的进程宏并发形成,即

process

newskC:exponent;

letpkC=exp(g,skC)inout(c,pkC);

newskS:exponent;

letpkS=exp(g,skS)inout(c,pkS);

newskTA:sskey,letpkTA=spk(skTA)inout(c,pkTA);

(

out(c,skI)|phase1;

(!TA(skTA,pkC,pkS))|

(!clientC(pkC,skC,kpTA))|

(!serverS(pkS,skS,pkTA))

)

其中TA为可信机构，进程宏表示为

letTA(skTA:sskey,pkC:pkey,pkS:pkey)=

letCertC=cert(idC,pkC,skTA)

inout(c1,CertC);

letCertS=cert(idS,pkS,skTA)

inout(c2,CertS).

3.2改进后的WTLS握手协议验证

改进前后WTLS协议的分析过程类似，现使用ProVerif工具对改进后协议的密码性和后向安全性进行验证。

(1) 秘密性验证

用ProVerif工具通过查询语句

queryattacker(s)

对改进后协议会话密钥的秘密性进行验证，如图3所示，ProVerif的验证结果为

notattackers(k)istrue.

这表明攻击者无法获取双方协商出的会话密钥kCS，改进后的WTLS握手协议的会话密钥满足秘密性。

图3　改进后协议秘密性验证结果

(2) 后向安全性验证

在满足秘密性的条件下，使用后向安全性定义，在描述协议的主进程

(!TA(skTA,pkC,pkS))|

(!clientC(pkC,skC,pkTA))|

(!serverS(pkS,skS,pkTA))

中加入阶段进程

out(c,skC) |phase1；

(out(c,skS) |phase1；)

对修改后的协议进行验证。会话密钥满足秘密性，这里只需验证私钥泄露1阶段时，会话密钥是否泄漏，为此，只需在ProVerif中输入查询语句

queryattacker(s)phase1

进行验证。如图4所示，ProVerif的验证结果为

notattacker_p1s(k)istrue.

这表明客户端长期私钥泄露时，协议之后建立的会话密钥kCS不会泄露。改进后的WTLS握手协议在客户端满足后向安全性。

图4　客户端私钥泄露时的验证结果

对服务器私钥泄露时的后向安全性进行验证，结果如图5所示,ProVerif的验证结果为

notattacker_p1s(k)istrue.

这表明服务器端长期私钥泄露时，协议之后建立的会话密钥kCS不会泄露。改进后的WTLS握手协议在服务器端满足后向安全性。

图5　服务器私钥泄露时的验证结果

对客户端和服务器双向私钥泄露时的后向安全性进行验证，结果如图6所示。ProVerif的验证结果为

notattacker_p1s(k)istrue.

这表明攻击者同时获取客户端和服务器的长期私钥时，也不能获取之后建立的会话密钥。改进后的WTLS握手协议在客户端和服务器双向私钥泄露时也满足后向安全性。

图6　双向私钥泄露时的验证结果

综上，改进后的WTLS握手协议能够满足秘密性及后向安全性。另外，由于客户端的数字证书是通过主密钥加密后再传输的，协议还能够抵抗未知密钥共享攻击和中间人攻击。

4结语

以应用π演算对WTLS协议进行建模并用ProVerif工具对其安全属性进行验证，结果表明WTLS握手协议的会话密钥满足秘密性，但协议并不满足后向安全性。借鉴D-H密钥交换协议处理方式对产生的随机数进行处理，并以RSA加密算法对客户端预主密钥进行加密传输，由此对基于RSA的WTLS握手协议所作的进一步改进，保证了即使长期私钥泄露，攻击者也无法获取会话密钥。对改进后WTLS握手协议进行验证，结果表明其满足后向安全性要求。

参考文献

[1]杨兰荣.移动商务端到端安全的关键技术研究[D].镇江:江苏大学, 2009:15.

[2]何毅俊,李杰,徐楠.提供前向保密性的无线交换和双向认证协议[J].计算机应用, 2007, 27(7): 1603-1605.

[3]李彬,王新梅.一种实用的WTLS握手协议[J]. 西北大学学报：自然科学版,2007,37(6): 977-981.

[4]谌双双,陈泽茂,王浩.基于身份的无线传输层安全握手协议改进方案[J].计算机应用,2011,31(11):2954-2956.

[5]邹学强,冯登国.WTLS握手协议的安全性分析及改进[J].中国科学院研究生院学报,2004, 21(4): 494-500.

[6]顾香.基于应用Pi演算的安全协议形式化分析[D].西安:西安通信学院, 2015:36-54.

[7]KwakDJ，HAJC，LEEHJ,etal.AWTLSHandshakeprotocolwithuseranonymityandforwardsecrecy[C]//MobileCommunications: 7thCDMAInternationalConference,CIC2002Seoul,Korea,October29 -November1, 2002RevisedPapers.BerlinHeidelberg:Springer-Verlag,2003: 219-230.DOI:10.1007/3-540-36555-9_23.

[8]崔媛媛,周永彬,丁金扣.一种具有用户匿名性和前向安全性的WTLS握手协议的安全性分析及其改进[J].高技术通讯,2005,15(4): 6-10.

[9]李强,冯登国,张立武.标准模型下增强的基于属性的认证密钥协商协议[J].计算机学报,2013,36(10):2156-2167.

[10]ABADIM,FOURNETC.MobileValues,NewNamesandSecureCommunication[C]//POPL’01Proceedingsofthe28thACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages.NewYork:ACM, 2001:104-115.DOI: 10.1145/373243.360213.

[11]MilnerR.CommunicatingandMobileSystems:Theπ-Calculus[M].Cambridge:CambridgeUniversityPress, 1999:1-161.

[12]ABADIM，BLANCHETB.AnalyzingSecurityProtocolswithSecrecyTypesandLogicPrograms[C]//POPL’02Proceedingsofthe29thACMSIGPLAN-SIGACTsymposiumonPrinciplesofprogramminglanguages.NewYork:ACM, 2002:33-44.DOI: 10.1145/503272.503277.

[13] 潘进,顾香,王小明.基于应用Pi演算的WTLS握手协议安全性分析[J].西安邮电大学学报,2015,20(2):26-31.

[责任编辑:瑞金]

Back-securityanalysisandimprovementontheWTLShandshakeprotocol

PANJin1,WANGXiaoming2,XIEQingsong1

(1.DepartmentofInformationSecurity,Xi’anCommunicationsInstitute,Xi’an710106,China；2.Teamof12th,Xi’anCommunicationsInstitute,Xi’an710106,China)

Abstract:the WTLS handshake protocol has a defect of key leakage by the application of modeling and analysis based on the applied-π calculus. It is to ensure that when the keys leaked, the attackers cannot obtain the posteriori session keys by using the power to deal with the random number in both keys negotiation process and using RSA encryption algorithm to encrypt the transmission of the established preliminary master key. Using ProVerif to validate the improved WTLS handshake protocol, and the result shows that it has backward security.

Keywords:applied π calculus, WTLS handshaking protocol, backward security, ProVerif

doi:10.13682/j.issn.2095-6533.2016.01.005

收稿日期：2015-10-10

基金项目：国家自然科学基金资助项目(61305083)

作者简介：潘 进(1959-)，男，博士，教授，博导，从事网络安全研究。E-mail:2373242787@qq.com 王小明(1982-)，男，硕士研究生，研究方向为网络安全与防护。E-mail:279804359@qq.com

中图分类号：TP393

文献标识码：A

文章编号：2095-6533(2016)01-0025-08