網(wǎng)絡(luò)安全協(xié)議的模型檢測(cè)分析及驗(yàn)證系統(tǒng).pdf

1、隨著計(jì)算機(jī)時(shí)代的迅猛發(fā)展,分析網(wǎng)絡(luò)的安全性相當(dāng)重要。保證安全協(xié)議的安全性及秘密性已是網(wǎng)絡(luò)安全領(lǐng)域的最熱門(mén)話題之一。安全協(xié)議自身的缺陷給網(wǎng)絡(luò)安全造成了巨大的威脅,為了確保網(wǎng)絡(luò)中傳輸?shù)男畔⒓皵?shù)據(jù)不被篡改或丟失,必須對(duì)協(xié)議進(jìn)行分析,且可以采用形式化及非形式化方法對(duì)協(xié)議進(jìn)行驗(yàn)證；為解決狀態(tài)空間爆炸問(wèn)題,必須利用搜索優(yōu)化算法對(duì)協(xié)議模型進(jìn)行改進(jìn)。由此可知,形式化分析驗(yàn)證方法是在網(wǎng)絡(luò)安全中最關(guān)鍵的技術(shù)。其中,對(duì)密碼協(xié)議性質(zhì)進(jìn)行規(guī)范極為重要,可以利用L

2、TL性質(zhì)對(duì)協(xié)議進(jìn)行描述。
　　 本文主要采用模型檢測(cè)技術(shù)對(duì)協(xié)議進(jìn)行形式化分析,旨在發(fā)現(xiàn)網(wǎng)絡(luò)安全協(xié)議中隱藏的漏洞,并對(duì)協(xié)議加以改進(jìn)。論文的主要工作和貢獻(xiàn)有:
　　 1.通過(guò)使用強(qiáng)大的驗(yàn)證密鑰協(xié)議的模型檢測(cè)工具-SPIN,運(yùn)用靜態(tài)分析技術(shù)及自動(dòng)約簡(jiǎn)方法,簡(jiǎn)化輸入方式以達(dá)到改善SPIN運(yùn)行環(huán)境的目的,從而使模型更簡(jiǎn)單易懂。
　　 2.通過(guò)將SPIN工具內(nèi)嵌入安全協(xié)議驗(yàn)證系統(tǒng),并使用狀態(tài)搜索方法滿足協(xié)議的設(shè)計(jì)規(guī)范,檢測(cè)協(xié)