安全協(xié)議的Rubin邏輯及有色Petri網(wǎng)分析方法研究與應(yīng)用.pdf

1、當(dāng)今，隨著網(wǎng)絡(luò)技術(shù)的迅猛發(fā)展和廣泛應(yīng)用，網(wǎng)絡(luò)已經(jīng)成為人們共享信息的主要方式，人們可以隨時(shí)、隨地以各種方式提供和接受信息。然而，網(wǎng)絡(luò)技術(shù)是一把雙刃劍，在給人們帶來(lái)巨大便利的同時(shí)也給信息的安全造成巨大威脅。因此，在當(dāng)今信息社會(huì)，信息安全的重要性與日俱增。而作為網(wǎng)絡(luò)通信基礎(chǔ)的安全協(xié)議是通信各方的橋梁。由此可見(jiàn)，協(xié)議安全是信息安全領(lǐng)域的重要課題。
　　然而，設(shè)計(jì)一個(gè)健壯有效的安全協(xié)議非常困難，這不僅因?yàn)榫W(wǎng)絡(luò)的復(fù)雜性還因?yàn)榘踩珔f(xié)議的多目標(biāo)性

2、。實(shí)踐證明，設(shè)計(jì)和分析安全協(xié)議需要依靠形式化方法和理論。經(jīng)過(guò)20多年的研究和發(fā)展，在安全協(xié)議的形式化方法和理論領(lǐng)域，百家爭(zhēng)鳴，百花齊放。但是，現(xiàn)有的形式化理論和方法都不完善。因此，深入研究安全協(xié)議的形式化分析理論和方法意義重大。
　　安全協(xié)議的形式化分析方法主要分為三類：基于推理結(jié)構(gòu)的方法，又稱形式邏輯方法，基于攻擊結(jié)構(gòu)的方法，又稱模型檢測(cè)方法，基于證明結(jié)構(gòu)的方法?；谶壿嫷男问交椒ㄊ亲钪苯右彩亲詈?jiǎn)單的方法，已經(jīng)被廣泛研究和應(yīng)用

3、。Rubin博士提出的Rubin邏輯是第一個(gè)可以推理非單調(diào)協(xié)議的邏輯。與BAN類邏輯相比，Rubin邏輯有諸多優(yōu)點(diǎn)?？梢哉f(shuō)，Rubin邏輯是安全協(xié)議分析中一個(gè)有潛力、有前途的方法。模型檢測(cè)技術(shù)一般使用自動(dòng)化工具，在自動(dòng)程度方面表現(xiàn)良好。屬于高級(jí)Petri網(wǎng)的有色Petri網(wǎng)已經(jīng)被證明是一個(gè)適于安全協(xié)議建模的方法。盡管如此，使用有色Petri網(wǎng)分析安全協(xié)議仍然需要進(jìn)一步研究。
　　本文主要對(duì)安全協(xié)議的Rubin邏輯的形式化方法與基于

4、有色Petri網(wǎng)的模型檢測(cè)技術(shù)進(jìn)行了深入研究，我們還系統(tǒng)研究了這兩種方法在協(xié)議形式化分析中的應(yīng)用。我們對(duì)Rubin邏輯進(jìn)行了一系列擴(kuò)展和改進(jìn)。此外，我們還提出了兩種基于有色Petri網(wǎng)的協(xié)議分析新方法。我們采用上述新方法分析了多個(gè)安全協(xié)議。總的來(lái)講，從理論和實(shí)踐兩個(gè)層面上研究了安全協(xié)議的形式化分析。主要工作有以下幾個(gè)方面：
　　1.對(duì)安全協(xié)議的基本理論進(jìn)行了研究，介紹了安全協(xié)議的基本概念，給出了一個(gè)安全協(xié)議模型，分析了安全協(xié)議的基

5、本性質(zhì)。指出了安全協(xié)議分析的復(fù)雜性。并著重對(duì)目前的安全協(xié)議分析形式化方法進(jìn)行了分析和討論。
　　2.研究了基于邏輯的安全協(xié)議形式化分析方法，其中對(duì)ZQ邏輯和Rubin邏輯進(jìn)行了著重的研究。介紹了BAN邏輯及其兩個(gè)重要擴(kuò)展GNY邏輯和SVO邏輯。提出了一個(gè)新的可追究和公平協(xié)議，這個(gè)協(xié)議是ISI支付協(xié)議的一個(gè)改進(jìn)版本，并用ZQ邏輯分析了新的協(xié)議滿足追究性和公平性。此外，應(yīng)用Rubin邏輯分析了Andrew安全RPC協(xié)議及其兩個(gè)改進(jìn)協(xié)議

6、，發(fā)現(xiàn)原始協(xié)議存在已知漏洞，并且發(fā)現(xiàn)G.Lowe修改后的協(xié)議仍然存在漏洞，隨后，提出了一個(gè)新的改進(jìn)，克服了所發(fā)現(xiàn)的漏洞。還應(yīng)用Rubin邏輯分析了SSL協(xié)議的恢復(fù)一個(gè)已存在的會(huì)話模式。此類實(shí)用協(xié)議往往難以用BAN類邏輯來(lái)分析。分析發(fā)現(xiàn)，此模式下SSL協(xié)議能夠?qū)崿F(xiàn)建立新的安全連接的目標(biāo)。這兩個(gè)例子說(shuō)明Rubin邏輯能夠較好的克服BAN類邏輯的缺陷。
　　3.著重研究了如何擴(kuò)展Rubin邏輯，并提出了三個(gè)擴(kuò)展。研究發(fā)現(xiàn)Rubin邏輯難

7、以分析含有時(shí)間戳的消息，此外，Rubin邏輯不適用于分析非否認(rèn)性、可追究性及公平性，而這三個(gè)性質(zhì)都是電子商務(wù)協(xié)議強(qiáng)調(diào)的安全性質(zhì)。由此，提出對(duì)Rubin邏輯的三個(gè)擴(kuò)展。第一個(gè)擴(kuò)展可用于分析含有時(shí)間戳的消息。采用ZQ邏輯的思想提出了第二個(gè)擴(kuò)展，可用于分析非否認(rèn)性。第三個(gè)擴(kuò)展是在第二個(gè)基礎(chǔ)上進(jìn)行的，可以分析非否認(rèn)性、可追究性和公平性，闡述了如何應(yīng)用改進(jìn)后的方法對(duì)電子商務(wù)協(xié)議進(jìn)行分析。這三個(gè)擴(kuò)展彼此聯(lián)系，可以根據(jù)協(xié)議類型不同靈活使用。
　

8、　另一方面，采用擴(kuò)展后的Rubin邏輯對(duì)三個(gè)分屬不同類型的安全協(xié)議進(jìn)行了分析。分析了采用時(shí)間戳的X.509認(rèn)證協(xié)議，發(fā)現(xiàn)協(xié)議不僅不能實(shí)現(xiàn)它的三個(gè)目標(biāo)而且還存在冗余。隨后給出了兩個(gè)改進(jìn)，其中一個(gè)改進(jìn)沒(méi)用使用時(shí)間戳。此外，分析了MANET中一個(gè)安全路由協(xié)議——ARAN，尤其，分析了協(xié)議中證書(shū)廢除這種非單調(diào)的知識(shí)。發(fā)現(xiàn)了該協(xié)議存在的一些問(wèn)題，并提出一個(gè)改進(jìn)。還分析了Zhou-Gollman協(xié)議這一經(jīng)典的電子商務(wù)協(xié)議。與其他方法不同之處在于，不

9、僅分析了該協(xié)議的可追究性和公平性，還分析了其機(jī)密性，完整性和新鮮性。發(fā)現(xiàn)該協(xié)議可以滿足完整性，但是不能實(shí)現(xiàn)機(jī)密性，交易雙方也很難確定消息的新鮮性。實(shí)例分析表明，擴(kuò)展后的Rubin邏輯不論在分析認(rèn)證協(xié)議還是分析電子商務(wù)協(xié)議中都表現(xiàn)良好。
　　4.研究了有色Petri網(wǎng)的基本理論及其一個(gè)自動(dòng)化工具CPNTools。闡述了Petri網(wǎng)及有色Petri網(wǎng)的形式化定義。分析討論了有色Petri網(wǎng)的動(dòng)態(tài)特性。此外對(duì)CPNTools的應(yīng)用接口及

10、如何使用這一工具對(duì)有色Petri網(wǎng)進(jìn)行建模和分析進(jìn)行了探討。
　　5.重點(diǎn)研究了使用有色Petri網(wǎng)的協(xié)議模型檢測(cè)技術(shù)，提出了兩種分別適用于分析認(rèn)證協(xié)議和電子商務(wù)協(xié)議的有色Petri網(wǎng)新方法。先是給出了一個(gè)網(wǎng)上閱卷流程的分層有色Petri網(wǎng)模型，并分析了該模型的并發(fā)、沖突和關(guān)系依賴。該建模方法可以作為安全協(xié)議建模的基礎(chǔ)。在對(duì)當(dāng)前流行的基于有色Petri網(wǎng)協(xié)議分析方法研究基礎(chǔ)之上，提出了一個(gè)采用有色Petri網(wǎng)和CPNTools的認(rèn)

11、證協(xié)議分析方法。該方法的主要貢獻(xiàn)在于入侵者有色Petri網(wǎng)模型的建立，該模型是開(kāi)放的，可以融合多種攻擊策略，這對(duì)于避免狀態(tài)空間爆炸有良好作用。隨后運(yùn)用新方法對(duì)Andrew安全RPC協(xié)議的一個(gè)改進(jìn)版本進(jìn)行了分析，同樣發(fā)現(xiàn)了一個(gè)G.Lowe找到的攻擊。此外，提出了一個(gè)用于分析電子商務(wù)協(xié)議的融合ZQ邏輯及有色Petri網(wǎng)的新方法，新方法無(wú)需建立爭(zhēng)端仲裁模型。應(yīng)用新方法分析了ISI支付協(xié)議，發(fā)現(xiàn)該協(xié)議的一個(gè)不安全的狀態(tài)，分析得到協(xié)議不能滿足可追