泰彬彬 王俊芳

（中國(guó)電子科技集團(tuán)公司第五十四研究所河北石家莊 050081）

基于串空間認(rèn)證測(cè)試的DTLS協(xié)議認(rèn)證性分析

泰彬彬 王俊芳

（中國(guó)電子科技集團(tuán)公司第五十四研究所河北石家莊 050081）

網(wǎng)絡(luò)通信的普及和發(fā)展使得對(duì)網(wǎng)絡(luò)協(xié)議尤其是安全協(xié)議的需求日益增長(zhǎng)，同時(shí)安全要求及攻擊方式的多樣化對(duì)網(wǎng)絡(luò)安全協(xié)議的效率和準(zhǔn)確性提出了更高的要求。通過(guò)對(duì)各種協(xié)議安全性分析方法進(jìn)行研究，采用串空間方法對(duì)DTLS協(xié)議進(jìn)行形式化建模，進(jìn)而采用認(rèn)證測(cè)試方法進(jìn)行協(xié)議認(rèn)證性證明，用簡(jiǎn)明清晰的方式驗(yàn)證DTLS協(xié)議的認(rèn)證性，保障了數(shù)據(jù)傳輸?shù)陌踩?/p>

協(xié)議安全性分析 串空間 認(rèn)證測(cè)試 DTLS；

1 引言

安全協(xié)議使用密碼技術(shù),實(shí)現(xiàn)網(wǎng)絡(luò)環(huán)境下的身份認(rèn)證和信息保密,它看似簡(jiǎn)單,但若確保正確是極其困難的。因此,對(duì)安全協(xié)議進(jìn)行分析就顯得十分重要，當(dāng)前形式化的分析方法被公認(rèn)為分析認(rèn)證協(xié)議的最有效手段。

近些年來(lái)，基于UDP的應(yīng)用程序不斷增加，為了保障數(shù)據(jù)傳輸?shù)陌踩?，DTLS協(xié)議應(yīng)運(yùn)而生，然而對(duì)DTLS協(xié)議的安全性分析十分缺乏，且大多為主觀分析或模擬仿真等非形式化分析的方法，或是分析過(guò)程不夠精確和嚴(yán)格，針對(duì)這種情況采用形式化分析方式對(duì)DTLS協(xié)議進(jìn)行認(rèn)證性分析。

2 形式化分析方法及比較

現(xiàn)狀主流的安全協(xié)議分析方法有3種：基于模態(tài)邏輯技術(shù)的分析方法、基于模型檢測(cè)技術(shù)的分析方法、基于定理證明的分析方法。

①基于模態(tài)邏輯技術(shù)的分析方法是一個(gè)演繹推理的過(guò)程，先定義邏輯推理規(guī)則和公理，其后對(duì)安全協(xié)議的形式化分析[1]。目前應(yīng)用最為廣泛，但該方法不能對(duì)保密性安全屬性進(jìn)行分析，并且存在規(guī)則不完善和語(yǔ)義不精確等問(wèn)題；

②基于模型檢測(cè)技術(shù)的分析方法也稱為基于狀態(tài)檢測(cè)的方法，其優(yōu)點(diǎn)是自動(dòng)化程度高，可以借助自動(dòng)分析工具來(lái)完成分析過(guò)程[2]。但其原理是對(duì)協(xié)議狀態(tài)空間進(jìn)行搜索，然而隨著協(xié)議的增大其狀態(tài)空間呈指數(shù)增長(zhǎng)，因此總是面臨著狀態(tài)空間爆炸問(wèn)題的困擾；

③基于定理證明的分析方法，其中最具代表性的是Paulson歸納證明法和串空間模型[2]。Paulson歸納法將協(xié)議形式化為所有可能的“跡”的集合，而“跡”是協(xié)議的通信事件序列，最終在“跡”上通過(guò)歸納的方法來(lái)證明協(xié)議的安全；串空間模型將協(xié)議運(yùn)行的各個(gè)狀態(tài)和整體過(guò)程轉(zhuǎn)化為集合和有向圖的形式進(jìn)行描述，利用協(xié)議運(yùn)行的特性訂閱集合中各個(gè)狀態(tài)間的偏序關(guān)系，通過(guò)對(duì)集合中最小元的定義和證明，確定是否存在攻擊節(jié)點(diǎn)。

采用串空間模型法，即可以避免了模型檢測(cè)方法普遍存在的狀態(tài)空間爆炸問(wèn)題，又把協(xié)議的執(zhí)行過(guò)程用圖示法表示，不僅簡(jiǎn)單直觀，也有利于通過(guò)圖論和算法對(duì)協(xié)議進(jìn)行分析。認(rèn)證測(cè)試方法是應(yīng)用串空間模型的一種協(xié)議安全分析的技術(shù)，認(rèn)證測(cè)試與其他協(xié)議安全分析方法相比更為簡(jiǎn)潔、直觀和清晰，更易于使用。因此選擇采用串空間方法建模，采用認(rèn)證測(cè)試方法進(jìn)行認(rèn)證性分析。

3 認(rèn)證測(cè)試方法及規(guī)則

認(rèn)證測(cè)試方法是基于串空間模型的一種安全協(xié)議形式化分析與設(shè)計(jì)方法。在認(rèn)證測(cè)試中仍然使用串空間模型中關(guān)于串、叢的定義和性質(zhì)，但是將保密數(shù)據(jù)作為構(gòu)造測(cè)試的標(biāo)準(zhǔn)，構(gòu)造測(cè)試分量，并根據(jù)測(cè)試分量的格式分別構(gòu)造入測(cè)試、出測(cè)試和主動(dòng)測(cè)試，從而證明協(xié)議能夠滿足的認(rèn)證和保密屬性。其基本思想為：假設(shè)安全協(xié)議中的一個(gè)主體生成并發(fā)送了一條包含新數(shù)據(jù)的消息，而后在一個(gè)不同的加密形式中接收到，則可以斷定某個(gè)擁有相關(guān)密鑰的主體接收并轉(zhuǎn)換了包含的消息[3]。認(rèn)證測(cè)試帶有一些本身所具有的規(guī)則，應(yīng)用這些規(guī)則能夠簡(jiǎn)化協(xié)議分析的過(guò)程。

定義1：令C為一個(gè)叢，S為一個(gè)串，n1，n2S，對(duì)于aM，aterm(n1)，并且n2產(chǎn)生一個(gè)新的分量t2，使得at2，若n1為負(fù)節(jié)點(diǎn)，n2為正節(jié)點(diǎn)，則n1n2為變換邊，若n1為正節(jié)點(diǎn)，n2為負(fù)節(jié)點(diǎn)，則n1n2為被變換邊[4]。

定義2：如果a唯一產(chǎn)生于節(jié)點(diǎn)n0，并且n0n1是a的被變換邊，則n0n1是a的測(cè)試[4]。

定義4：若n0n1是對(duì)a的測(cè)試，并且KP，a在節(jié)點(diǎn)n0處唯一生成，同時(shí)滿足t0={|h|}K是a在n0的測(cè)試分量，則稱n0n1是a在t0的出測(cè)試，而t0={|h|}K是a在n0的出測(cè)試分量[5]。

若n0n1是對(duì)a的測(cè)試，并且KP，a在節(jié)點(diǎn)n0處唯一生成，同時(shí)滿足t0={|h|}K是a在n1的測(cè)試分量，則稱n0n1是a在t0的入測(cè)試，而t0={|h|}K是a在n1的入測(cè)試分量[5]。

若t={|h|}K是任何a在n中的測(cè)試分量，且KP，則負(fù)節(jié)點(diǎn)n是t的一個(gè)主動(dòng)測(cè)試[6]。

4 DTLS協(xié)議介紹

DTLS協(xié)議由5部分組成，其中記錄層為基礎(chǔ)，握手層、密鑰規(guī)格變更層、警告層和應(yīng)用層為記錄層所承載的數(shù)據(jù)。記錄層會(huì)將承載的數(shù)據(jù)進(jìn)行分段、壓縮和加密（協(xié)議好密碼后才進(jìn)行），最后添加DTLS協(xié)議頭部。DTLS協(xié)議通過(guò)明文進(jìn)行握手和密鑰交換，協(xié)商好密鑰后應(yīng)用層數(shù)據(jù)傳輸是加密進(jìn)行的，其握手及密鑰交換流程如圖1所示。

圖1 DTLS握手及密鑰交換過(guò)程

在握手過(guò)程中，由于DTLS協(xié)議是基于UDP之上的，消息在傳輸過(guò)程中可能會(huì)丟失，是不可靠的。為此，DTLS協(xié)議采用接收確認(rèn)這種傳統(tǒng)的處理消息丟失的方法進(jìn)行處理，保證了消息傳輸?shù)目煽啃浴?/p>

5 DTLS協(xié)議認(rèn)證性證明

DTLS握手協(xié)議的形式化描述如下：

結(jié)合DTLS協(xié)議交互過(guò)程，及形式化分析中對(duì)明文消息可忽略[9]，由此可將DTLS協(xié)議的串空間模型描述如下：

⑴客戶端串模型

所用符號(hào)說(shuō)明：

VerC和VerS為客戶端和服務(wù)器端支持的協(xié)議版本號(hào)；SecC和SecS為支持的加密方法；NC和NS為協(xié)議中產(chǎn)生的隨機(jī)數(shù)；pre-K表示客戶端發(fā)送完證書后生成的主密鑰；Session ID表示客戶端發(fā)起會(huì)話的會(huì)話標(biāo)識(shí)號(hào)；Cookie表示服務(wù)器為本次會(huì)話生成的標(biāo)識(shí)號(hào)；message表示握手協(xié)議運(yùn)行至發(fā)送消息為止所有消息的內(nèi)容的hash；CS-K表示客戶端與服務(wù)器協(xié)商的會(huì)話密鑰。；CID表示客戶端標(biāo)識(shí)，SID表示服務(wù)器端標(biāo)識(shí)；K-change為會(huì)話密鑰生成的標(biāo)識(shí)；MC和MS為協(xié)議中交換的消息歷史；C-K和S-K為雙方公鑰；Certificate{signCA{S，S-K}}、Certificate{signCA{C，C-K}}為經(jīng)可信中心簽名的證書；signC{}為客戶端用私鑰簽名的消息；C-height(S)表示串S在叢C中的叢高度；term(結(jié)點(diǎn))為結(jié)點(diǎn)事件函數(shù)，sign()為結(jié)點(diǎn)符號(hào)函數(shù)，匚表示子項(xiàng)關(guān)系。

由認(rèn)證測(cè)試的理論可知發(fā)起者發(fā)起通信后必定有響應(yīng)者響應(yīng)通信，且在交互的過(guò)程中必定存在某個(gè)帶有新鮮性的變量（隨機(jī)數(shù)）的不同加密形式，以確保該交互過(guò)程的唯一性及保密性[10]；每個(gè)響應(yīng)者的響應(yīng)必定存在發(fā)起者發(fā)起通信，且交互過(guò)程存在某個(gè)帶有新鮮性的變量的不同加密形式，以確保該交互過(guò)程的唯一性及保密性[11]。

條目（1）證明

設(shè)C為叢，N為包含隨機(jī)數(shù)NC的一個(gè)集合，由DTLS協(xié)議的認(rèn)證過(guò)程可知，C-height(Si)=4，結(jié)點(diǎn)＜Si，1＞為串中NC出現(xiàn)的第一個(gè)結(jié)點(diǎn)，且NC匚term(＜Si，1＞)且NCN，所以其是集合N的入口點(diǎn)，所以NC起源于結(jié)點(diǎn)＜Si，1＞，且由假設(shè)知，每個(gè)NC均為唯一獨(dú)立的，所以NC唯一起源于結(jié)點(diǎn)＜Si，1＞。

令結(jié)點(diǎn)n1=＜Si，1＞，n2=＜Si，4＞，sign(n1)=+，sign(n2)=-，NC起源于n1，且存在n2的新分量t2={NC}CS-K使得NC匚t2，所以邊是NC的被變換邊。

并且NC唯一起源于n1，所以邊是NC的測(cè)試。

令t={NS，NC，MS}CS-K，NC匚t，且t是n2的分量，t不是其他任意結(jié)點(diǎn)的真子項(xiàng)，所以t是NC的測(cè)試分量。令P為攻擊者的密鑰集合，邊是NC的測(cè)試，其中P，除t外，NC不在n2的任何分量中出現(xiàn)(唯一起源)，t是結(jié)點(diǎn)n2中a的測(cè)試分量。且邊是NC的被變換邊，稱邊n1n2為t中數(shù)據(jù)NC的入測(cè)試。

條目（2）證明

由上面條目（1）和（2）的證明可以看出客戶端與服務(wù)器相互認(rèn)證成功，從而證明了DTLS協(xié)議的認(rèn)證性，從而通過(guò)形式化語(yǔ)言對(duì)其認(rèn)證性進(jìn)行了分析。

6 結(jié)束語(yǔ)

詳細(xì)討論了DTLS協(xié)議原理，運(yùn)用形式化分析的方法對(duì)DTLS進(jìn)行形式化建模，并考慮到形式化分析中存在過(guò)于復(fù)雜的證明步驟及狀態(tài)空間的無(wú)限膨脹，采用認(rèn)證測(cè)試的方法對(duì)DTLS協(xié)議的形式化模型進(jìn)行安全性分析，降低了證明的復(fù)雜性，從而通過(guò)較為簡(jiǎn)潔的方式證明了該協(xié)議的理論安全性。

[1]冀云剛.傳輸層安全協(xié)議研究及應(yīng)用[D].陜西:西安電子科技大學(xué),2011.

[2]余磊.基于串空間模型的安全協(xié)議分析方法研究[D].安徽:淮北師范大學(xué),2010.

[3]王聰，劉軍，王孝國(guó),等.安全協(xié)議原理與驗(yàn)證[M].北京:北京郵電大學(xué)出版社,2011.

[4]李建華.網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證[M].北京:機(jī)械工業(yè)出版社,2010.

[5]邢媛，蔣睿.基于串空間模型的UMTS AKA協(xié)議安全分析與改進(jìn)[J].東南大學(xué)學(xué)報(bào),2010(6):1163-1168.

[6]孔娟，曹利培.TLS協(xié)議認(rèn)證測(cè)試模型與形式化分析[J].計(jì)算機(jī)工程與應(yīng)用,2009(23):100-103.

[7]劉家芬.安全協(xié)議形式化分析中認(rèn)證測(cè)試方法的研究[D].成都:電子科技大學(xué),2009.

[8]鄧葒.基于DTLS協(xié)議VPN的研究與實(shí)現(xiàn)[D].成都:電子科技大學(xué),2011.

[9]周清雷，毋曉英.認(rèn)證測(cè)試方法的擴(kuò)展及其應(yīng)用[J].鄭州大學(xué)學(xué)報(bào),2010(3):50-53.

[10]楊明，羅軍舟.基于認(rèn)證測(cè)試的安全協(xié)議分析[J].軟件學(xué)報(bào),2006(1):148-156.

[11]方燕萍.串空間模型及其認(rèn)證測(cè)試方法的擴(kuò)展與應(yīng)用[D].江蘇:蘇州大學(xué),2009.

[12]李謝華，李建華,楊樹(shù)堂等.認(rèn)證測(cè)試方法在安全協(xié)議分析中的應(yīng)用[J].計(jì)算機(jī)工程,2006(2):19-22.

Analysis on DTLS Protocol Authentication Based on Strand Space Authentication Test

TAI Bin-bin WANG Jun-fang
(The 54th Research Institute of CETC,Shijiazhuang Hebei 050081,China)

The popularization and development of network communication make the demands of network protocol,especially security protocol,increase significantly.At the same time,the diversification of security requirements and attack modes require higher efficiency and accuracy of network security protocol.This paper studies various protocol security analysis methods,implements the formal modeling for DTLS protocol by strand space method,certifies the protocol authentication by authentication test method,and verifies the authentication of DTLS protocol through concise and clear way to ensure the security of data transmission.

interruption;timer;performance test;thread;event

TP39

A

1008-1739（2014）24-51-3

定稿日期：2014-11-26