基于模型檢測(cè)技術(shù)的密碼協(xié)議驗(yàn)證與分析.pdf

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

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