熊 玲,彭代淵

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

一種改進(jìn)的安全協(xié)議認(rèn)證測試分析方法*

熊 玲1,2,彭代淵2

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

認(rèn)證測試方法是以串空間模型為基礎(chǔ)的一種形式化分析方法。該方法在協(xié)議形式化分析過程中具有簡潔、清晰等優(yōu)點,然而,認(rèn)證測試方法不能檢測類型缺陷攻擊,文中著力于研究認(rèn)證測試方法的定義、輸出測試定理、輸入測試定理以及主動測試定理,以ISO/IEC9798-3協(xié)議的安全性分析為例指出認(rèn)證測試方法的局限,在此基礎(chǔ)上重新修改認(rèn)證測試方法的相關(guān)定義,提出新的改進(jìn)方案,新的認(rèn)證測試方法擴(kuò)大了認(rèn)證測試?yán)碚摰膽?yīng)用范圍。

安全協(xié)議 認(rèn)證測試 串空間

0 引 言

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

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

1 認(rèn)證測試

1.1 符號與約定

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

A、B表示協(xié)議的參與方。

K表示密鑰。

RA和RB分別表示為A和B的隨機(jī)數(shù)。

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

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

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

1.2 基本概念和定理

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

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

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

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

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

如果值a在唯一起源于結(jié)點n0,且邊n0圯+n是關(guān)于a的轉(zhuǎn)換邊,則稱邊n0圯+n是a的一個測試。

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

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

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

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

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

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

2 認(rèn)證測試的局限性研究

下面通過利用ISO/IEC9798-3協(xié)議的分析來說明認(rèn)證測試的局限。

2.1 ISO/IEC9798-3協(xié)議

目標(biāo):A和B完成雙向認(rèn)證。

交互過程:

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

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

1)攻擊者串。

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

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

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

2.2 發(fā)起者對響應(yīng)者的認(rèn)證

發(fā)起者保障:假設(shè)

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

2)SA?KP,SB?KP。

3)RA在∑中唯一源發(fā)。

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

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

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

根據(jù)上面的分析,發(fā)起者A能夠?qū)憫?yīng)者B的身份進(jìn)行成功認(rèn)證。

2.3 響應(yīng)者對發(fā)起者的認(rèn)證

響應(yīng)者保障:假設(shè)

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

2)SA?KP,SB?KP。

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

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

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

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

根據(jù)上面的分析,發(fā)起者B能夠?qū)憫?yīng)者A的身份進(jìn)行成功認(rèn)證。

2.4 安全性分析

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

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

3 改進(jìn)的認(rèn)證測試方案

基于以上分析,重新定義認(rèn)證測試相關(guān)定義。

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

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

4 結(jié) 語

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

認(rèn)證測試方法具有簡潔、清晰的優(yōu)點,但是目前認(rèn)證測試方法主要對密碼協(xié)議的認(rèn)證屬性進(jìn)行形式化分析,下一步工作將繼續(xù)研究認(rèn)證測試方法對密碼其它安全屬性的形式化分析,其次是安全協(xié)議形式化分析自動化工具的實現(xiàn)。

[1] 高悅翔,李敏.基于串空間模型的WAI密鑰協(xié)商協(xié)議分析[J].通信技術(shù),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] 楊明,羅軍舟.基于認(rèn)證測試的安全協(xié)議分析[J].軟件學(xué)報,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] 劉家芬,周明天.突破認(rèn)證測試方法的局限性[J].軟件學(xué)報,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