導(dǎo)語：基于SPIN的安全協(xié)議形式化驗(yàn)證方法一文來源于網(wǎng)友上傳，不代表本站觀點(diǎn)，若需要原創(chuàng)文章可咨詢客服老師，歡迎參考。

1引言

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

2SPIN的工作原理

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

2.1待驗(yàn)證屬性的描述

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

2.2Promela(PROcessMetaLanguage)建模語言

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

3用SPIN驗(yàn)證協(xié)議的過程

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

4實(shí)例分析

4.1協(xié)議的簡化的描述

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

4.2協(xié)議的系統(tǒng)模型以及Promela描述

以Dolev-Yao模型為依據(jù)對協(xié)議系統(tǒng)進(jìn)行建模。假設(shè)協(xié)議主體在擁有了正確的秘鑰時(shí)才可以解碼，并且產(chǎn)生的密文必須擁有相應(yīng)的明文和秘鑰，攻擊者無法破譯密碼，但是他可以在任意時(shí)刻對任意信道截獲密文，也可以再任意時(shí)刻對任意信道發(fā)送密文。這樣可以看出系統(tǒng)中應(yīng)有三個(gè)進(jìn)程，消息發(fā)起者進(jìn)程，消息響應(yīng)者進(jìn)程，攻擊者進(jìn)程。進(jìn)程之間通過信道來通信。定義Promela程序的數(shù)據(jù)類型: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為通信主體接收、發(fā)送數(shù)據(jù)通道。Msg為信息格式，code1、code2、code3分別Alice,Bob,Eve的加密區(qū)，即當(dāng)code1為1表示消息被加密Alice，其他情況以此類推。src_Alice為Alice發(fā)送區(qū)，rev_Alice為Alice接收區(qū)，src_Bob為Bob發(fā)送區(qū)，rev_Bob為Bob接收區(qū),src_Eve為Eve發(fā)送區(qū)，rev_Eve為Eve接收區(qū)，OK表示入侵者成功獲取了其他通信主體的非加密信息。協(xié)議發(fā)起者Bob、協(xié)議入侵者Eve的代碼和Alice差不多只是在消息的發(fā)送和接收方面有一些差異。

4.3協(xié)議安全屬性的描述

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

4.4模型驗(yàn)證的結(jié)果分析

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

5結(jié)束語

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

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