基于間接認證鏈的輸入測試證明方法

通信作者： 鄧珍榮(1977-)，女，廣西全州人,副教授，研究方向為網(wǎng)絡(luò)協(xié)議安全、軟件架構(gòu)。E-mail:zhrdeng@ guet.edu.cn

引文格式： 代凱，鄧珍榮.基于間接認證鏈的輸入測試證明方法[J].桂林電子科技大學(xué)學(xué)報，2015,35(1):49-53.

代凱，鄧珍榮

(桂林電子科技大學(xué) 計算機科學(xué)與工程學(xué)院，廣西 桂林541004)

摘要：針對無法運用認證測試方法中的輸入測試對Yahalom協(xié)議進行驗證的問題，提出一種基于間接認證鏈的輸入測試證明方法。該方法引入間接一致性的概念，解決了Yahalom協(xié)議中存在的不完整的挑戰(zhàn)-應(yīng)答機制和輸入測試在原證明方法上只具備直接性這2個問題，成功地將輸入測試運用于驗證Yahalom協(xié)議，并將該證明方法推廣到對Yahalom-Paulson協(xié)議的驗證。新的證明方法擴展了輸入測試的應(yīng)用范圍。

關(guān)鍵詞：安全協(xié)議；認證測試；Yahalom協(xié)議；間接認證鏈

收稿日期：2014-03-28

基金項目：廣西可信軟件重點實驗室開放基金(PF13089X)

中圖分類號：TP309文獻標(biāo)志碼： A

Anewprovingmethodofincomingtestbasedonindirectauthenticationchain

DaiKai,DengZhenrong

(SchoolofComputerScienceandEngineering,GuilinUniversityofElectronicTechnology,Guilin541004,China)

Abstract：Yahalom protocol can’t be verified by incoming test in authentication test, so a new incoming test proving method based on indirect authentication chain is proposed. The concept of indirect consistency is introduced to solve two issues, one is the incomplete challenge-response mechanism in Yahalom protocol, another is directness characteristic in the original proving method of incoming test. This method verifies Yahalom protocol by incoming test successfully, and it is extended to verify the Yahalom-Paulson protocol. The new proving method effectively extends the application range of incoming test.

Keywords：securityprotocol;authenticationtest;Yahalomprotocol;indirectauthenticationchain

隨著互聯(lián)網(wǎng)的飛速發(fā)展，網(wǎng)絡(luò)安全問題變得越來越突出和嚴峻，解決網(wǎng)絡(luò)安全問題對于眾多網(wǎng)絡(luò)應(yīng)用來說是當(dāng)務(wù)之急。安全協(xié)議作為網(wǎng)絡(luò)安全的基礎(chǔ)，其安全性對于整個網(wǎng)絡(luò)的安全起著至關(guān)重要的作用，而安全協(xié)議工作時復(fù)雜的環(huán)境條件和判斷協(xié)議是否能夠正常執(zhí)行的困難性，使得分析安全協(xié)議的安全性是一項困難的工作。認證測試方法是一種較新的安全協(xié)議分析方法，相較于其他分析方法具有簡潔、高效、直觀的優(yōu)點，其更符合安全協(xié)議分析領(lǐng)域未來的發(fā)展趨勢。

認證測試方法[1]是2000年由Guttman等提出的在串空間[2]理論基礎(chǔ)上用于判斷認證協(xié)議一致性的方法，已成功應(yīng)用于Otway-Rees[3]、Neuman-Stubblebine[4]和NSPK[5]等協(xié)議的分析，但現(xiàn)有的文獻都沒有給出驗證Yahalom協(xié)議[6]的證明過程。為此，嘗試運用認證測試方法對Yahalom協(xié)議進行分析。

1Yahalom協(xié)議認證性分析

1988年提出的Yahalom協(xié)議是一個經(jīng)典的認證協(xié)議，如圖1所示。參加協(xié)議的主體是通信雙方A、B和認證服務(wù)器S，其目的是在通信雙方之間分配會話密鑰。

圖1　Yahalom協(xié)議 Fig.1　Yahalom protocol

1)A→B:ANa；

2)B→S:B{ANaNb}Kbs；

3)S→A:{BKabNaNb}Kas{AKab}Kbs；

4)A→B:{AKab}Kbs{Nb}Kab。

1.1Yahalom協(xié)議的串空間模型

Yahalom協(xié)議串空間由以下3類串族組成：

1)發(fā)起者串Si，協(xié)議跡為：〈+ANa,-{BKabNaNb}KasH,+H{Nb}Kab〉，Si∈Cinit[A，B，Na，Nb，Kab]。

2)響應(yīng)者串Sr，協(xié)議跡為：〈-ANa,+B{ANaNb}Kbs,-{AKab}Kbs{Nb}Kab〉，Sr∈Cresp[A，B，Na，Nb，Kab]。

3)服務(wù)器串S，協(xié)議跡為：〈-B{ANaNb}Kbs,+{BKabNaNb}Kas{AKab}Kbs〉，S∈Cserv[A，B，Na，Nb，Kab]。

其中H表示主體無法識別的加密信息。假設(shè)A，B∈Tname，Kbs?Kp，Kas?Kp，Kab?Tname，Na，Nb∈TTname，Na和Nb在Σ中是唯一起源。Yahalom協(xié)議的叢圖如圖2所示。

圖2　Yahalom協(xié)議叢圖 Fig.2　The bundle of Yahalom protocol

1.2Yahalom協(xié)議的認證性分析

1.2.1服務(wù)器S對響應(yīng)者B的認證

命題1假設(shè)C為Yahalom的串空間Σ中的一個叢，A≠B，Kas，Kbs?Kp，S∈Cserv[A，B，Na，Nb，Kab]的Cheight為1，則C中存在Sr∈Cresp[A，B，Na，Nb，*]，其Cheight為2。

證明{ANaNb}Kbs構(gòu)成主動測試，根據(jù)主動測試定理，C中存在正則節(jié)點m∈C，t為m的分量，A≠B，{ANaNb}Kbs只能出現(xiàn)在串Sr∈Cresp[A，B，Na，Nb，*]的〈Sr，2〉節(jié)點上。命題得證。

1.2.2發(fā)起者A對服務(wù)器S的認證

命題2 假設(shè)Yahalom串空間Σ的叢C中，A≠B，Kas?Kp，存在串Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為2，則C中存在S∈Cserv[A，B，Na，Nb，Kab]，且其Cheight為2。

證明〈Si，1〉?〈Si，2〉構(gòu)成Na的輸入測試，測試分量為{BKabNaNb}Kas，根據(jù)輸入測試定理，C中應(yīng)存在Na的正則變換邊。根據(jù)叢C中的消息類型，該變換邊只能在S∈Cserv[A，B，Na，Nb，Kab]上出現(xiàn)。命題得證。

1.2.3 響應(yīng)者B對發(fā)起者A的認證

命題3假設(shè)Yahalom串空間Σ的叢C中，A≠B，Kbs?Kp，存在串Sr∈Cresp[A，B，Na，Nb，Kab]，且其Cheight為3，則C中存在Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為3。

證明〈Sr，2〉?〈Sr，3〉構(gòu)成Nb的輸入測試，測試分量為{Nb}Kab，根據(jù)輸入測試定理，C中應(yīng)存在Nb的正則變換邊。根據(jù)叢C中的消息類型，該變換邊只能在Si∈Cinit[A，B，Na′，Nb，Kab]上出現(xiàn)，且其Cheight為3。因A與B在參數(shù)Na上沒有達成直接一致,且沒有附加條件能證明Na′=Na。于是，不能證明叢C中存在Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為3。命題不得證。

2輸入測試不能分析Yahalom協(xié)議的原因

經(jīng)過分析發(fā)現(xiàn)，輸入測試不能驗證Yahalom協(xié)議的原因有以下2點：Yahalom協(xié)議的特殊性和認證測試協(xié)議證明方法的局限性。

2.1Yahalom協(xié)議的特殊性

Yahalom協(xié)議的設(shè)計是很微妙的[6]，在信息4)中，響應(yīng)者B收到的不是像Otway-Rees協(xié)議一樣通信的不同實體只收到一個來自可信第3方(TTP)的證書，而是來自發(fā)起者A的2個證書。其中一個證書包含密鑰Kab，但未保證新鮮的標(biāo)識，而另一個證書卻用未證實安全的密鑰Kab對其加密。后一個證書能否作為證明密鑰Kab新鮮性的證據(jù)，其依賴于在不完整的挑戰(zhàn)-應(yīng)答過程中被密鑰Kab加密的Nb的保密性，之所以稱這個挑戰(zhàn)-問答過程是不完整的，是因為在信息4)中只有發(fā)起者A對響應(yīng)者B的挑戰(zhàn)，而沒有響應(yīng)者B對發(fā)起者A的應(yīng)答。

2.2認證測試協(xié)議證明方法的局限性

認證測試方法通過找出信息所在的確切位置證明信息的一致性。Guttman[1]只考慮了直接的認證過程而未考慮通過第3方的認證過程，也就是測試分量多次變換后參數(shù)的間接一致性的問題。例如在Yahalom協(xié)議中，響應(yīng)者B對發(fā)起者A發(fā)起的認證，輸入測試〈Sr，2〉?〈Sr，3〉就存在這2個對應(yīng)的變換邊〈S，1〉?〈S，2〉和〈Si，2〉?〈Si，3〉。Guttman直接運用輸入測試的證明方法，未考慮通信實體之間間接的認證過程，導(dǎo)致無法采用輸入測試對Yahalom進行正面的驗證。經(jīng)分析發(fā)現(xiàn)，實體之間的認證關(guān)系可通過間接認證實現(xiàn)，即采用一串直接認證的間接認證鏈證明實體間的認證性。

3間接認證鏈方法的提出

3.1參數(shù)直接一致性和參數(shù)間接一致性

協(xié)議的認證等級與協(xié)議實體在通信中對參數(shù)的一致程度有著密切的關(guān)系[7]，因此，在提出間接認證鏈方法前，先定義參數(shù)直接一致性和參數(shù)間接一致性。

定義1參數(shù)直接一致性：若在認證測試中直接由測試分量的項就能確定一致的參數(shù)，則B對于A在該參數(shù)上有直接一致性。

定義2參數(shù)間接一致性：若Nb唯一起源于B，且主體B對A在Nb上達成直接一致，而對Na未直接一致，但A對于C在Na和Nb上有直接一致性。若有C=B，則主體B對A在Na達成間接一致；若C≠B，但C對于D在Na和Nb上有直接一致性，若D=B，則主體B對A在Na達成間接一致。

把參數(shù)分為主體標(biāo)識、隨機數(shù)和協(xié)商數(shù)據(jù)3個種類[8]，當(dāng)主體標(biāo)識達成直接一致，Na與Nb中只有一個參數(shù)直接一致時，若要證明另一個參數(shù)一致，則要證明另一個參數(shù)滿足參數(shù)間接一致性。

3.2參數(shù)間接一致性的證明方法

假如B對A進行認證，項a唯一起源于B，那么認證的方法就圍繞a進行。其步驟為：

1)假設(shè)認證方(B)的串執(zhí)行完畢。

2)求出認證方(B)與被認證方(A)的參數(shù)一致的情況，若項a在對話中達成直接一致，而其他項b沒有，要證明b在對話中達成間接一致，就要考慮以A為認證方時，被認證方(B或者是可信第3方S)的參數(shù)一致的情況，但有個條件，就是B的測試分量對應(yīng)在A上的變換邊或節(jié)點的Cheight一定要大于等于以A為認證方時測試分量所在A的Cheight。

3)若步驟2)中認證的S不等于B，則繼續(xù)步驟2)；若S等于B，則比較初始認證方與S的參數(shù)一致性情況；若B與S在a上達成一致，則b與b′是相同的。

3.3間接認證鏈方法

當(dāng)通信雙方無法僅通過彼此的直接證明確定認證等級時，可通過對未認證一致的參數(shù)證明其具有參數(shù)間接一致性，從而完成對協(xié)議認證等級的證明。

4間接認證鏈方法證明Yahalom協(xié)議

4.1發(fā)起者A對響應(yīng)者B的認證

命題4假設(shè)Yahalom串空間Σ的叢C中，A≠B，Kas?Kp，存在串Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為2，則C中存在Sr∈Cresp[A，B，Na，Nb，*]，且其Cheight為2。

證明若Si∈Cinit[A，B，Na，Nb，Kab]，且Cheight為2，根據(jù)命題2只能證明S∈Cserv[A，B，Na，Nb，Kab]，且其Cheight為2。又由命題1，間接證明Sr∈Cresp[A，B，Na，Nb，*]，其Cheight為2。命題得證。

4.2響應(yīng)者B對發(fā)起者A的認證

命題5 假設(shè)Yahalom串空間Σ的叢C中，A≠B，Kbs?Kp，存在串Sr∈Cresp[A，B，Na，Nb，Kab]，且其Cheight為3，則C中存在Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為3。

證明〈Sr，2〉?〈Sr，3〉構(gòu)成Nb的輸入測試，測試分量為{Nb}Kab，根據(jù)輸入測試定理，C中應(yīng)存在Nb的正則變換邊。根據(jù)叢C的消息類型，該變換邊只能在Si∈Cinit[A，B，Na′，Nb，Kab]，且其Cheight為3。因A與B在參數(shù)Na上未達成直接一致，且Nb在B上是唯一起源，對Si運用命題4，證明叢C中存在Sr′∈Cresp[A，B，Na′，Nb，*]，且其Cheight為2。由響應(yīng)者串的形式，Nb起源于〈Sr′，2〉，因Nb是唯一起源，故〈Sr′，2〉=〈Sr，2〉，因此，Sr′=Sr,Na′=Na。于是，叢C中存在Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為3。命題得證。

本證明與Guttman[9]使用基于新進性輸出測試證明的結(jié)論效果相同，且與文獻[10]使用理想與誠實證明的結(jié)論也相同，從而表明了間接認證鏈方法的正確性。

5間接認證鏈方法的應(yīng)用

5.1Yahalom-Paulson協(xié)議

為了證明間接認證鏈方法具有廣泛適用性，將該方法推廣到對Yahalom-Paulson協(xié)議的分析。Burrows等[11]使用BAN邏輯對Yahalom協(xié)議進行分析后指出，在協(xié)議運行過程中，若存在惡意的參與者，則存在對協(xié)議的重放攻擊。Burrows將Yahalom協(xié)議改進為BAN-Yahalom協(xié)議，并采用BAN邏輯證明了BAN-Yahalom協(xié)議的安全性。Syverson[12]給出了對BAN-Yahalom協(xié)議的2種攻擊，Paulson[6]修改了BAN-Yahalom協(xié)議，給出了Yahalom-Paulson協(xié)議，如圖3所示。

圖3　Yahalom-Paulson協(xié)議 Fig.3　Yahalom-Paulson protocol

1)A→B:ANa；

2)B→S:BNb{ANa}Kbs；

3)S→A:Nb{BKabNa}Kas{ABKabNb}Kbs；

4)A→B:{ABKabNb}Kbs{Nb}Kab。

Yahalom-Paulson協(xié)議串空間由3類串族組成：

1)發(fā)起者串Si，協(xié)議跡為：〈+ANa,-Nb{BKabNa}KasH，+H{Nb}Kab〉，Si∈Cinit[A，B，Na，Nb，Kab]。

2)響應(yīng)者串Sr，協(xié)議跡為：〈-ANa,+BNb{ANa}Kbs,-{ABKabNb}Kbs{Nb}Kab〉，Sr∈Cresp[A，B，Na，Nb，Kab]。

3)服務(wù)器串S，協(xié)議跡為：〈-BNb{ANa}Kbs，+Nb{BKabNa}Kas{ABKabNb}Kbs〉，S∈Cserv[A，B，Na，Nb，Kab]。

其中H為主體無法識別的加密信息，假設(shè)A，B∈Tname，Kbs?Kp，Kas?Kp，Kab?Tname，Na，Nb∈TTname，Na和Nb在Σ中是唯一起源。Yahalom-Paulson協(xié)議的叢圖如圖4所示。

圖4　Yahalom-Paulson協(xié)議叢圖 Fig.4　The bundle of Yahalom-Paulson protocol

5.2Yahalom-Paulson協(xié)議的認證性分析

5.2.1服務(wù)器S對響應(yīng)者B的認證

命題6 假設(shè)C為Yahalom-Paulson的串空間Σ中的一個叢，A≠B，Kas，Kbs?Kp，S∈Cserv[A，B，Na，Nb，Kab]，且其Cheight為1，則C中存在Sr∈Cresp[A，B，Na，**]，其Cheight為2。

證明{ANa}Kbs構(gòu)成主動測試，根據(jù)主動測試定理，C中存在正則節(jié)點m∈C，t為m的分量，A≠B，{ANa}Kbs只能出現(xiàn)在串Sr∈Cresp[A，B，Na，**]的〈Sr，2〉節(jié)點上。命題得證。

5.2.2發(fā)起者A對服務(wù)器S的認證

命題7 假設(shè)Yahalom-Paulson串空間Σ的叢C中，A≠B，Kas?Kp，存在串Si∈Cinit[A，B，Na，Nb，Kab]，且其Cheight為2，則C中存在S∈Cserv[A，B，Na，*，Kab]，且其Cheight為2。

證明〈Si，1〉?〈Si，2〉構(gòu)成Na的輸入測試，測試分量為{BKabNa}Kas，根據(jù)輸入測試定理，C中應(yīng)存在Na的正則變換邊。根據(jù)叢C的消息類型，該變換邊只能在S∈Cserv[A，B，Na，*，Kab]上出現(xiàn)。命題得證。

5.2.3響應(yīng)者B對服務(wù)器S的認證

命題8 假設(shè)Yahalom-Paulson串空間Σ的叢C中，A≠B，Kbs?Kp，存在串Sr∈Cresp[A，B，Na，Nb，Kab]，且其Cheight為3，則C中存在S∈Cserv[A，B，*，Nb，Kab]，且其Cheight為2。

證明〈Sr，2〉?〈Sr，3〉構(gòu)成Nb的輸入測試，測試分量為{ABKabNb}Kbs，根據(jù)輸入測試定理，C中應(yīng)存在Nb的正則變換邊。根據(jù)叢C的消息類型，該變換邊只能在S∈Cserv[A，B，*，Nb，Kab]上出現(xiàn)。命題得證。

5.2.4響應(yīng)者B對發(fā)起者A的認證

命題9 假設(shè)Yahalom-Paulson串空間Σ的叢C中，A≠B，Kbs?Kp，存在串Sr∈Cresp[A，B，Na，Nb，Kab]，且其Cheight為3，則C中存在Si∈Cinit[A，B，*，Nb，Kab]，且其Cheight為3。

證明〈Sr，2〉?〈Sr，3〉構(gòu)成Nb的輸入測試，測試分量為{Nb}Kab，根據(jù)輸入測試定理，C中應(yīng)存在Nb的正則變換邊。根據(jù)叢C的消息類型，該變換邊只能在Si∈Cinit[A，B，Na′，Nb，Kab]上出現(xiàn)，且其Cheight為3。因A與B在參數(shù)Na上未達成直接一致,且Kab在S上是唯一起源，這里使用參數(shù)間接一致性的證明方法，對Si運用命題7，證明叢C中存在S′∈Cserv[A，B，Na′′，Nb′，Kab]，且其Cheight為2。由服務(wù)器串S的形式，Kab起源于〈S′，2〉，因Kab是唯一起源，故〈S′，2〉=〈S，2〉，因此，S′=S，Na′′=Na′，Nb′=Nb。于是，叢C中存在Si∈Cinit[A，B，Na′，Nb，Kab]，且其Cheight為3。命題得證。

6結(jié)束語

采用認證測試方法對Yahalom協(xié)議進行驗證的過程中發(fā)現(xiàn)，協(xié)議中不完整的挑戰(zhàn)-應(yīng)答機制以及認證測試方法在證明方式上的局限性是導(dǎo)致輸入測試不能證明Yahalom協(xié)議的原因。采用間接認證鏈方法，證明了Yahalom協(xié)議，并證明了Yahalom-Paulson協(xié)議的正確性，新的證明方法擴展了輸入測試方法的應(yīng)用范圍。

參考文獻:

[1]GuttmanJD,ThayerFJ.Authenticationtestsandthestructureofbundles[J].TheoreticalComputerScence,2002,283(2):333-380.

[2]ThayerFJ,HerzogJC,GuttmanJD.Strandspaces:whyisasecurityprotocolcorrect[C].LosAlamitos:IEEEComputerSocietyPress,1998:160-171.

[3]ThayerFJ,HerzogJC,GuttmanJD.Strandspaces:provingsecurityprotocolscorrect[J].JournalofComputerSecurity,1999,7(23):191-230.

[4]NeumanBC,StubblebineSG.Anoteontheuseoftimestampsasnonces[J].OperatingSystemsReview,1993,27(2):10-14.

[5]卿斯?jié)h.安全協(xié)議[M].北京：清華大學(xué)出版社，2005:124-127.

[6]PaulsonLC.Relationsbetweensecrets:twoformalanalysesoftheYahalomprotocol[J].JournalofComputerSecurity,2001,9(3):197-216.

[7]楊明，羅軍舟.安全協(xié)議關(guān)聯(lián)性分析[J].通信學(xué)報，2006,27(7):39-45.

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

[9]GuttmanJD.Keycompromise,strandspaces,andtheauthenticationtests[C]//Proceedingsofthe7thConferenceontheMathematicalFoundationsofProgrammingSemantics,ElectronicNotesinTheoreticalComputerScience.London:Springer-Verlag,2001:141-161.

[10]丁萌偉，周清雷，趙東明.Yahalom-Paulson協(xié)議的串空間模型與分析[J].計算機工程與應(yīng)用，2008,44(22):97-99.

[11]BurrowsM,AbadiM,NeedhamRM.Alogicofauthentication[J].ProceedingsoftheRoyalSocietyofLondon,1989,426:223-271.

[12]SyversonP.Ataxonomyofreplayattacks[C]//ProceedingsoftheComputerSecurityFoundationsWorkshop,1994:187-191.

編輯:翁史振