潘 進, 顧 香, 王小明

(1.西安通信學院 信息安全系, 陜西 西安 710106; 2.西安通信學院 12隊, 陜西 西安 710106)

基于應用Pi演算的WTLS握手協(xié)議建模與分析

潘 進1, 顧 香2, 王小明2

(1.西安通信學院 信息安全系, 陜西 西安 710106; 2.西安通信學院 12隊, 陜西 西安 710106)

針對WTLS握手協(xié)議中的特殊密碼原語，用等值理論定義了橢圓曲線DH密鑰交換原語，用可信機構(gòu)頒發(fā)數(shù)字證書的方式定義了數(shù)字證書原語。并在密碼原語定義的基礎(chǔ)上建立了WTLS握手協(xié)議的形式化模型，最后用Pro Verif工具分析了協(xié)議的秘密性和認證性。結(jié)果表明WTLS握手協(xié)議滿足其安全性說明。

應用Pi演算;密碼原語；WTLS握手協(xié)議；Pro Verif；秘密性；認證性

隨著電子政務、電子商務的興起以及科研、教育、國防工作對網(wǎng)絡依賴的加劇，網(wǎng)絡安全受到廣泛關(guān)注。網(wǎng)絡通信，作為各項網(wǎng)絡業(yè)務的基礎(chǔ)，它的實質(zhì)是協(xié)議通信，在很大程度上，協(xié)議的安全性決定著網(wǎng)絡的安全性。為了保證網(wǎng)絡信息的安全，需要協(xié)議具有高度的安全性。網(wǎng)絡協(xié)議安全性分析受到了世界各國的高度重視。形式化分析方法長期以來被視為分析協(xié)議安全性的有效方法，基于應用Pi演算來描述協(xié)議，再用Pro Verif工具自動化驗證協(xié)議安全屬性是一種可靠簡單的協(xié)議分析方法，在實踐中該方法是比較精確的[1]。

應用Pi演算是在Pi演算語法的基礎(chǔ)上增加了函數(shù)應用，是Spi演算的一般形式，它的優(yōu)點是能夠描述各種密碼學原語，缺點是沒有給定各個密碼原語的具體定義，不適當?shù)拿艽a原語定義可能會造成驗證工具分析的失敗。特別是一些大型復雜協(xié)議中用到的特殊密碼原語，定義起來比較復雜，如DH(Diffie-Hellman)密鑰交換，橢圓曲線加密，XOR(異或)運算和數(shù)字證書等。

Kusters等將XOR運算中的一個元素考慮為常量定義了XOR原語[2]，將DH密鑰交換中的指數(shù)設(shè)為常量定義了DH密鑰交換原語[3]，這種方法比較繁瑣，定義較復雜；文[4]和文[5]用等值理論分別定義了DH密鑰交換原語，但等值理論只能處理特定的等式；文[6]用簽名的方式定義了數(shù)字證書原語，但是對證書的描述不夠全面。

針對WTLS握手協(xié)議中的數(shù)字證書和基于橢圓曲線的Diffie-Hellman(EC-DH)交換兩種特殊的密碼操作，本文根據(jù)文獻[4-5]中的等值理論方法定義了EC-DH原語，用可信機構(gòu)CA頒發(fā)數(shù)字證書的方式定義了數(shù)字證書原語并建立WTLS握手協(xié)議模型，最后用Pro Verif工具驗證了協(xié)議的秘密性和認證性。

1 WTLS握手協(xié)議概述

WTLS協(xié)議[7]為無線傳輸層安全協(xié)議，它共定義了握手協(xié)議、更改密碼規(guī)范協(xié)議、警告協(xié)議以及記錄協(xié)議4個協(xié)議。其中WTLS握手協(xié)議主要用于協(xié)商協(xié)議版本，選擇密碼算法，認證通信雙方的身份(可選功能)以及生成共享密鑰，一個完整的握手過程如圖1所示。握手過程就是建立或者恢復一個會話的過程，是WTLS協(xié)議棧中非常重要的一個協(xié)議。

圖1 WTLS握手過程流程

(1)客戶端發(fā)起一個新的會話，發(fā)送ClientHello消息。包括客戶端生成的隨機數(shù)NC，該次會話的標識符Sid，客戶端所支持的密碼套件列表SuiteC及壓縮算法列表MethodC。

(2)服務器收到ClientHello消息后，選擇其所支持的密碼套件和壓縮算法等，并生成隨機數(shù)，發(fā)送下列消息。

?ServerHello消息：服務器生成的隨機數(shù)NS，該次會話的標識符Sid，服務器從客戶端發(fā)送過來的密碼套件列表中選擇其所支持的密碼套件SuiteS，以及從客戶端發(fā)送過來的壓縮算法列表中選擇其所支持的壓縮算法MethodS。

?ServerCertificate消息：如果服務器需要被認證，服務器發(fā)送自己的證書給客戶端。

?ServerKeyExchange消息：該消息僅在發(fā)送的ServerCertificate消息中沒有包含足夠的信息使客戶端交換預主密鑰時才發(fā)送，用來為客戶端協(xié)商預主密鑰傳遞密碼信息。

?CertificateRequest消息：服務器發(fā)送該消息指示客戶端提供其證書。

?ServerHelloDone消息：服務器Hello消息階段的結(jié)束。

(3)客戶端通過服務器發(fā)送的證書進行認證。如果認證不成功，客戶端發(fā)送一個警告消息，會話無法建立。如果認證成功，客戶端發(fā)送下列消息。

?ClientCertificate消息：該消息只有在服務器要求證書的情況下才發(fā)送。如果客戶端沒有合適的證書，也可以發(fā)送不包含證書的ClientCertificate消息。

?ClientKeyExchange消息：一般使用RSA公鑰加密的方式直接傳輸預主密鑰，或使用DH、EC-DH方法使雙方商定該密鑰。本文討論使用EC-DH協(xié)商密鑰的方式。

?CertificateVerify消息：用來提供顯示的客戶證書校驗。

?ChangeCipherSpec消息：表明客戶端和服務器的記錄層將從預備狀態(tài)轉(zhuǎn)換到當前狀態(tài)，以后的數(shù)據(jù)傳送將采用協(xié)商好的加密算法和對稱密鑰KCS進行加密、計算MAC等。

?Finished消息：第一個用剛剛商定的密鑰和算法進行保護的消息，用來校驗密鑰交換和認證過程是否成功。

(4)服務器同樣也發(fā)送ChangeCipherSpec消息和Finished消息。

2 基于應用Pi演算的WTLS握手協(xié)議建模

2.1 應用Pi演算

應用Pi演算是一種新的進程演算理論，它的語法包括項和進程兩部分，它們的定義[8]分別如表1和表2所示。

表1 應用Pi演算的項語法

表2 應用Pi演算的進程語法

2.2 密碼原語的定義

基于應用Pi演算建立協(xié)議的形式化模型之前，首先要對協(xié)議用到的所有密碼操作原語進行定義。WTLS握手協(xié)議用到的密碼操作有：對稱加解密、非對稱加解密、數(shù)字簽名、哈希函數(shù)、數(shù)字證書和EC-DH或DH密鑰交換。

2.2.1 典型的密碼原語

基于應用Pi演算的語法，一些典型的密碼原語可以直接用簡單的構(gòu)造函數(shù)和析構(gòu)函數(shù)進行定義。

(1)對稱加解密：若k為對稱密鑰，m為被加密信息，用構(gòu)造函數(shù)senc(m,k)表示加密后的信息。根據(jù)對稱加解密性質(zhì)，知道加密密鑰，能夠恢復加密信息，則可用析構(gòu)函數(shù)

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

來表示解密。

(2)非對稱加解密：若sk為私有密鑰，pk(sk)表示公鑰的計算，aenc(m,pk(sk))表示公鑰加密，則可用

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

表示私鑰解密獲取信息。

(3)數(shù)字簽名：用sign(m,sk)表示私鑰簽名，用

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

表示公鑰驗證簽名信息。

(4)哈希函數(shù)：用一元函數(shù)hash(m)表示哈希函數(shù)，它是不可逆的，沒有對應的析構(gòu)函數(shù)。

2.2.2 擴展的密碼原語

(1)數(shù)字證書：本文定義的數(shù)字證書為X.509格式的證書。證書就是一個數(shù)據(jù)結(jié)構(gòu)，它是由可信機構(gòu)CA簽名頒發(fā)的，并將某一實體姓名和相應公鑰捆綁在一起。本文用構(gòu)造函數(shù)Cert(sk,X,pkX)來表示證書，它有三個參數(shù)，可信機構(gòu)CA的私鑰sk，某一實體姓名X及其公鑰pkX。證書是需要驗證的，根據(jù)CA的公鑰pk(sk)，就可以對需要驗證的實體進行驗證，可以用析構(gòu)函數(shù)

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

表示驗證成功。另外，根據(jù)證書，還能得到實體的公鑰，表示為析構(gòu)函數(shù)

GetCert(Cert(sk,X,pkX),pk(sk))=pkX。由于證書是由可信機構(gòu)CA頒發(fā)的，需要建立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)的離散對數(shù)運算，要求G的階是一個足夠大的素數(shù)，且G的階是滿足

nG=0

的最小正整數(shù)n。一個主體A從[1,n]中選擇一個整數(shù)nA作為私鑰，并計算

PA=nAG

作為自己的公開密鑰。類似地，B也選擇一個私鑰nB并產(chǎn)生一個公鑰

PB=nBG。

A和B都能得到雙方的公開密鑰PA和PB，這樣A可以計算秘密密鑰

K=nAPB，

B計算秘密密鑰

K=nBPA。

由于

nAPB=nAnBG=nBPA，

這兩個密鑰是相等的。并且只知道PA，PB和G，是無法算出nA和NB的，從而無法獲取秘密密鑰。

EC-DH密鑰交換需要表述項之間的代數(shù)關(guān)系，不能編譯為析構(gòu)函數(shù)，但可用Blanchet提出的等值理論進行定義，即用等式來表示這些性質(zhì)。

根據(jù)等值理論，可對EC-DH原語進行如下定義：首先定義函數(shù)ec(sk,G)表示用橢圓曲線加密體制計算私鑰為sk對應的公鑰，其中G為生成元，假設(shè)它是一個常量。再定義函數(shù)com(skx,pky)表示秘密密鑰的計算，其中skx表示協(xié)議一方的私鑰，pky表示協(xié)議另一方的公鑰。最后構(gòu)建等式

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

來表示

nAPB=nBPA。

此等式從左到右是終止的，滿足收斂性。等式的變量skx，sky在等號左右兩側(cè)都只出現(xiàn)一次，它也滿足線性。

2.3 WTLS握手協(xié)議的模型

定義了WTLS握手協(xié)議用到的密碼原語之后，需要應用Pi演算建立消息交互的模型。在建立形式化模型之前，需要對協(xié)議的交互過程進行抽象，抽象后的WTLS握手協(xié)議描述如下。

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消息抽象為用協(xié)商好的對稱密鑰KCS對消息進行加密，雙方可驗證內(nèi)容的正確性，可表述為

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

根據(jù)WTLS握手協(xié)議的抽象模型，首先分別建立協(xié)議交互主體客戶端和服務器的進程模型。其中客戶端的進程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握手協(xié)議的系統(tǒng)進程由客戶端進程clientC、服務器進程serverS以及頒發(fā)證書的可信機構(gòu)進程CA并發(fā)組成，主進程為

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握手協(xié)議的安全性分析

3.1 自動化分析工具Pro Verif

Bruno Blanchet開發(fā)了形式化自動分析協(xié)議工具Pro Verif[10]基于Prolog語言系統(tǒng)，能夠分析驗證應用Pi演算或者Horn邏輯子句描述的協(xié)議的安全屬性。它由3部分組成，其體系結(jié)構(gòu)如圖2所示。

圖2 Pro Verif體系結(jié)構(gòu)圖

雖然該工具及其理論仍處于研究之中，但目前已經(jīng)成功分析了很多協(xié)議，如Needham-Schroeder shared key， Otway-ReesMain mode of Skeme，JFK和kerberos等。本文在分析過程中采用了最新版本Pro Verif1.88版[11]。Pro Verif可以證明可達性，對應性斷言和觀察等價，在此基礎(chǔ)上是通過查詢來分析協(xié)議的秘密性和認證性的。基于Pro Verif的秘密性和認證性被定義如下。

定義1(秘密性) 如果M為協(xié)議的一個基本項，輸入查詢語句：query attacker(M)，其輸出結(jié)果為not attacker (M) is true，則稱協(xié)議保證項M的秘密性。

其中attacker(M)表示攻擊者能夠獲取項M。證明可達性是Pro Verif最基本的功能，工具允許研究查詢攻擊者能夠獲得哪些項。因此，如果攻擊者不能獲取項M，即not attacker (M) is true，那么協(xié)議就保證了項M的秘密性。

定義2(認證性) 假設(shè)A和B為協(xié)議交互方，當A認為他已經(jīng)與B執(zhí)行過協(xié)議時執(zhí)行事件event(e1(x,y))；當B相信正開始與A運行協(xié)議時執(zhí)行事件event(e2(x,y))，查詢語句

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

其輸出結(jié)果為

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

時，則稱協(xié)議滿足A對B的認證，反之亦然。

其中

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

表示如果事件e1(x,y)已經(jīng)被執(zhí)行了，那么事件e2(x,y)在這之前已經(jīng)被執(zhí)行了。Pro Verif能夠驗證這種對應性斷言。如果A認為他與B執(zhí)行過協(xié)議前，B已經(jīng)相信正與A運行協(xié)議，即A在執(zhí)行事件e1(x,y)時，B已經(jīng)執(zhí)行事件e2(x,y)了，即

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

那么A對B的認證性是滿足的。B對A的認證性驗證也是類似的。

3.2 安全性分析

3.2.1 秘密性

WTLS握手協(xié)議建立了會話密鑰KCS，協(xié)議需要保證會話密鑰的秘密性。當s為秘密信息，攻擊者無法獲取通過會話密鑰KCS加密后傳輸?shù)拿孛苄畔時，則WTLS握手協(xié)議具有秘密性。在用Pro Verif工具分析時，通過查詢語句query attacker(s)能夠進行WTLS握手協(xié)議的秘密性分析。

Pro Verif的輸出結(jié)果為圖3所示。由圖3可知，Pro Verif的驗證結(jié)果為true，表明攻擊者無法獲取雙方協(xié)商出的會話密鑰KCS，WTLS握手協(xié)議滿足秘密性。

圖3 秘密性分析結(jié)果

3.2.2 認證性

WTLS握手協(xié)議結(jié)束時雙方都會發(fā)送Finished消息來驗證密鑰交換和認證過程是否成功，那么如果客戶端檢驗服務器發(fā)來的Finished消息是正確的，那么客戶端就相信已經(jīng)與服務器完成了協(xié)議；反之亦然，如果服務器檢驗客戶端發(fā)來的Finished消息是正確的，那么服務器相信是與客戶端完成了協(xié)議。在分析認證性時，需要聲明以下事件:

?event beginC(ns, CertS)：客戶端接收到服務器發(fā)來Hello消息及證書時，他記錄相信正開始與服務器運行協(xié)議；

?event endC(kCS)：客戶端檢驗服務器發(fā)來的Finished消息是正確的，他已與服務器完成了握手協(xié)議；

?event beginS(nc)：服務器接收到客戶端發(fā)來Hello消息時，他記錄相信開始與客戶端運行協(xié)議；

?event endS(kCS)：服務器檢驗客戶端發(fā)來的Finished消息是正確的，他已經(jīng)與客戶端完成了密鑰的協(xié)商。

(1)客戶端對服務器的認證

客戶端認為已經(jīng)與服務器完成了握手協(xié)議(event endC(kCS))，那么服務器之前必然已經(jīng)開始與客戶端運行協(xié)議(event beginS(nc))，在用Pro Verif工具進行驗證時，通過查詢語句

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

可得出認證結(jié)果。

(2) 服務器對客戶端的認證

服務器認為已經(jīng)與客戶端完成了密鑰協(xié)商(event endS(kCS))，那么客戶端之前已確認是與服務器在運行協(xié)議(event beginC(ns, CertS))，通過

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

查詢語句可驗證結(jié)果。

Pro Verif的輸出結(jié)果如圖4和圖5所示。Pro Verif的驗證結(jié)果都為true，表明客戶端和服務器能夠確認彼此身份，WTLS握手協(xié)議滿足認證性。

圖4 客戶端對服務器認證的分析結(jié)果

圖5 服務器對客戶端認證的分析結(jié)果

4 結(jié)束語

基于應用Pi演算，對WTLS握手協(xié)議中數(shù)字證書和EC-DH密碼原語進行了定義，并建立了WTLS握手協(xié)議的形式化模型，最后用Pro Verif工具驗證了其秘密性和認證性，結(jié)果表明WTLS握手協(xié)議滿足其安全性說明。在今后的研究中，將進一步擴展應用Pi演算的語法，定義更多更復雜的密碼原語，使其能夠分析更復雜的安全協(xié)議。

[1] 馮登國.安全協(xié)議:理論與實踐[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] 徐軍.關(guān)于秘密共享方案在應用pi演算中的實現(xiàn)[J].計算機應用,2013,33(11):3247-3251.

[6] 趙宇,王亞弟,韓繼紅.基于Spi演算的SSL3.0協(xié)議安全性分析[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演算的遠程網(wǎng)絡投票協(xié)議安全性自動化證明[D].武漢:中南民族大學,2011:10-12.

[9] 李海峰,馬海云,徐燕文.現(xiàn)代密碼學原理及應用[M].北京: 國防工業(yè)出版社, 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-)，男，博士，教授，博導，從事網(wǎng)絡安全研究。E-mail:2373242787@qq.com 顧香(1987-)，女，碩士研究生，研究方向為網(wǎng)絡安全與對抗。E-mail:xiangxiangycc@163.com

10.13682/j.issn.2095-6533.2015.02.006

TP309

A

2095-6533(2015)02-0026-06