基于模型檢測技術的密碼協(xié)議驗證與分析.pdf

1、隨著計算機網(wǎng)絡通信的迅猛發(fā)展,密碼協(xié)議的重要性越來越得到重視。而在眾多的驗證方法中,模型檢測方法在對密碼協(xié)議的驗證中體現(xiàn)出了它的優(yōu)勢。
　　本課題研究的目的是采用模型檢測技術對密碼協(xié)議進行分析。文章介紹了密碼協(xié)議研究的背景、概念和分類,給出了密碼協(xié)議的系統(tǒng)模型,闡述了模型檢測分析密碼協(xié)議的理論技術?？偨Y了驗證密碼協(xié)議的各種形式化方法后,詳細研究了模型檢測工具SPIN分析密碼協(xié)議的方法,給出了SPIN對密碼協(xié)議分析的原理,構造了系統(tǒng)

2、驗證模型。最后還對模型檢測技術新的一個發(fā)展方向—“概率模型檢測”進行了研究,歸納了幾種概率模型和所使用的形式邏輯,采用PRISM概率符號模型檢測工具對概率密碼協(xié)議進行了分析,所取得的主要研究成果如下:
　　(1)基于模型檢測技術,使用SPIN對IKEv2協(xié)議進行了建模和分析。應用Promela語言描述了協(xié)議模型,并用LTL(Linear Temporal Logic)規(guī)約了該協(xié)議需要滿足的認證性和機密性,發(fā)現(xiàn)了協(xié)議的兩個攻擊,然后