基于SPIN的安全協議形式化驗證方法

導語：基于SPIN的安全協議形式化驗證方法一文來源于網友上傳，不代表本站觀點，若需要原創文章可咨詢客服老師，歡迎參考。

1引言

隨著計算機技術的發展，人類進入了信息時代，信息技術已經滲透到了人們日常生活的方方面面，然而信息在開放的網絡環境中傳輸會遭到各種各樣的攻擊，如偷聽攻擊、截取攻擊、偽造攻擊、篡改攻擊等。這些攻擊的存在在不同程度上損害了網絡用戶的利益。因此為了確保信息安全，人們設計出了安全協議來保證通信過程的安全可靠。安全協議是一個分布式算法，它規定了兩個或兩個以上的協議主體在一次通信過程中必須要執行的一系列步驟。利用安全協議人們來實現在開發網絡中的安全通信?？梢哉f安全協議是信息安全的基礎，其自身的安全問題已成為安全研究的重要內容。目前，在安全協議驗證領域存在多種驗證方法如模擬、形式化等，模擬的方法存在不能100%覆蓋的缺陷，而形式化能夠達到覆蓋率100%而且具有嚴密的數學基礎，因而越來越受到業內人士的信賴。形式化驗證主要有兩種驗證方法定理證明和模型檢測兩種方法。定理證明的基本思想是將安全協議描述為公理系統，安全協議的安全目標則表示成需要證明的定理，安全協議是否符合安全目標則對應于公理系統中的目標定理是否成立。定理證明的最大優勢是協議運行期間不會出現狀態爆炸的問題。缺點是，對使用者的技術要求較高，需專業人士才能駕馭，而且自動化程度不高，需要人工干預。模型檢測的基本思想是，把安全協議看成一個分布式系統，單個協議實體涉及的協議執行部分為局部狀態，所有局部狀態構成了分布式系統的全局狀態。在安全協議的全局狀態上定義安全屬性，安全協議是否滿足安全屬性等價于系統可達的每個全局狀態上安全屬性都能夠得到滿足。模型檢測可實現全自動的執行，人的干預較少操作簡單易實行，但模型檢測會出現狀態空間爆炸的情況，這種情況制約了模型檢測技術的發展。SPIN這種模型檢測工具利用on-the-fly技術可以有效的緩解狀態空間爆炸問題，SPIN模型檢測工具的基本思想是將協議表示成一自動機的形式，并且將待驗證屬性表示為另一自動機，然后求這兩個自動機的同步積。通過遍歷求同步積后產生的新的狀態機的整個狀態空間，檢查協議是否滿足我們期望的性質描述。如果不滿足則返回錯誤并提供導致錯誤的狀態遷移路徑，我們將通過錯誤路徑來定位錯誤。本文詳細介紹了模型檢測工具SPIN的工作原理，并給出了一個基于spin模型檢測工具的簡單安全協議的形式化描述和分析。

2SPIN的工作原理

SPIN作為一種驗證反應式并發系統邏輯一致性的工具，已廣泛應用到航空、核電、網絡信息安全等眾多領域中。它首先把用Promela建模語言，通過進程、變量和消息通道等描述的待驗證系統，以及以LTL或斷言描述的待驗證屬性，作為輸入，然后把Promela描述的待驗證系統中每個進程轉化為一個有限自動機并對這些有限自動機進行異步積運算得到優先自動機A，同時把LTL表達式取反并轉換為一個自動機B，最后對自動機A和自動機B進行同步積運算得到自動機C。SPIN通過內嵌的搜索算法對自動機C進行窮盡搜索，在搜索的過程中SPIN通過on-the-fly技術以及偏序簡化技術對狀態空間進行簡化，當搜索完畢顯示自動機C所能接受的語言為空，表示待驗證系統滿足LTL表達的屬性，反之則不滿足。若在檢測過程中，發現了違背待驗證屬性的反例，返回到交互模擬執行狀態再繼續仔細診斷，定位錯誤原因。

2.1待驗證屬性的描述

對于待驗證屬性的描述一般使用LTL公式。LTL就在命題邏輯的基礎上加入了時序操作符：G：表示永遠為真。F：表示最終為真。X：表示下一個時刻為真。U：表示直到某刻前一直為真。R：表示到了某刻才為真。時序邏輯只在乎事件發生的先后順序，不在乎事件發生的時間間隔。每一個LTL公式都可以表達為一個buchi自動機，在SPIN中用neverclaim來描述buchi自動機。時序邏輯提高了對于系統在時間順序上的行為的公式化描述，有了這些操作符，我們就可以方便地描述系統的時態性質了。斷言也可以作為一種描述待驗證屬性的方法，如可以驗證在某個狀態下某個性質是否成立，是否存在無意義的空轉等。

2.2Promela(PROcessMetaLanguage)建模語言

Promela語言不是一種設計語言，它是一種系統描述語言。它是用來對有限狀態系統進行建模的形式描述語言．由于Promela提供對數據結構與c代碼嵌入方面的支持，可以很好地形式化描述協議．一個Promela(processmetalanguage)模型由類型(type)、通道(channe1)、變量(variable)與進程(process)構成。Promela允許動態創建并行的進程，并且可以在進程之間通過消息通道進行同步或異步通信．同步使用會面點(rendezvousport)進行通信，而異步使用緩沖(bufers)進行通信．由此可以看出它是一種面向反應式系統的描述語言,而安全協議屬于典型的反應式系統，因此用Promela語言來描述協議系統是可行的、方便的。對于待驗證屬性我們可行使用LTL、never以及斷言等來描述。

3用SPIN驗證協議的過程

基于SPIN的安全協議驗證，我們首先依據Dolev-Yao模型構造協議主體及攻擊者模型然后對它們進行交叉復合來構造整個模型。協議的一次運行包括所有協議主體所有動作的交叉序列。主要步驟:(1)用Promela語言描述各個協議主體，定義協議的各個元素的數據類型，定義協議主體的行為動作。由于各個協議主體具有并發性，因而使用進程來描述各個協議主體。在進程內部通過協議的各個元素及協議主體的行為動作對協議主體進行描述，進程與進程間通過信道進行交互。(2)以進程的形式為系統增加工具者。根據Dolev-Yao模型假設攻擊者能夠監聽和截取網絡中的每一條消息而且能夠向其他協議主體發送新的消息。依據攻擊者假設通過協議的各個元素及攻擊者的行為動作對攻擊者進行Promela描述(3)用LTL公式描述協議需要驗證的數據機密性屬性要求。(4)運行SPIN進行語法檢查。(5)運行SPIN驗證器進行屬性驗證(6)觀察協議的運行結果，發現協議的問題。SPIN可以產生一個錯誤跟蹤文件，我們能夠根據這個文件通過SPIN提供的模擬功能還原協議執行時產生的問題。

4實例分析

4.1協議的簡化的描述

在用戶Alice和Bob不知道對方私鑰的情況下，用戶Alice希望采用公鑰密碼技術向Bob發送一條秘密消息，協議使用RSA公鑰加密算法。該協議利用了RSA算法加密和解密是互反而且可交換的性質。協議流程如下：（1）Message1:Alice-Bob:{X}pk_Alice（2）Message2:Bob-Alice:{{X}pk_Alice)pk_Bob（3）Message3:Alice-Bob:{X}pk_Bob其中Alice,Bob是協議的通信個體，其中Alice為協議的發起者，Bob為協議的響應者。X為發送的消息。pk_Alice,pk_Bob分別是Alice和Bob的公鑰，用于加密消息。協議流程如下：首先，發起者Alice將消息X用自己的公鑰加密后發送給Bob,然后當Bob接收Alice發來的秘文消息后，由于它沒有Alice的私鑰，所以不能解讀收到的消息，它用自己的公鑰將接收到的密文消息再次加密后發送給Alice。Alice根據RSA算法的交換性質解除自己的加密后得到{X}pk_Bob，并將該消息發送給用戶Bob，用戶Bob接收到該消息后，利用自己的私鑰解密，從而得到消息X。表面上看，通過該協議用戶Alice和Bob可以進行安全通信；然而事實上是攻擊者Eve可以通過截獲Alice和Bob之間的消息，并插入一些自己的消息來達到獲取機密信息甚至是破壞的目的。

4.2協議的系統模型以及Promela描述

以Dolev-Yao模型為依據對協議系統進行建模。假設協議主體在擁有了正確的秘鑰時才可以解碼，并且產生的密文必須擁有相應的明文和秘鑰，攻擊者無法破譯密碼，但是他可以在任意時刻對任意信道截獲密文，也可以再任意時刻對任意信道發送密文。這樣可以看出系統中應有三個進程，消息發起者進程，消息響應者進程，攻擊者進程。進程之間通過信道來通信。定義Promela程序的數據類型:chanch1=[1]of{byte,byte,byte,byte};chanch2=[1]of{byte,byte,byte,byte};typedefMsg{bytecode1,code2,code3,message};Msgsrc_Alice,rev_Alice,src_Bob,rev_Bob,src_Eve,rev_Eve;byteOK;其中，ch1,ch2為通信主體接收、發送數據通道。Msg為信息格式，code1、code2、code3分別Alice,Bob,Eve的加密區，即當code1為1表示消息被加密Alice，其他情況以此類推。src_Alice為Alice發送區，rev_Alice為Alice接收區，src_Bob為Bob發送區，rev_Bob為Bob接收區,src_Eve為Eve發送區，rev_Eve為Eve接收區，OK表示入侵者成功獲取了其他通信主體的非加密信息。協議發起者Bob、協議入侵者Eve的代碼和Alice差不多只是在消息的發送和接收方面有一些差異。

4.3協議安全屬性的描述

即：！[]（OK==0）表示入侵者不會永遠獲取不到其他通信主體的非加密信息。我們要驗證系統的轉移過程中不會出現人侵者Eve能夠成功獲取其他通信主體的非加密信息，從而證明各個協議主體在通信過程其發送的數據具有機密性。我們通過SPIN中“neverclaim”來描述待驗證屬性，驗證協議系統模型是否滿足要傳輸數據機密性要求。

4.4模型驗證的結果分析

SPIN驗證的結果：SPIN驗證出存在Eve成功獲取其他通信主體非加密信息的情況，通過SPIN自帶的模擬工具我們可以看出Eve獲取其他通信主體非加密信息的路徑為：可以看出Eve通過冒充Alice的身份接收或發送消息。攻擊者截獲Bob發送給Alice的消息，并用自己的公鑰加密，并將兩次加密的消息發送給Bob，而Bob無法識別該消息是不是他所期望的從Alice發出的，因為每條隨機信息看起來都很相似，根據協議，他會立即解除自己的加密，并將結果發送給Alice，此時攻擊者再次將消息截獲，解除自己的加密，那么他就得到了Bob發送給Alice的非加密的消息。

5結束語

通過應用SPIN模型檢測工具對安全協議進行分析，我們可以發現形式化驗證可以發現一些深層次的問題，這些問題靠人工審查和分析是很難發現的，這是形式化驗證的巨大優勢，然而我們也可以看到隨著協議主體的增加狀態空間大小呈指數級增長，無可避免的會出現狀態空間爆炸問題，狀態空間的大小與我們待驗證系統的抽象是緊密相關的，因而如何合理抽象是我們以后的研究方向。

本文作者：劉虹工作單位：河北省張家口市陽原縣華原市政工程有限公司