肖躍雷，朱志祥，張勇

一種新的認證協(xié)議自動驗證方法

肖躍雷，朱志祥，張勇

為了實現(xiàn)對認證協(xié)議的自動驗證，首先，通過對認證協(xié)議的協(xié)議主體行為分析，給出了驅動模型（Driving Module，DM）的定義。然后，根據(jù)串空間模型中的常規(guī)者串和攻擊者串分別構建了常規(guī)者DM和攻擊者DM。最后，提出了基于常規(guī)者DM和攻擊者DM的自動驗證算法。實例分析和定理證明表明，該算法的搜索過程不僅是全面和正確的，而且能有效地避免狀態(tài)空間爆炸問題。

自動驗證；驅動模型；串空間模型；認證協(xié)議

0 引言

認證協(xié)議是許多信息系統(tǒng)的安全基礎，因而確保認證協(xié)議的正確性是至關重要的。但是，設計一個正確的認證協(xié)議是一項十分困難的任務。目前許多公布的認證協(xié)議太多都存在著各種各樣的安全漏洞。為了驗證認證協(xié)議的正確性，研究者們提出了許多形式化分析方法。這些形式化分析方法可以分為3類：（1）基于知識邏輯與信念的方法，如BAN邏輯[1]；（2）驗證工具，如Murφ[2]、FDR[3]、NRL[4]和Athena[5]；（3）定理證明的方法，如串空間模型[6-11]。自動驗證工具的優(yōu)點是不需要使用人員是安全專家，而且從驗證結果中可以直觀地看到認證協(xié)議是如何被攻擊的。但是，自動驗證工具通常無法避免狀態(tài)空間爆炸問題。

為了解決這一問題，本文首先分析了認證協(xié)議的協(xié)議主體行為，并定義了驅動模塊（Driving Module，DM），然后，利用串空間模型（Strand Space Model，SSM）構建了常規(guī)者DM和攻擊者DM，最后，提出了基于DM的認證協(xié)議自動驗證算法。通過定理證明和對NSPK協(xié)議[12]的實例分析可知，該自動驗證算法不僅能很快地搜索到認證協(xié)議的安全漏洞，而且能有效地避免狀態(tài)空間爆炸問題。

1 新自動驗證方法

1.1 符號定義

為了分析認證協(xié)議，需要對認證協(xié)議的消息符號進行了一般化定義，本文用到的消息符號為：

Xi：表示協(xié)議主體；

N*：表示未知協(xié)議主體產(chǎn)生的隨機數(shù)；

*：表示僅能驗證其長度的值；

其中，i =1,2,3……。

1.2 驅動模塊

認證協(xié)議是各個協(xié)議主體之間進行的一些事件序列。認證協(xié)議執(zhí)行過程中的協(xié)議主體行為主要為發(fā)送消息和接收消息。任何一個認證協(xié)議都有始發(fā)點和終止點，始發(fā)點發(fā)送消息驅動協(xié)議的進行，終止點接收消息而結束整個協(xié)議執(zhí)行過程。對于認證協(xié)議執(zhí)行過程的中間部分，協(xié)議主體接收消息之后必然發(fā)送新的消息給其他協(xié)議主體，這顯然構成了一個驅動過程。根據(jù)以上對認證協(xié)議執(zhí)行過程的分析，本文給出了驅動模塊（Driven Module）的定義如下：

定義1協(xié)議主體X接收消息或不接收消息而發(fā)送新的消息給其他協(xié)議主體的協(xié)議執(zhí)行過程為一個驅動模塊（Driving Module，DM），X稱為DM的主體。

對于一個認證協(xié)議而言，該協(xié)議的合法參與者稱為常規(guī)者，而非法參與者便稱為攻擊者。若DM的主體為常規(guī)者，則該DM為常規(guī)者DM；否則，該DM為攻擊者DM。

（1）常規(guī)者DM構建

由于常規(guī)者DM的主體為常規(guī)者，而常規(guī)者的協(xié)議執(zhí)行過程必須遵守正常協(xié)議的執(zhí)行規(guī)則，所以常規(guī)者DM可以根據(jù)正常協(xié)議的執(zhí)行過程得到，即可以根據(jù)文獻[6]所述的常規(guī)者串得到。如圖1所示：

圖1 NPSK協(xié)議的常規(guī)串和常規(guī)者DM

例如，NPSK協(xié)議[12]的常規(guī)者串如圖1中的(a)所示，而得到的相應常規(guī)者DM圖1中的(b)所示。

從圖1可知，協(xié)議主體A的常規(guī)者串由常規(guī)者DM①和常規(guī)者者 DM③構成，而協(xié)議主體 B的常規(guī)者串由常規(guī)者DM②和常規(guī)者DM④構成，從而NPSK協(xié)議是由常規(guī)者DM①、常規(guī)者DM②、常規(guī)者DM③和常規(guī)者DM④按序列構成和執(zhí)行的，其中常規(guī)者DM①稱為NPSK協(xié)議的始發(fā)常規(guī)者DM，常規(guī)者DM④稱為NPSK協(xié)議的終止常規(guī)者DM，常規(guī)者DM②和常規(guī)者DM③稱為NSPK協(xié)議的過程常規(guī)者DM。

（2）攻擊者DM構建

攻擊者的能力主要由兩方面因素來描述：一是攻擊者獲得它可掌握的消息；二是攻擊者由它所能掌握的消息產(chǎn)生新消息的能力。根據(jù)文獻[6]所述的攻擊者串，可以得到如下攻擊者DM：

①發(fā)送文本項：<+t>；

②發(fā)送密鑰項：<+K>；

③級聯(lián)各組件為消息：<-h1，-h2，-…， +h>；

④分割消息為各組件：<-h，+h1，+h2，+…>；

⑤加密消息：<-K，-h，+{h}K>；

⑥解密消息：<-{h}K，- K-1，+ h>。

其中，h1、h2、…為h的各個組件[7]，h為消息，K為加密密鑰，K-1為解密密鑰。本文用到的組件是指文本項、密鑰項或加密項。

1.3 自動驗證算法

由DM的定義可知，任何協(xié)議過程都可以描述成一系列DM過程。因此，不管是正常協(xié)議還是攻擊協(xié)議（通常稱為攻擊劇本），都可利用以上定義的DM描述出來。為了得到這些攻擊劇本，本文基于DM對協(xié)議過程執(zhí)行自底向上的自動驗證。自動驗證機理如圖2所示：

圖2 自動驗證機理

其中m1、m2、m、r1、r2、s1、s2為消息項，①表示父結點DM的接收消息都由常規(guī)者DM發(fā)送，②表示父結點DM的接收消息都由攻擊者DM發(fā)送，③表示父結點DM的接收消息由常規(guī)者DM和攻擊者DM共同發(fā)送。

按照圖2所示的自動檢驗機理，對安全協(xié)議的自動檢驗可以形成一個DM結點搜索樹。DM結點搜索樹的每一條搜索路徑稱為DM結點路徑。這些DM結點路徑包括正常協(xié)議的DM結點路徑和攻擊協(xié)議的DM結點路徑(攻擊劇本的過程)。自動驗證算法的具體過程如下：

以認證協(xié)議的終止常規(guī)者DM為根結點DM，依據(jù)根結點DM中接收消息的格式分別搜索該協(xié)議的常規(guī)者DM集和攻擊者DM集，并按自動驗證機理生成各個子結點DM，然后以可得到的各子結點DM為父結點DM再作類似的搜索，直至生成的子結點DM數(shù)為零，其中搜索過程必須滿足以下條件：

（1）協(xié)議的假設條件；

（2）搜索攻擊者DM中的④或⑥時，要保證它們的接收消息在分割消息集和解密消息集中；

（3）同一條DM結點路徑上不能出現(xiàn)兩個相同的DM；

（4）同一條DM結點路徑上不能出現(xiàn)兩個互成逆過程的攻擊者DM。

分割消息集是指各常規(guī)者 DM的發(fā)送消息經(jīng)過直接分割或分割和解密組合的間接分割過程可獲得到消息集。解密消息集是指各常規(guī)者 DM的發(fā)送消息經(jīng)過直接解密或分割和解密組合的間接解密過程可獲得到消息集。

最后，根據(jù)文獻[6]中的協(xié)議正確性定義判定哪些 DM結點路徑是正常協(xié)議執(zhí)行過程，哪些DM結點路徑是攻擊劇本執(zhí)行過程，哪些DM結點路徑是無效攻擊過程。

2 應用實例

其中， A和B表示常規(guī)者（發(fā)起者和響應者），P表示攻擊者。由于認證協(xié)議的終止常規(guī)DM在自動驗證算法中是明確描述的根結點 DM，所以上述 NSPK協(xié)議的終止常規(guī)DM是明確描述的。

本文利用 C語言實現(xiàn)上述自動驗證算法，通過輸入NSPK協(xié)議的假設條件和各個常規(guī)DM的一般化描述，最終得到NSPK協(xié)議的DM結點搜索樹，如圖3所示：

圖3 NPSK協(xié)議的DM結點搜索樹

在圖3的DM結點搜索樹中，各個DM結點值為：1. <-

分析圖3可知，DM結點①的最左邊的分支樹為NSPK協(xié)議的正常協(xié)議過程，而右邊的 3條分支樹分別構成了NSPK協(xié)議的3個攻擊劇本。這3個攻擊劇本的攻擊效果是一致的，與文獻[3]中分析結果相同，從而說明該自動驗證算法是有效的。

3 分析與討論

下面將證明該自動驗證算法的搜索過程不僅是全面和正確的，而且能夠有效地避免狀態(tài)空間爆炸問題。

定理1 對某個接收消息搜索常規(guī)DM就是搜索常規(guī)者可以發(fā)送該消息的能力。

證明：由于常規(guī)DM是根據(jù)常規(guī)者串而得到的，所以常規(guī)DM代表了常規(guī)者發(fā)送消息的能力。常規(guī)DM空間是由各個常規(guī)DM構成的，而常規(guī)者串空間是各個常規(guī)者串構成的，所以搜索各個常規(guī)DM就相當于搜索各個常規(guī)者串，即搜索常規(guī)者可以發(fā)送該消息的能力。因此，對某個接收消息搜索常規(guī)DM就是搜索常規(guī)者可以發(fā)送該消息的能力。

定理2對某個接收消息搜索攻擊DM就是搜索攻擊者可以發(fā)送該消息的能力。

證明：由于攻擊 DM是根據(jù)文獻[6]中的攻擊者串而得到的，其中攻擊DM①與文獻[6]中的攻擊者串M相同，攻擊DM②與文獻[6]中的攻擊者串K相同，攻擊DM③與文獻[6]中的攻擊者串C等價，攻擊DM④與文獻[6]中的攻擊者串S等價，攻擊DM⑤與文獻[6]中的攻擊者串E相同，攻擊DM⑥與文獻[6]中的攻擊者串D相同，而文獻[6]中的攻擊跡F和T直接隱含在DM搜索過程中，所以對某個接收消息搜索攻擊DM就是搜索攻擊者可以發(fā)送該消息的能力。

定理3 自動驗證算法是全面的和正確的。

證明：自動驗證算法是對每個接收消息搜索常規(guī)DM和攻擊DM，從定理1和定理2可知該自動驗證算法是全面的。搜索條件（1）是協(xié)議的假設條件，搜索條件（2）是根據(jù)協(xié)議常規(guī)DM能力來描述攻擊者分割和解密消息的能力，搜索條件（3）和（4）是用于避免循環(huán)搜索的。這些搜索條件都是合理和正確的。因此，自動驗證算法是全面的和正確的。

定理4 自動驗證算法能有效地避免狀態(tài)空間爆炸。

證明：自動驗證算法采用自底向上的搜索方式，而每一條搜索路徑總是收斂于搜索條件（1）～（4），所以可有效地避免了狀態(tài)空間爆炸問題。

4 總結

本文提出了一種新的認證協(xié)議自動驗證方法。首先，通過對認證協(xié)議的協(xié)議主體行為分析，給出了DM的定義。然后，根據(jù)串空間模型中的常規(guī)者串和攻擊者串分別構建了常規(guī)者DM和攻擊者DM，它們分別代表了認證協(xié)議的常規(guī)者能力和攻擊者能力。最后，提出了基于常規(guī)者DM和攻擊者DM的自動驗證算法，并基于串空間模型中的正確性定義判定哪些DM結點路徑是正常協(xié)議執(zhí)行過程，哪些DM結點路徑是攻擊劇本執(zhí)行過程，哪些DM結點路徑是無效攻擊過程。此外，通過定理證明和對NSPK協(xié)議的實例分析可知，該方法的搜索過程是全面和正確的，而且能夠有效地避免了狀態(tài)空間爆炸問題。

[1] Burrows M, Abadi M, Needham R. A logic of authentication[J]. ACM Transactions on Computer System, 1990, 8(1):18-36.

[2] Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Murφ[A]. Proceedings of the 1997 IEEE Symposium on Security and Privacy[C]. USA: IEEE Computer Society Press, 1997：141-151.

[1] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[A]. Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science[C]. Beilin: Springer Verlag, 1996：147-166.

[2] Meadows C. The NRL Protocol Analyzer: an overview [J]. Journal of Logic Programming, 1996, 26(2):113-131.

[3] Song D. Athena: A new efficient automated checker for security protocols analysis [A]. Proceedings of the 12th IEEE Computer Security Foundations Workshop[C]. IEEE Computer Society Press, 1999：192-202.

[4] Thayer F. Herzog J C. Guttman J D. Strand space: why is a security protocol correct?[A]. Proceedings of the 1998 IEEE Symposium on Security and Privacy[C]. New York: IEEE Computer Press, 1998：160-171.

[5] Guttman JD, Thayer FJ. Authentication tests [A]. Proceedings of the 2000 IEEE Symposium on Security and Privacy[C].IEEE Computer Society Press, 2000：150～164.

[6] 董學文,馬建峰,牛文生,等. 基于串空間的 Ad Hoc安全路由協(xié)議攻擊分析模型[J]. 軟件學報，2011，22(7)：1641-1651.

[7] 泰彬彬,王俊芳. 基于串空間認證測試的 DTLS協(xié)議認證性分析[J]. 計算機與網(wǎng)絡，2014，40(496)：51-55.

[8] 吳名歡,程小輝. Casper/FDR和串空間在物聯(lián)網(wǎng)通信協(xié)議中的形式化分析[J]. 桂林理工大學學報，2014，34(2)：338-344.

[9] Xiao Y L, Wang Y M, Pang L J. A Verification of trusted networkaccess protocols in the strand space model[J]. IEICE Transactions onFundamentals of Electronics, Communications and Computer Sciences, 2012, E95-A(3)：665-668.

[10] NeedhamR, Schroeder M. Using encryption for authenticationin large networks of computers [J]. Communicationsof the ACM, 1978，21(12)：993-999.

TP393.08文獻標志碼：A

2015.04.11）

1007-757X (2015)08-0004-03

國家自然科學基金（61402367）；陜西省信息化技術研究項目（2013-008）；西安郵電大學青年教師科研基金項目（401-1201）

肖躍雷（1979-），男，漢族，江西吉安人，西安郵電大學，物聯(lián)網(wǎng)與兩化融合研究院，講師，博士后，研究方向：可信計算、安全協(xié)議分析與設計、無線網(wǎng)絡安全，西安，710061；朱志詳（1959-），男，,漢族，西安郵電大學，物聯(lián)網(wǎng)與兩化融合研究院，教授，博士，研究方向：多媒體通信，信息化應用，網(wǎng)絡安全，西安，710061；張勇（1974-），男，,漢族，西安郵電大學，物聯(lián)網(wǎng)與兩化融合研究院，高工，博士，研究方向：信息安全，云計算與儲存技術，西安，710061；