一種改進的安全協議認證測試分析方法*

熊 玲,彭代淵

(1.保密通信重點實驗室,四川成都610041;2.西南交通大學,四川成都610041)

一種改進的安全協議認證測試分析方法*

熊 玲1,2,彭代淵2

(1.保密通信重點實驗室,四川成都610041;2.西南交通大學,四川成都610041)

認證測試方法是以串空間模型為基礎的一種形式化分析方法。該方法在協議形式化分析過程中具有簡潔、清晰等優點,然而,認證測試方法不能檢測類型缺陷攻擊,文中著力于研究認證測試方法的定義、輸出測試定理、輸入測試定理以及主動測試定理,以ISO/IEC9798-3協議的安全性分析為例指出認證測試方法的局限,在此基礎上重新修改認證測試方法的相關定義,提出新的改進方案,新的認證測試方法擴大了認證測試理論的應用范圍。

安全協議 認證測試 串空間

0 引 言

串空間理論因為其簡單清晰的證明過程被廣泛應用于協議安全形式化分析中[1]。2000年,Guttman和Thayer在文獻[2]中首次提出了基于串空間理論的認證測試方法。隨后Guttman于2002年對認證測試理論作了進一步的研究,為認證測試定理開辟了新的空間[3]。認證測試方法以挑戰-應答機制來驗證協議安全屬性,具有簡潔、清晰等優點,然而,目前認證測試方法不能有效檢測類型缺陷攻擊。國內學者楊明和羅軍周提出了一種增強型的認證測試方案,該方案解決了安全協議關聯屬性問題[4],使協議分析人員可以比較方便的進行手動分析,更利于自動化工具的實現。劉家芬和周明天在文獻[5]的基礎上改進了認證測試方案,突破了認證測試元素在整個協議消息中不能被多重加密的限制,擴展了認證測試理論的應用[6]。

本文著力于研究認證測試方法的測試定理,通過分析ISO/IEC9798-3協議的安全性來說明認證測試不能抵抗類型缺陷攻擊的局限,在此基礎上提出了一種改進的認證測試方法,新的方法具有更廣泛的應用。

1 認證測試

1.1 符號與約定

本文使用的符號說明如下:

A、B表示協議的參與方。

K表示密鑰。

RA和RB分別表示為A和B的隨機數。

CertA和CertB分別表示為A和B的公鑰證書,證書中包含了公鑰,身份識別碼等信息。

{M}K表示用密鑰K加密消息M。

P表示攻擊者可能獲得的所有消息的集合。

1.2 基本概念和定理

下面介紹認證測試中基本概念和定理[1]:

定義1 組成元素(Component)：項t0稱為項t的組成元素,當且僅當t0不屬于級聯類型,且對任何t0≠t1,均有t0?t1?t。即組成元素或者是原子項,或者是密文,簡稱元素。

定義2 新元素(New Component)：若t0是結點＜S,i＞的新元素,當且僅當t0是＜S,i＞的組成元素,且不是其他任意結點＜S,j＞,(j＜i)的組成元素。

定義3 變換邊(Transformed Edge)/變換進行邊(Transforming Edge)：若＜S,i＞圯+＜S,j＞是關于值a的變換邊,當且僅當a在結點＜S,i＞發送,且a在結點＜S,j＞以新元素形式接收。若＜S,i＞圯+＜S,j＞是關于值a的變換進行邊,當且僅當a在結點＜S,i＞接收,且a在結點＜S,j＞以新元素形式發送。

定義4 測試元素(Test Component)/測試(Test)：t={h}k是結點n關于a的測試元素,如果a?t,且t是結點n的組成元素,t不是串空間∑中其它常規結點的組成元素的子項。

如果值a在唯一起源于結點n0,且邊n0圯+n是關于a的轉換邊,則稱邊n0圯+n是a的一個測試。

定義5 輸出測試(Outgoing Test)：邊n0圯+n1是元素t={h}k關于a的輸出測試,如果①邊n0圯+n1是a的一個測試;②K?KP;③a不在結點n0的除t以外的任何其他元素中出現;④t是結點n0關于a的一個測試元素。

定義6 輸入測試(Incoming Test)：邊n0圯+n1是元素t={h}k關于a的輸入測試,如果①邊n0圯+n1是a的一個測試;②K?KP;③t是結點n1關于a的一個測試元素。

定義7 主動測試(Unsolicited Test)：接收結點n是元素t={h}k關于a的主動測試,如果①t是結點n1關于a的一個測試元素;②K?KP。

定理1 輸出測試定理：假設叢C中,n0,n1∈C,邊n0圯+n1是元素t關于a的輸出測試,則:①必然存在結點m,m′∈C滿足t是m的組成元素,并且邊m圯+m′是a的測試進行邊;②若a在結點m′的元素t={h}k中出現,t不是任何其它常規結點的元素,且K?KP,則必然存在一個包含t為組成元素的常規結點,且該結點為負結點。

定理2 輸入測試定理：假設叢C中,n0,n1∈C,邊n0圯+n1是元素t關于a的輸入測試,則必然存在常規結點m,m′∈C滿足t是m′的組成元素,并且m圯+m′是a的測試進行邊;

定理3 主動測試定理：假設叢C中,n∈C,且n是元素t關于a的主動測試,則必然存在常規正結點m∈C,使得t是m的組成元素。

2 認證測試的局限性研究

下面通過利用ISO/IEC9798-3協議的分析來說明認證測試的局限。

2.1 ISO/IEC9798-3協議

目標:A和B完成雙向認證。

交互過程:

其中交互傳遞過程中的A和B表示身份識別碼,SA和SB分別為A和B的私鑰。

定義8設(∑,P)是一個滲透串空間,如果∑由下述3種串組成,就稱它為ISO/IEC9798-3串空間:

1)攻擊者串。

2)發起者串Init[A,B,RA,RB],其跡為:

3)響應者串Resp[A,B,RA,RB],其跡為:

圖1 ISO/IEC9798-3協議串空間模型Fig.1 Strand space model of ISO/IEC9798-3

2.2 發起者對響應者的認證

發起者保障:假設

1)ISO/IEC9798-3協議的串空間∑中,C為包含發起者串Si∈Init[A,B,RA,RB]的叢,并且發起者串的C-height為3。

2)SA?KP,SB?KP。

3)RA在∑中唯一源發。

需要證明的是叢C中一定包含響應串Sr∈Resp[A,B,RA,RB],且該響應者串的C-height為2。

證明：根據ISO/IEC9798-3協議的叢圖,RA在∑中唯一源發于節點＜Si,1＞,并且＜Si,1＞圯＜Si,2＞構成變換邊,又因SB?KP,則邊＜Si,1＞圯＜Si,2＞構成{RB‖RA‖A}SB關于RA輸入測試,{RB‖RA‖A}SB為RA的測試元素。根據輸入測試定理,叢C中存在常規結點m和m′,使得{RB‖RA‖A}SB為m′的組成元素,并且邊m圯+m′為RA的變換進行邊。

根據輸入測試定理,結點m′為正結點,且m′為響應者串Sr中的結點,m′=＜Sr,2＞,且{RB‖RA‖A}SB為m′的組成元素。由于常規正結點中包含{RB‖RA‖A}SB形式的只有＜Sr,2＞,且該串的C-height為2。所以C中必然存在一個響應者串Resp[A,B,RA,RB]。

根據上面的分析,發起者A能夠對響應者B的身份進行成功認證。

2.3 響應者對發起者的認證

響應者保障:假設

1)ISO/IEC9798-3協議的串空間∑中,C為包含響應者串Sr∈Resp[A,B,RA,RB]的叢,并且響應者串的C-height為3。

2)SA?KP,SB?KP。

3)RA≠RB,且RB在∑中唯一源發。

需要證明的是叢C中一定包含發起者串Si∈Init[A,B,RA,RB],且發起者串的C-height為3。

證明：根據協議叢圖RA≠RB,且RB唯一起源于＜Sr,2＞,由于SA?KP,所以邊＜Sr,2＞圯＜Sr,3＞構成{RA‖RB‖B}SA關于RB輸入測試,{RA‖RB‖B}SA為RB的測試元素。根據輸入測試定理,叢C中存在常規結點m和m′,{RA‖RB‖B}SA為m′的組成元素,并且邊m圯+m′為RB的變換進行邊。

常規正結點中包含{RA‖RB‖B}SA形式的只有＜Si,3＞,且{RA‖RB‖B}SA為m′的組成元素,且該串的C-height為3。故C中必然存在一個發起者串Si∈Init[A,B,RA,RB]。

根據上面的分析,發起者B能夠對響應者A的身份進行成功認證。

2.4 安全性分析

根據認證測試分析得出ISO/IEC9798-3協議滿足雙向認證,然而實際上ISO/IEC9798-3協議中響應者對發起者認證測試存在漏洞,圖2是該協議的攻擊過程。這是由于認證測試理論對測試元素的定義有局限,2.3節叢C中存在常規結點m和m′, {RA‖RB‖B}SA為m′的組成元素,并且邊m圯+m′為RB的變換進行邊。如果針對測試元素{RA‖RB‖B}SA,這種方法并沒有問題,然而實際上響應者B并沒有將RA與前一輪使用的RA進行一致性驗證,現有的認證測試方法并沒有考慮該種情況,攻擊者可以冒充發起者A將{R′A‖RB‖B}SA發送給相應者B,B認為是A,從而攻擊成功。

圖2 ISO/IEC9798-3協議串空間攻擊模型Fig.2 Attack strand space model of ISO/IEC9798-3

3 改進的認證測試方案

基于以上分析,重新定義認證測試相關定義。

定義9 新輸入測試(incoming test)：邊n0圯+n1是元素t′={h′}k關于a的輸入測試,如果①邊n0圯+n1是a的一個測試;②K?KP;③h′∩h={…a…},其中t={h}k是結點n1關于a的一個測試元素。

定理4 新輸入測試定理：假設叢C中,n0,n1∈C,邊n0圯+n1是元素t′關于a的輸入測試,則必然存在常規結點m,m′∈C滿足t′={h′}k,a?t′是m′的組成元素,并且m圯+m′是a的測試進行邊。

4 結 語

本文通過認證測試方法對ISO/IEC9798-3協議進行形式化實例分析,指出現有的認證測試不能抵抗類型缺陷攻擊,在此基礎上重新定義了認證測試方法的相關定義,并提出改進的方案,顯然改進的方案擴大了協議的形式化分析范圍。

認證測試方法具有簡潔、清晰的優點,但是目前認證測試方法主要對密碼協議的認證屬性進行形式化分析,下一步工作將繼續研究認證測試方法對密碼其它安全屬性的形式化分析,其次是安全協議形式化分析自動化工具的實現。

[1] 高悅翔,李敏.基于串空間模型的WAI密鑰協商協議分析[J].通信技術,2008,41(12):313-315.

GAO Yue-Xiang,LI Ming.Analysis of WAI Key Agreement Protocol based on the Strand Space Model,Communication Technology.2008,41(12):313-315.

[2] GUTTMAN JD,FABREGA FJT.Authentication Tests [C]//Proc.of the 2000 IEEE Symp on Security and Privacy.Los Amitoses:IEEE Computer Society Press, 2000.96-109.

[3] GUTTMAN JD,FABREGA FJT.Authentication tests and the structure of bundles[J].Theoretical Computer Science.2002,283(02):333-380.

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

YANG Ming,LUO Jun-zhou.Analysis of Security Protocols Based on Authentication Test.Journal of Software, 2006,17(1):148-156.

[5] PERRIG A,SONG D.Looking for Diamonds in the Desert -Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement[C]//Proc.of the 13th IEEE Computer Security Foundations Workshop.Los Amitoses:IEEE Computer Society Press,2000.64-76.

[6] 劉家芬,周明天.突破認證測試方法的局限性[J].軟件學報,2009,20(10):2799-2809.

LIU Jia-fen,ZHOU Ming-tian.Overcome the Limitation on Authentication Test[J].Journal of Software,2009, 20(10):2799-2809.

XIONG Ling(1983-),female,M.Sci., engineer,majoring in cryptography theory.

彭代淵(1955—),男,博士,教授,主要研究方向為編碼理論,信息安全。

PENG Dai-yuan(1955-),male,Ph.D.,professor, mainly working at coding theory and information security.

An Improved Authentication Test for Security Protocol Analysis

XIONG Ling1,2,PENG Dai-yuan2
(1.Key Laboratory of Confidential Communication,Chengdu Sichuan 610041,China; 2.Southwest Jiaotong University,Chengdu Sichuan 610041,China)

Authentication test is a new type of formal analysis based on strand space model.Compared with strand space model,authentication test is simpler and clearer.However,authentication test cannot detect type flaw attack.This paper focuses on the definition of authentication test,outgoing test theorems,incoming theorems and unsolicited test theorems,and takes ISO/IEC9798-3 protocol as an example,then points out deficiency of authentication test.It modifies the definition of authentication test,and proposes an improved authentication test theory.Compared with original method,the new approach could expand the application scale of the authentication test theory.

security protocol;authentication test;strand space

TP393

A

1002-0802(2014)08-0951-04

10.3969/j.issn.1002-0802.2014.08.022

熊 玲(1983—),女,碩士,工程師,主要研究方向為密碼理論;

2014-05-05;

2014-06-10 Received date：2014-05-05;Revised date：2014-06-10