一種新的認證協議自動驗證方法

肖躍雷，朱志祥，張勇

一種新的認證協議自動驗證方法

肖躍雷，朱志祥，張勇

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

自動驗證；驅動模型；串空間模型；認證協議

0 引言

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

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

1 新自動驗證方法

1.1 符號定義

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

Xi：表示協議主體；

N*：表示未知協議主體產生的隨機數；

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

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

1.2 驅動模塊

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

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

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

（1）常規者DM構建

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

圖1 NPSK協議的常規串和常規者DM

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

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

（2）攻擊者DM構建

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

①發送文本項：<+t>；

②發送密鑰項：<+K>；

③級聯各組件為消息：<-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的定義可知，任何協議過程都可以描述成一系列DM過程。因此，不管是正常協議還是攻擊協議（通常稱為攻擊劇本），都可利用以上定義的DM描述出來。為了得到這些攻擊劇本，本文基于DM對協議過程執行自底向上的自動驗證。自動驗證機理如圖2所示：

圖2 自動驗證機理

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

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

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

（1）協議的假設條件；

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

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

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

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

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

2 應用實例

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

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

圖3 NPSK協議的DM結點搜索樹

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

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

3 分析與討論

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

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

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

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

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

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

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

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

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

4 總結

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

[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安全路由協議攻擊分析模型[J]. 軟件學報，2011，22(7)：1641-1651.

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

[8] 吳名歡,程小輝. Casper/FDR和串空間在物聯網通信協議中的形式化分析[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-），男，漢族，江西吉安人，西安郵電大學，物聯網與兩化融合研究院，講師，博士后，研究方向：可信計算、安全協議分析與設計、無線網絡安全，西安，710061；朱志詳（1959-），男，,漢族，西安郵電大學，物聯網與兩化融合研究院，教授，博士，研究方向：多媒體通信，信息化應用，網絡安全，西安，710061；張勇（1974-），男，,漢族，西安郵電大學，物聯網與兩化融合研究院，高工，博士，研究方向：信息安全，云計算與儲存技術，西安，710061；