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

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

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