基于SPIN的網(wǎng)絡(luò)協(xié)議形式化分析與驗(yàn)證.pdf

1、隨著計(jì)算機(jī)通信與網(wǎng)絡(luò)技術(shù)的發(fā)展，網(wǎng)絡(luò)協(xié)議的穩(wěn)定性和安全性發(fā)揮著越來(lái)越重要的作用，所以對(duì)網(wǎng)絡(luò)協(xié)議的研究有重要意義。形式化的方法將成為分析網(wǎng)絡(luò)協(xié)議的重要方法，目前有很多研究網(wǎng)絡(luò)協(xié)議的理論和方法，比較重要的理論有BAN邏輯，定理證明和模型檢測(cè)等，而模型檢測(cè)作為形式化分析理論方法中的一種，有著自動(dòng)化和提供反例等優(yōu)點(diǎn)，基于此，我們采用形式化方法和模型檢測(cè)工具來(lái)檢測(cè)網(wǎng)絡(luò)協(xié)議的漏洞也是很有意義的，從而達(dá)到提高網(wǎng)絡(luò)協(xié)議安全性和穩(wěn)定性的目的。
　　

2、 本文首先在介紹網(wǎng)絡(luò)協(xié)議、形式化方法和模型檢測(cè)工具及其應(yīng)用的基礎(chǔ)上，通過(guò)不同的安裝環(huán)境對(duì)SIPN工具使用做了介紹，并對(duì)形式化描述的幾種語(yǔ)言進(jìn)行比較；其次，介紹了OSPF路由協(xié)議的概念、特性和協(xié)議的操作及工作過(guò)程，同時(shí)采用形式化方法的FSM分析了OSPF協(xié)議；接著重點(diǎn)分析了OSPF網(wǎng)絡(luò)類(lèi)型、報(bào)文頭部、報(bào)文處理流程和LSA處理流程；緊接著通過(guò)SPIN模型檢測(cè)工具對(duì)OSPF協(xié)議進(jìn)行抽象化建模，描述了OSPF協(xié)議的LTL性質(zhì)，并剛XSPIN模

3、型檢測(cè)工具進(jìn)行了檢測(cè)驗(yàn)證，得到了運(yùn)行軌跡，在此基礎(chǔ)上又采剛穩(wěn)定狀態(tài)驗(yàn)證的方法從可行性和正確性等方面驗(yàn)證了OSPF路由協(xié)議；最后總結(jié)本文的主要工作并對(duì)尚需完善的工作進(jìn)行展望。
　　 本文采用的主要方法和技術(shù)如下：⑴采用形式化的分析方法，對(duì)OSPF協(xié)議分析；⑵SPIN適用于并行系統(tǒng)，本文探討了在Windows、Java、Cygwin等環(huán)境下對(duì)SPIN工具的安裝和使用，并詳細(xì)介紹了SPIN的圖形界面工具XSPIN的安裝過(guò)程和功能的使用