潘 进, 顾 香, 王小明

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

基于应用Pi演算的WTLS握手协议建模与分析

潘 进1, 顾 香2, 王小明2

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

针对WTLS握手协议中的特殊密码原语，用等值理论定义了椭圆曲线DH密钥交换原语，用可信机构颁发数字证书的方式定义了数字证书原语。并在密码原语定义的基础上建立了WTLS握手协议的形式化模型，最后用Pro Verif工具分析了协议的秘密性和认证性。结果表明WTLS握手协议满足其安全性说明。

应用Pi演算;密码原语；WTLS握手协议；Pro Verif；秘密性；认证性

随着电子政务、电子商务的兴起以及科研、教育、国防工作对网络依赖的加剧，网络安全受到广泛关注。网络通信，作为各项网络业务的基础，它的实质是协议通信，在很大程度上，协议的安全性决定着网络的安全性。为了保证网络信息的安全，需要协议具有高度的安全性。网络协议安全性分析受到了世界各国的高度重视。形式化分析方法长期以来被视为分析协议安全性的有效方法，基于应用Pi演算来描述协议，再用Pro Verif工具自动化验证协议安全属性是一种可靠简单的协议分析方法，在实践中该方法是比较精确的[1]。

应用Pi演算是在Pi演算语法的基础上增加了函数应用，是Spi演算的一般形式，它的优点是能够描述各种密码学原语，缺点是没有给定各个密码原语的具体定义，不适当的密码原语定义可能会造成验证工具分析的失败。特别是一些大型复杂协议中用到的特殊密码原语，定义起来比较复杂，如DH(Diffie-Hellman)密钥交换，椭圆曲线加密，XOR(异或)运算和数字证书等。

Kusters等将XOR运算中的一个元素考虑为常量定义了XOR原语[2]，将DH密钥交换中的指数设为常量定义了DH密钥交换原语[3]，这种方法比较繁琐，定义较复杂；文[4]和文[5]用等值理论分别定义了DH密钥交换原语，但等值理论只能处理特定的等式；文[6]用签名的方式定义了数字证书原语，但是对证书的描述不够全面。

针对WTLS握手协议中的数字证书和基于椭圆曲线的Diffie-Hellman(EC-DH)交换两种特殊的密码操作，本文根据文献[4-5]中的等值理论方法定义了EC-DH原语，用可信机构CA颁发数字证书的方式定义了数字证书原语并建立WTLS握手协议模型，最后用Pro Verif工具验证了协议的秘密性和认证性。

1 WTLS握手协议概述

WTLS协议[7]为无线传输层安全协议，它共定义了握手协议、更改密码规范协议、警告协议以及记录协议4个协议。其中WTLS握手协议主要用于协商协议版本，选择密码算法，认证通信双方的身份(可选功能)以及生成共享密钥，一个完整的握手过程如图1所示。握手过程就是建立或者恢复一个会话的过程，是WTLS协议栈中非常重要的一个协议。

图1 WTLS握手过程流程

(1)客户端发起一个新的会话，发送ClientHello消息。包括客户端生成的随机数NC，该次会话的标识符Sid，客户端所支持的密码套件列表SuiteC及压缩算法列表MethodC。

(2)服务器收到ClientHello消息后，选择其所支持的密码套件和压缩算法等，并生成随机数，发送下列消息。

•ServerHello消息：服务器生成的随机数NS，该次会话的标识符Sid，服务器从客户端发送过来的密码套件列表中选择其所支持的密码套件SuiteS，以及从客户端发送过来的压缩算法列表中选择其所支持的压缩算法MethodS。

•ServerCertificate消息：如果服务器需要被认证，服务器发送自己的证书给客户端。

•ServerKeyExchange消息：该消息仅在发送的ServerCertificate消息中没有包含足够的信息使客户端交换预主密钥时才发送，用来为客户端协商预主密钥传递密码信息。

•CertificateRequest消息：服务器发送该消息指示客户端提供其证书。

•ServerHelloDone消息：服务器Hello消息阶段的结束。

(3)客户端通过服务器发送的证书进行认证。如果认证不成功，客户端发送一个警告消息，会话无法建立。如果认证成功，客户端发送下列消息。

•ClientCertificate消息：该消息只有在服务器要求证书的情况下才发送。如果客户端没有合适的证书，也可以发送不包含证书的ClientCertificate消息。

•ClientKeyExchange消息：一般使用RSA公钥加密的方式直接传输预主密钥，或使用DH、EC-DH方法使双方商定该密钥。本文讨论使用EC-DH协商密钥的方式。

•CertificateVerify消息：用来提供显示的客户证书校验。

•ChangeCipherSpec消息：表明客户端和服务器的记录层将从预备状态转换到当前状态，以后的数据传送将采用协商好的加密算法和对称密钥KCS进行加密、计算MAC等。

•Finished消息：第一个用刚刚商定的密钥和算法进行保护的消息，用来校验密钥交换和认证过程是否成功。

(4)服务器同样也发送ChangeCipherSpec消息和Finished消息。

2 基于应用Pi演算的WTLS握手协议建模

2.1 应用Pi演算

应用Pi演算是一种新的进程演算理论，它的语法包括项和进程两部分，它们的定义[8]分别如表1和表2所示。

表1 应用Pi演算的项语法

表2 应用Pi演算的进程语法

2.2 密码原语的定义

基于应用Pi演算建立协议的形式化模型之前，首先要对协议用到的所有密码操作原语进行定义。WTLS握手协议用到的密码操作有：对称加解密、非对称加解密、数字签名、哈希函数、数字证书和EC-DH或DH密钥交换。

2.2.1 典型的密码原语

基于应用Pi演算的语法，一些典型的密码原语可以直接用简单的构造函数和析构函数进行定义。

(1)对称加解密：若k为对称密钥，m为被加密信息，用构造函数senc(m,k)表示加密后的信息。根据对称加解密性质，知道加密密钥，能够恢复加密信息，则可用析构函数

sdec(senc(m,k),k)=m

来表示解密。

(2)非对称加解密：若sk为私有密钥，pk(sk)表示公钥的计算，aenc(m,pk(sk))表示公钥加密，则可用

adec(aenc(m,pk(sk)),sk)=m

表示私钥解密获取信息。

(3)数字签名：用sign(m,sk)表示私钥签名，用

checksign(sign(m,sk),pk(sk))=m

表示公钥验证签名信息。

(4)哈希函数：用一元函数hash(m)表示哈希函数，它是不可逆的，没有对应的析构函数。

2.2.2 扩展的密码原语

(1)数字证书：本文定义的数字证书为X.509格式的证书。证书就是一个数据结构，它是由可信机构CA签名颁发的，并将某一实体姓名和相应公钥捆绑在一起。本文用构造函数Cert(sk,X,pkX)来表示证书，它有三个参数，可信机构CA的私钥sk，某一实体姓名X及其公钥pkX。证书是需要验证的，根据CA的公钥pk(sk)，就可以对需要验证的实体进行验证，可以用析构函数

CheckCert(Cert(sk,X,pkX),pk(sk),X)=true

表示验证成功。另外，根据证书，还能得到实体的公钥，表示为析构函数

GetCert(Cert(sk,X,pkX),pk(sk))=pkX。由于证书是由可信机构CA颁发的，需要建立CA的进程模型，可描述为

let CA =

let CertX=

Cert(sk,X, pkX) in out(c1, CertX);

let CertY=

Cert(sk,Y, pkY) in out(c2, CertY)。

(2) EC-DH：椭圆曲线DH密钥交换[9]是取决于椭圆曲线Ep(a,b)上生成元G(x1,y1)的离散对数运算，要求G的阶是一个足够大的素数，且G的阶是满足

nG=0

的最小正整数n。一个主体A从[1,n]中选择一个整数nA作为私钥，并计算

PA=nAG

作为自己的公开密钥。类似地，B也选择一个私钥nB并产生一个公钥

PB=nBG。

A和B都能得到双方的公开密钥PA和PB，这样A可以计算秘密密钥

K=nAPB，

B计算秘密密钥

K=nBPA。

由于

nAPB=nAnBG=nBPA，

这两个密钥是相等的。并且只知道PA，PB和G，是无法算出nA和NB的，从而无法获取秘密密钥。

EC-DH密钥交换需要表述项之间的代数关系，不能编译为析构函数，但可用Blanchet提出的等值理论进行定义，即用等式来表示这些性质。

根据等值理论，可对EC-DH原语进行如下定义：首先定义函数ec(sk,G)表示用椭圆曲线加密体制计算私钥为sk对应的公钥，其中G为生成元，假设它是一个常量。再定义函数com(skx,pky)表示秘密密钥的计算，其中skx表示协议一方的私钥，pky表示协议另一方的公钥。最后构建等式

com(skx,ec(sky,G))=com(sky,ec(skx,G))

来表示

nAPB=nBPA。

此等式从左到右是终止的，满足收敛性。等式的变量skx，sky在等号左右两侧都只出现一次，它也满足线性。

2.3 WTLS握手协议的模型

定义了WTLS握手协议用到的密码原语之后，需要应用Pi演算建立消息交互的模型。在建立形式化模型之前，需要对协议的交互过程进行抽象，抽象后的WTLS握手协议描述如下。

MSG1 C→S:NC

MSG2 S→C:NS,CERTS,CERTREQ

{hash(Messages,NC,NS,MS)}KCS

MSG4 S→C:{hash(Messages,NC,NS,MS)}KCS

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

{Hash(Messages,NC,NS,MS)}KCS。

根据WTLS握手协议的抽象模型，首先分别建立协议交互主体客户端和服务器的进程模型。其中客户端的进程clientC为

let clientC(skC:skey, pkC:pkey, pkCA:spkey) =

in(c1,CertX:bitstring);

new nc: bitstring;

out(c,nc);

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

if checkcert(xCertS, pkCA) = S then

let pkX:pkey = getcert(xCertS, pkCA) in

let PMS = com(skC, pkX) in

let MS:key = ms(PMS,(nc, nx)) in

let kCS:key = ms(MS,(nc, nx)) in

out(c,(CertX,sign(h((M,nc,nx,MS)),skey_to_sskey(skC)),senc(h((M,nc,nx,MS)),kCS)));

in(c, z:bitstring);

if sdec(z, kCS) = h((M, nc, nx, MS)) then

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

服务器的进程serverS为

let serverS(skS:skey,pkS:pkey,pkCA:spkey) =

in(c2,CertY:bitstring);

in(c, ny:bitstring);

new ns:bitstring;

out(c,(ns, CertY));

in(c,(xCertC:bitstring, z:bitstring, q:bitstring));

if checkcert(xCertC, pkCA) = C then

let pkY:pkey = getcert(xCertC, pkCA) in

let PMS = com(skS, pkY) in

let MS:key = ms(PMS,(ny, ns)) in

let kCS:key = ms(MS,(ny, ns)) in

if h((M, ny, ns, MS)) = checksign(z, pkey_to_spkey(pkY)) then

if sdec(q, kCS) = h((M, ny, ns, MS)) then

out(c,senc(h((M, ny, ns, MS)), kCS));

in(c, y:bitstring);

let mx = sdec(y,kCS) in

0.

WTLS握手协议的系统进程由客户端进程clientC、服务器进程serverS以及颁发证书的可信机构进程CA并发组成，主进程为

process

new skC:skey; let pkC = ec(skC, p) in

new skS:skey; let pkS = ec(skS, p) in

new skCA:sskey; let pkCA = spk(skCA) in

(

(!clientC(skC,pkC,pkCA))| (!serverS(skS,pkS,pkCA)) | (!CA(skCA,pkC,pkS))

)

3 WTLS握手协议的安全性分析

3.1 自动化分析工具Pro Verif

Bruno Blanchet开发了形式化自动分析协议工具Pro Verif[10]基于Prolog语言系统，能够分析验证应用Pi演算或者Horn逻辑子句描述的协议的安全属性。它由3部分组成，其体系结构如图2所示。

图2 Pro Verif体系结构图

虽然该工具及其理论仍处于研究之中，但目前已经成功分析了很多协议，如Needham-Schroeder shared key， Otway-ReesMain mode of Skeme，JFK和kerberos等。本文在分析过程中采用了最新版本Pro Verif1.88版[11]。Pro Verif可以证明可达性，对应性断言和观察等价，在此基础上是通过查询来分析协议的秘密性和认证性的。基于Pro Verif的秘密性和认证性被定义如下。

定义1(秘密性) 如果M为协议的一个基本项，输入查询语句：query attacker(M)，其输出结果为not attacker (M) is true，则称协议保证项M的秘密性。

其中attacker(M)表示攻击者能够获取项M。证明可达性是Pro Verif最基本的功能，工具允许研究查询攻击者能够获得哪些项。因此，如果攻击者不能获取项M，即not attacker (M) is true，那么协议就保证了项M的秘密性。

定义2(认证性) 假设A和B为协议交互方，当A认为他已经与B执行过协议时执行事件event(e1(x,y))；当B相信正开始与A运行协议时执行事件event(e2(x,y))，查询语句

query event(e1(x,y))⟹event(e2(x,y))，

其输出结果为

event(e1(x,y))⟹event(e2(x,y)) is true

时，则称协议满足A对B的认证，反之亦然。

其中

event(e1(x,y))⟹event(e2(x,y))

表示如果事件e1(x,y)已经被执行了，那么事件e2(x,y)在这之前已经被执行了。Pro Verif能够验证这种对应性断言。如果A认为他与B执行过协议前，B已经相信正与A运行协议，即A在执行事件e1(x,y)时，B已经执行事件e2(x,y)了，即

event(e1(x,y))⟹event(e2(x,y)) is true，

那么A对B的认证性是满足的。B对A的认证性验证也是类似的。

3.2 安全性分析

3.2.1 秘密性

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

Pro Verif的输出结果为图3所示。由图3可知，Pro Verif的验证结果为true，表明攻击者无法获取双方协商出的会话密钥KCS，WTLS握手协议满足秘密性。

图3 秘密性分析结果

3.2.2 认证性

WTLS握手协议结束时双方都会发送Finished消息来验证密钥交换和认证过程是否成功，那么如果客户端检验服务器发来的Finished消息是正确的，那么客户端就相信已经与服务器完成了协议；反之亦然，如果服务器检验客户端发来的Finished消息是正确的，那么服务器相信是与客户端完成了协议。在分析认证性时，需要声明以下事件:

•event beginC(ns, CertS)：客户端接收到服务器发来Hello消息及证书时，他记录相信正开始与服务器运行协议；

•event endC(kCS)：客户端检验服务器发来的Finished消息是正确的，他已与服务器完成了握手协议；

•event beginS(nc)：服务器接收到客户端发来Hello消息时，他记录相信开始与客户端运行协议；

•event endS(kCS)：服务器检验客户端发来的Finished消息是正确的，他已经与客户端完成了密钥的协商。

(1)客户端对服务器的认证

客户端认为已经与服务器完成了握手协议(event endC(kCS))，那么服务器之前必然已经开始与客户端运行协议(event beginS(nc))，在用Pro Verif工具进行验证时，通过查询语句

query event(endC(kCS))⟹event(beginS(nc))

可得出认证结果。

(2) 服务器对客户端的认证

服务器认为已经与客户端完成了密钥协商(event endS(kCS))，那么客户端之前已确认是与服务器在运行协议(event beginC(ns, CertS))，通过

query event(endS(kCS))⟹event(beginC(ns, CertS))

查询语句可验证结果。

Pro Verif的输出结果如图4和图5所示。Pro Verif的验证结果都为true，表明客户端和服务器能够确认彼此身份，WTLS握手协议满足认证性。

图4 客户端对服务器认证的分析结果

图5 服务器对客户端认证的分析结果

4 结束语

基于应用Pi演算，对WTLS握手协议中数字证书和EC-DH密码原语进行了定义，并建立了WTLS握手协议的形式化模型，最后用Pro Verif工具验证了其秘密性和认证性，结果表明WTLS握手协议满足其安全性说明。在今后的研究中，将进一步扩展应用Pi演算的语法，定义更多更复杂的密码原语，使其能够分析更复杂的安全协议。

[1] 冯登国.安全协议:理论与实践[M].北京:清华大学出版社,2011:72.

[2] Kusters R， Trudrung T. Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach[C]// Proceedings of the 15th ACM conference on Computer and Communications Security (CCS’08), Alexandria, VA, USA: Hilton Alexandria Mark Center, 2008: 129-138.

[3] Kusters R， Trudrung T. Using ProVerif to analyze protocols with Diffie-Hellman exponentiation[C]// 22nd IEEE Computer Security Foundations Symposium (CSF’09), New-York, USA: IEEE Computer Society, 2009: 157-171.

[4] Blanchet B, Abadi M, Fournet C. Automated verification of selected equivalences for security protocols[J]. Journal of Logic and Algebraic Programming, 2008, 75(1): 3-51.

[5] 徐军.关于秘密共享方案在应用pi演算中的实现[J].计算机应用,2013,33(11):3247-3251.

[6] 赵宇,王亚弟,韩继红.基于Spi演算的SSL3.0协议安全性分析[J].计算机应用,2005,25(11):2515-2520.

[7] WAP Forum. Wireless Application Protocol Wireless Transport Layer Security Specification Version 06[EB/OL]. (2006-02-02)[2014-12-20]. http: //www. wapforum.org.

[8] 黄伟.基于应用PI演算的远程网络投票协议安全性自动化证明[D].武汉:中南民族大学,2011:10-12.

[9] 李海峰,马海云,徐燕文.现代密码学原理及应用[M].北京: 国防工业出版社, 2013 :127-128.

[10] Blanchet B. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[C]//Proceeding of the 14th IEEE Computer Security Foundations Workshop(CSFW-14), Cape Breton, Nova Scotia, Canada: IEEE Computer Society, 2001:82-96.

[11] Blanchet B, Smyth B, Cheval V. ProVerif 1.88: Automatic Cryptographic Protocol Verifier User Manual and Tutorial, [EB/OL]. (2013-08-30)[2014-12-01]. http: //prosecco.gforge.inria.fr/personal/bblanche/proverif/

[责任编辑:祝剑]

Modeling and analysis of WTLS handshake protocol based on applied Pi calculus

PAN Jin1, GU Xiang2, WANG Xiaoming2

(1.Department of Information Security, Xi’an Communications Institute, Xi’an 710106, China；2.Team of 12th, Xi’an Communications Institute, Xi’an 710106, China)

According to the special cryptographic primitives of WTLS handshake protocol, EC-DH key agreements using equation theories and digital certificates using a process model of a Certification Authority issuing digital certificates are defined in this paper. Based on those definitions, formal models for WTLS handshake protocol are built. In the last, Pro Verif tool is used to verify security and authentication of the protocol. Results show that WTLS handshake protocol can meet its security statement.

applied Pi calculus, cryptographic primitives, WTLS handshake protocol, Pro Verif, security, authentication

2015-01-03

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

潘进(1959-)，男，博士，教授，博导，从事网络安全研究。E-mail:2373242787@qq.com 顾香(1987-)，女，硕士研究生，研究方向为网络安全与对抗。E-mail:xiangxiangycc@163.com

10.13682/j.issn.2095-6533.2015.02.006

TP309

A

2095-6533(2015)02-0026-06