技術領域

本發明涉及網絡安全協議領域，特別是涉及一種多方合同簽署協議公平性驗證技術。?

背景技術

隨著計算機網絡技術的發展和電子商務的普及，電子商務協議變得越來越重要，合同簽署協議作為電子商務協議的一個重要分支，對其技術實現結果的公平性問題受到了研究者的廣泛關注。其公平性包含兩種情況，一種是所有的協議參與者都獲得了自己期望的信息，另一種是所有的協議參與者都沒有獲得自己期望的信息。?

與傳統的安全協議相比，多方合同簽署協議復雜度較高，消息交換數量較多，并且消息發送方在協議執行上占有優勢，因此公平性更難以理解和分析。現有的比較成熟的多方合同簽署協議分析方法主要有邏輯推理、歸納法證明、串空間模型以及ATS模型檢測方法，它們各有側重點和優勢，但自動化程度較低，時空復雜度較高，也不能給出可視化攻擊路徑。?

發明內容

為了克服上述現有技術存在的問題，本發明提出一種基于CSP#和LTL邏輯的多方合同簽署協議公平性驗證方法，多方合同簽署協議的公平性驗證為出發點，用CSP#和LTL邏輯對多方合同簽署協議進行建模，并針對狀態空間爆炸問題給出了狀態約減規則，最后在PAT平臺驗證協議的公平性并給出攻擊路徑。?

本發明提出的一種基于CSP#和LTL邏輯的多方合同簽署協議公平性驗證方法，該方法包括以下步驟：?

步驟1、用CSP#語言對多方合同簽署協議進行建模，建立的協議結構模型為Kripke四元組M，令AP為原子命題集合M=(S,S0,R,L)，其中：S是協議狀態的有限集合；是協議初始狀態的集合；是狀態轉移函數；L：S→2^AP是標記函數，用于標記在某個狀態下位真的原子命題的集合；?

并且，該模型滿足以下假設，即：假設一：協議參與者之間的信道是不可靠的，即傳輸的消息可能會延遲或者丟失。但參與者與可信第三方之間的信道是可恢復信道；假設二：協議參與者可能是不誠實的，但多個參與者中至少有一個是誠實的，可信第三方是誠實的。誠實的參與者將嚴格按照協議規定執行操作，不誠實者也可以是合法用戶，擁有自己的公鑰和私鑰，以及定義針對協議的不誠實參與者是安全的；?

步驟2、對于協議系統S，用LTL線性時序邏輯可以將協議參與者P_i的公平性描述，模型表示如下：?

強公平性模型：?

弱公平性模型：?

根據上述公式P_i的公平性描述為：在協議中止時，如果P₁，P₂，...，P_i-1，P_i+1，...，P_n中的任意一位參與者獲得了P_i的數字簽名則一定存在一條路徑使得P_i能夠獲得P₁，P₂，...，P_i-1，P_i+1，...，P_n對合同m的簽名；然后進行上述模型檢測的狀態約減，即采用Move-One-Step方法根據操作語義規則產生所有可以轉換到目標狀態的中間狀態，并以Encode-State方法為基礎對目標狀態進行布爾公式編碼。?

所述模型檢測的狀態約減，具體包括以下處理：?

減去系統不可達狀態，降低狀態搜索時間；?

合并本質相同的狀態，壓縮狀態空間；以及?

刪除一定導致協議公平性的狀態，便于攻擊路徑的跟蹤。?

所述步驟（2）之后還包括PAT平臺上的模型檢測，給出公平性驗證和可視化攻擊路徑的步驟。?

與現有技術相比，本發明只需在協議規則的基礎上，輸入協議CSP#模型和LTL公平性描述，即可實現公平性自動驗證，操作簡單，能夠切實驗證協議性質；并針對狀態空間爆炸問題給出了狀態約減規則，較好的完成了狀態分支約減，同時減小了時空復雜度。并給出自動跟蹤攻擊路徑來方便協議的改進和完善。?

該方法預期達到以下有益效果：?

1、本發明使用LTL邏輯描述協議公平性，給出模型檢測壓縮狀態空間，提出狀態約減規則對狀態剪枝，緩解了狀態爆炸問題；?

2、本發明支持進程間的直接轉換，無需進行不必要的狀態匹配搜索，降低了協議分析的時間復雜度；?

3、如果協議存在公平性缺陷，本文將跟蹤該路徑，并給出可視攻擊路徑，便于協議的改進與完善；?