泰彬彬 王俊芳

（中國電子科技集團公司第五十四研究所河北石家莊 050081）

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

泰彬彬 王俊芳

（中國電子科技集團公司第五十四研究所河北石家莊 050081）

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

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

1 引言

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

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

2 形式化分析方法及比較

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

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

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

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

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

3 認證測試方法及規(guī)則

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

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

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

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

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

若t={|h|}K是任何a在n中的測試分量，且KP，則負節(jié)點n是t的一個主動測試[6]。

4 DTLS協(xié)議介紹

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

圖1 DTLS握手及密鑰交換過程

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

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

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

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

⑴客戶端串模型

所用符號說明：

VerC和VerS為客戶端和服務(wù)器端支持的協(xié)議版本號；SecC和SecS為支持的加密方法；NC和NS為協(xié)議中產(chǎn)生的隨機數(shù)；pre-K表示客戶端發(fā)送完證書后生成的主密鑰；Session ID表示客戶端發(fā)起會話的會話標(biāo)識號；Cookie表示服務(wù)器為本次會話生成的標(biāo)識號；message表示握手協(xié)議運行至發(fā)送消息為止所有消息的內(nèi)容的hash；CS-K表示客戶端與服務(wù)器協(xié)商的會話密鑰。；CID表示客戶端標(biāo)識，SID表示服務(wù)器端標(biāo)識；K-change為會話密鑰生成的標(biāo)識；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é)點)為結(jié)點事件函數(shù)，sign()為結(jié)點符號函數(shù)，匚表示子項關(guān)系。

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

條目（1）證明

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

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

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

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

條目（2）證明

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

6 結(jié)束語

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

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

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

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

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

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

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

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

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

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

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

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

[12]李謝華，李建華,楊樹堂等.認證測試方法在安全協(xié)議分析中的應(yīng)用[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