熊 玲,彭代淵

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

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

熊 玲1,2,彭代淵2

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

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

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

0 引 言

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

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

1 認(rèn)證測(cè)試

1.1 符號(hào)與約定

本文使用的符號(hào)說(shuō)明如下:

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

K表示密鑰。

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

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

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

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

1.2 基本概念和定理

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

交互過(guò)程:

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

定義8設(shè)(∑,P)是一個(gè)滲透串空間,如果∑由下述3種串組成,就稱(chēng)它為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ā)起者對(duì)響應(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é)點(diǎn)＜Si,1＞,并且＜Si,1＞圯＜Si,2＞構(gòu)成變換邊,又因SB?KP,則邊＜Si,1＞圯＜Si,2＞構(gòu)成{RB‖RA‖A}SB關(guān)于RA輸入測(cè)試,{RB‖RA‖A}SB為RA的測(cè)試元素。根據(jù)輸入測(cè)試定理,叢C中存在常規(guī)結(jié)點(diǎn)m和m′,使得{RB‖RA‖A}SB為m′的組成元素,并且邊m圯+m′為RA的變換進(jìn)行邊。

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

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

2.3 響應(yīng)者對(duì)發(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輸入測(cè)試,{RA‖RB‖B}SA為RB的測(cè)試元素。根據(jù)輸入測(cè)試定理,叢C中存在常規(guī)結(jié)點(diǎn)m和m′,{RA‖RB‖B}SA為m′的組成元素,并且邊m圯+m′為RB的變換進(jìn)行邊。

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

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

2.4 安全性分析

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

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

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

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

4 結(jié) 語(yǔ)

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

認(rèn)證測(cè)試方法具有簡(jiǎn)潔、清晰的優(yōu)點(diǎn),但是目前認(rèn)證測(cè)試方法主要對(duì)密碼協(xié)議的認(rèn)證屬性進(jìn)行形式化分析,下一步工作將繼續(xù)研究認(rèn)證測(cè)試方法對(duì)密碼其它安全屬性的形式化分析,其次是安全協(xié)議形式化分析自動(dòng)化工具的實(shí)現(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)證測(cè)試的安全協(xié)議分析[J].軟件學(xué)報(bào),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)證測(cè)試方法的局限性[J].軟件學(xué)報(bào),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—),男,博士,教授,主要研究方向?yàn)榫幋a理論,信息安全。

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—),女,碩士,工程師,主要研究方向?yàn)槊艽a理論;

2014-05-05;

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