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

泰彬彬 王俊芳

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

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

泰彬彬 王俊芳

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

網絡通信的普及和發展使得對網絡協議尤其是安全協議的需求日益增長，同時安全要求及攻擊方式的多樣化對網絡安全協議的效率和準確性提出了更高的要求。通過對各種協議安全性分析方法進行研究，采用串空間方法對DTLS協議進行形式化建模，進而采用認證測試方法進行協議認證性證明，用簡明清晰的方式驗證DTLS協議的認證性，保障了數據傳輸的安全。

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

1 引言

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

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

2 形式化分析方法及比較

現狀主流的安全協議分析方法有3種：基于模態邏輯技術的分析方法、基于模型檢測技術的分析方法、基于定理證明的分析方法。

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

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

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

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

3 認證測試方法及規則

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

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

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

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

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

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

4 DTLS協議介紹

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

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

在握手過程中，由于DTLS協議是基于UDP之上的，消息在傳輸過程中可能會丟失，是不可靠的。為此，DTLS協議采用接收確認這種傳統的處理消息丟失的方法進行處理，保證了消息傳輸的可靠性。

5 DTLS協議認證性證明

DTLS握手協議的形式化描述如下：

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

⑴客戶端串模型

所用符號說明：

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

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

條目（1）證明

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

令結點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不是其他任意結點的真子項，所以t是NC的測試分量。令P為攻擊者的密鑰集合，邊是NC的測試，其中P，除t外，NC不在n2的任何分量中出現(唯一起源)，t是結點n2中a的測試分量。且邊是NC的被變換邊，稱邊n1n2為t中數據NC的入測試。

條目（2）證明

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

6 結束語

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

[1]冀云剛.傳輸層安全協議研究及應用[D].陜西:西安電子科技大學,2011.

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

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

[4]李建華.網絡安全協議的形式化分析與驗證[M].北京:機械工業出版社,2010.

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

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

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

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

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

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

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

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