蘇桂平 ，孫 莎

(1.中國科學院研究生院 信息科學與工程學院，北京 100049；2.中國科學院研究生院 工程教育學院，北京 100049)

如何在一個無法確定的操作環(huán)境下，保證計算機間傳送信息的安全性，從而確保通信雙方主體之間的“信任”以及通信數(shù)據(jù)的秘密和完整，其中安全協(xié)議對保障網絡安全起到至關重要的作用。但一些著名的協(xié)議在使用了相當長的時間后，相繼被發(fā)現(xiàn)存在有若干安全漏洞。由于安全協(xié)議的運行是處于某種不安全的環(huán)境中，很難用人工識別的方法來分析其安全性，必須借助形式化的分析方法或工具來完成。

關于安全協(xié)議的形式化分析，國內外學者基于不同的模型進行了不少有益的研究。如Yasinsac提出的通用安全協(xié)議分析語言CPAL[1]、Millen開發(fā)的通用認證協(xié)議說明語言CAPSL[2]、李夢君等人用擴展Horn邏輯模型對安全協(xié)議進行分析和驗證方法[3]、懷進鵬等人用代數(shù)模型來研究協(xié)議的安全性[4]、WE等人基于有色 Petri網CPN(Coloured Petri Net)提出一種集成的安全協(xié)議分析模型[5]。

現(xiàn)有的方法大多針對個別協(xié)議進行分析，很少能夠通用于大部分的安全協(xié)議，并且大部分的方法還停留在理論上，缺少自動分析的工具[6]。

本文利用CPN tools建模語言(CPN ML)中的查詢函數(shù)對安全屬性進行描述，然后對CPN tools工具在規(guī)范協(xié)議描述、簡化協(xié)議建模、自動檢測進行擴展三方面，搭建一個能夠覆蓋大部分安全性質的CPN查詢函數(shù)庫，提出一種基于CPN的通用和規(guī)范的安全協(xié)議形式化分析語言，該語言可以像用面向對象編程語言編程一樣對安全協(xié)議進行建模。

1 基于CPN的安全協(xié)議

1.1 有色Petri網(CPN)理論研究

Petri網是一種可用于多種系統(tǒng)的圖形化、數(shù)學化建模工具，為描述和研究具有并行、異步、分布式和隨機性等特征的復雜系統(tǒng)提供了強有力的手段。

作為一種圖形化工具，可以把Petri網看作與數(shù)據(jù)流圖和網絡相似的方法來描述系統(tǒng)模型；作為一種數(shù)學化工具，它可以用來建立狀態(tài)方程、代數(shù)方程和其他描述系統(tǒng)行為的數(shù)學模型。

在CPN模型中，有色標志表示系統(tǒng)中不同的資源，同時每個位置都與特定的顏色集綁定，表示該位置中只能存放相應顏色的標志。在弧上和變遷上標注的條件表達式和運算函數(shù)是用于解釋弧的權值、運算所用的顏色以及變遷觸發(fā)的條件。

CPN tools是一個專用于有色Petri網編輯、模擬和分析的工具，除了有強大的CPN分析工具外，它還有簡潔緊湊的CPN圖形編輯工具，幾乎所有的CPN元素(除數(shù)據(jù)類型、變量申明外)都能在模型圖中表示。

CPN是將Petri網具有相似性質的元素分類，用不同顏色區(qū)分不同類別，每一種顏色用一種標識符號來表示，將某種屬性賦予標記。

CPN=(Σ，P，T，A，N，C，G，E)，在 CPN 的一個狀態(tài) M下，t上的綁定元素(t，b)是可實施的，當且僅當：

若把t實施之后產生的后繼狀態(tài)定義為M′，則：

可以稱作M′是從 M出發(fā)，經過(t，b)變遷是可達的，記為M[(t，b)>M′。如果存在一個變遷σ序列使得M可以達到狀態(tài) M′，則記為 M[σ>M′，由 M出發(fā)的所有可達狀態(tài)的集合表示為[M>。

矩陣方程：

其中， 矩陣 C=?cij」(1≤i≤n，1≤j≤m) 是 CPN 的 關聯(lián)矩 陣，cij=Wtj，si-Wsi，tj、Wtj，si和 Wsi，tj是 弧 權 。

利用矩陣方程可以判斷不安全狀態(tài)的可達性。

在安全協(xié)議形式化分析方面，CPN具有其獨特的優(yōu)勢：(1)將分層思想與數(shù)據(jù)結構結合；(2)對時間因素的靈活描述；(3)強大的仿真及狀態(tài)分析自動工具；(4)有效的化簡方法。

1.2 基于CPN的安全協(xié)議

安全協(xié)議的形式化分析與驗證是一個復雜的過程，首先都要用形式化方法的語義對安全協(xié)議進行描述與建模。然而，從協(xié)議的非形式化描述，尤其是自然語言描述轉變成形式化說明的過程可能會有錯誤發(fā)生，將直接導致后續(xù)分析的不確定性。同時一些形式化方法的提出都是從個別安全協(xié)議出發(fā)來設計規(guī)范的術語，遇見了新的協(xié)議形式，再對原有規(guī)范加以擴展，這樣的形式化術語存在通用性差的問題。所以在進行安全協(xié)議的形式化描述與建模之前，需要采用通用的安全協(xié)議形式化說明加以規(guī)范。

為了使得通用安全協(xié)議說明更加適合于Petri網方法，本文在CAPSL的基礎上抽象出通用安全協(xié)議的基本要素，在此基礎上建立與Petri網要素的一一對應，如表1所示。

表1 CPN元素與安全協(xié)議基本元素對照表

2 對安全協(xié)議的描述和函數(shù)庫的創(chuàng)建

CPN tools提供給每個變遷一個用CPN ML語言編程的程序編輯區(qū)。當變遷發(fā)生時，執(zhí)行所編輯的程序，完成所需的功能。程序編輯區(qū)有三條固定的語句：input()、output()、action()，分別表示輸入?yún)?shù)、輸出參數(shù)和執(zhí)行語句。

2.1 用CPN ML語言對安全屬性進行描述

安全協(xié)議的重要安全性質包括：機密性、認證性、完整性。描述如下：

機密性：針對受保護的特定內容t的泄密狀態(tài)來進行定義：

該函數(shù)表示搜索所有的狀態(tài)結點，如果有結點滿足斷言函數(shù)fn，說明機密信息t泄露。

認證性：實體經過解密或者驗證簽名來實現(xiàn)認證，并在其緩沖區(qū)中保留認證成功的證據(jù)，類型為AUT的顏色集colset AUT=with auth；同時保留被認證者的身份的名稱。用查詢函數(shù)來定義：

完整性：安全協(xié)議確保交互的消息不能被篡改、刪除和替代，或者至少消息的改變是可以被發(fā)現(xiàn)的。用形式化定義來表示：

2.2 搭建安全協(xié)議的CPN查詢函數(shù)庫

先建立好一個函數(shù)模型庫，對應于常見的密碼學操作，并不斷地擴展。上層實體通過函數(shù)調用的方式，利用分層建模的設置子頁面工具將上層操作變遷與函數(shù)對應起來。

通用安全協(xié)議的功能層其實就是安全協(xié)議函數(shù)庫，即在底層先建立好一個函數(shù)模型庫，對應于常見的密碼學操作，并不斷地擴展。上層實體只需要通過函數(shù)調用的方式，利用分層建模的設置子頁面工具將上層操作變遷與函數(shù)對應起來就可以了。

在上面描述和對擴展的基礎上，建立一個安全性質查詢函數(shù)庫。本文建立了一個能夠覆蓋絕大部分安全性質的查詢函數(shù)庫，用戶只需要調用相應函數(shù)即可完成協(xié)議的相關安全性質的檢查而不需要自己利用CPN ML語言編寫查詢函數(shù)。

2.3 一種基于CPN的通用安全協(xié)議形式化分析方法

本項目利用前面基于CPN的安全協(xié)議描述、對CPN tools的擴展、CPN的安全協(xié)議操作函數(shù)庫的建立，再結合實體模型中類似面向對象的類、派生對象概念，利用通用和規(guī)范的方法建模，提出一種基于CPN的通用安全協(xié)議形式化分析語言，該語言使用時就像用面向對象編程語言進行編程一樣方便有效。

基于CPN的安全協(xié)議形式化分析語言工作流程圖如圖1所示。

圖1 基于CPN的安全協(xié)議形式化分析語言工作流程圖

針對具體協(xié)議，將安全屬性用CPN ML查詢函數(shù)進行形式化描述：首先用斷言函數(shù)定義不安全狀態(tài)，即協(xié)議滿足安全屬性時不可能出現(xiàn)的狀態(tài)，如會話密鑰泄露時的狀態(tài)；再定義搜索函數(shù)對狀態(tài)空間的所有狀態(tài)進行斷言函數(shù)的測試，尋找符合的結點標識；最后運行搜索查詢函數(shù)，分析實驗結果。

3 應用舉例

本文以ASW(Asokan-Shoup-Waidner)協(xié)議為例，利用本文提出的基于CPN模型對協(xié)議的安全性進行分析。

3.1 基于CPN模型對協(xié)議建模

ASW 協(xié) 議 由 exchange、abort、resolve_A 和resolve_B 4個子協(xié)議構成。在正常情況下，只執(zhí)行exchange子協(xié)議。僅當A或B認為協(xié)議執(zhí)行出現(xiàn)問題時，才執(zhí)行其他子協(xié)議。

協(xié)議的exchange子協(xié)議具體描述如下：

其中，Na、Nb分別為 A與 B生成的臨時值；m為 A向 B發(fā)送的電子郵件；C={m，Na，Ka，Kb}Kttp是加密電子郵件。

圖2 ASW協(xié)議的Alice模型

在exchange子協(xié)議中，如圖2所示，Alice生成me1并發(fā)送給B。如果A在合理的時間范圍內沒有收到me2，A將異常終止協(xié)議；否則，A將me3發(fā)送給B。如果等待me4的時間超時了，A將異常終止協(xié)議并激活resolve_A子協(xié)議；否則，exchange子協(xié)議成功運行結束。函數(shù)gen_time(result)隨機生成了一個延遲時間。條件if temptime

3.2 分析和驗證

本文分別針對在exchange子協(xié)議異常終止和正常結束的兩種情況下進行模型檢測。因此在計算完全部狀態(tài)空間后，修改了函數(shù)fun Verif_Fairness，分別執(zhí)行了以下兩個ML查詢函數(shù)：

函數(shù)fun Verif_Fairness_suc查詢的是在exchange子協(xié)議正常結束的情況下，是否有不滿足公平性的狀態(tài)。結果為0，說明當exchange子協(xié)議成功結束后，協(xié)議滿足可追究性和公平性。相反，fun Verif_Fairness_fail的查詢結果列出了一些不安全狀態(tài)，說明當協(xié)議異常終止后，不滿足安全性。

本文將面向對象方法及其概念(如類、對象、函數(shù)等)引入建模中，并直接嵌入通用安全協(xié)議描述中，以此為基礎的協(xié)議建模就具有了抽象、重用、繼承等性質，簡化了建模過程，使得圖型化的CPN建模能夠像面向對象編程語言一樣方便和有效。利用CPN tools提供的復制和分層次工具實現(xiàn)函數(shù)調用以及派生實體的快速建模，將面向對象思想中的派生實體與函數(shù)調用思想應用于建模過程中。本文提出通用的安全協(xié)議分析語言，具有通用性、易用性、圖形化等特點。

[1]李夢君，李舟軍，陳火旺.安全協(xié)議的擴展Horn邏輯模型及其驗證方法 [J].計算機學報，2006，29(9)：1666-1678.

[2]懷進鵬，李先賢.密碼協(xié)議的代數(shù)模型及其安全性[J].中國科學(E 輯)，2003，33(12).

[3]馮登國，范紅.安全協(xié)議理論與方法[M].北京：科學出版社，2003.

[4]YASINSEC A.A formal semantics for evaluating cryptographic protocols[D].University of Virginia，1996.

[5]MILLEN J.CAPSL： common authentication protocol specification language[R].Technical Report MP97B48，The MITRE Corporation，1997.

[6] WeiJin， Su Guiping.An integrated modelto analyze cryptographic protocols with colored Petri Nets.In Proceeing[C].11th IEEE Symposium on High Assurance Systems Engineering Symposium，2008.