基于模型檢測(cè)工具SPIN的安全協(xié)議分析和驗(yàn)證.pdf

1、隨著Internet和分布式系統(tǒng)的廣泛應(yīng)用，安全協(xié)議逐漸發(fā)揮著越來(lái)越重要的作用。形式化的方法是分析安全協(xié)議的主要方法。目前已經(jīng)有很多研究安全協(xié)議的理論和方法，其中比較著名的有可證明安全理論、BAN邏輯、串空間模型理論以及模型檢測(cè)和定理證明的方法等。 模型檢測(cè)作為形式化分析安全理論方法的一種，有著自動(dòng)化和提供反例等諸多優(yōu)點(diǎn)。并且近年在硬件驗(yàn)證中得到了廣泛應(yīng)用。模型檢測(cè)器SPIN是由貝爾實(shí)驗(yàn)室開發(fā)的一種專門用于軟件和協(xié)議驗(yàn)證的工具。

2、 本文基于模型檢測(cè)工具SPIN，對(duì)電子商務(wù)協(xié)議Netbill協(xié)議做形式化地分析和驗(yàn)證。 首先對(duì)此協(xié)議從行為屬性和安全性兩方面進(jìn)行抽象。包括對(duì)協(xié)議主體建立狀態(tài)和狀態(tài)轉(zhuǎn)移描述；然后對(duì)協(xié)議采用PROMELA語(yǔ)言建立模型。協(xié)議的安全屬性描述采用LTL邏輯公式。最后運(yùn)用SPIN對(duì)協(xié)議的模型進(jìn)行行為模擬，對(duì)LTL描述的協(xié)議屬性進(jìn)行正確性及安全性驗(yàn)證。在驗(yàn)證和模擬的過(guò)程中，隨時(shí)根據(jù)模型的狀態(tài)數(shù)目和系統(tǒng)的消耗調(diào)整抽象模型的結(jié)構(gòu)和行為。對(duì)