模型檢測(cè)在安全協(xié)議形式化驗(yàn)證中的應(yīng)用.pdf

1、信息對(duì)當(dāng)代社會(huì)具有重要作用，信息安全依賴于安全協(xié)議的應(yīng)用。對(duì)安全協(xié)議的分析是一項(xiàng)極有價(jià)值的工作。目前的安全協(xié)議驗(yàn)證工作主要采用各種形式化方法，如模態(tài)邏輯證明、定理證明理論以及模型檢測(cè)方法。模態(tài)邏輯技術(shù)采用各種公式進(jìn)行論述，驗(yàn)證是否能實(shí)現(xiàn)預(yù)期要求，操作流程比較簡(jiǎn)便，其中著名的方法有BAN邏輯、SVO邏輯、Kialar邏輯等；定理證明理論通過對(duì)各實(shí)體進(jìn)行定義，利用命題證明檢驗(yàn)缺陷的有無，其中應(yīng)用較多的技術(shù)有Isabelle技術(shù)、串空間等。隨

2、著各種檢測(cè)手段的發(fā)展，入侵技術(shù)也在不斷更新，原有檢測(cè)手段的不足逐漸顯露出來。模態(tài)邏輯方式雖然易懂易用，可有時(shí)不能提供精確的表達(dá)，分析能力有限；定理證明方法較模態(tài)邏輯有了較大改進(jìn)，驗(yàn)證過程更加嚴(yán)謹(jǐn)，但是檢測(cè)內(nèi)容主要集中在協(xié)議正確性方面，驗(yàn)證能力比較有限，證明過程不是很好理解，而且難以實(shí)現(xiàn)自動(dòng)化。即便如此，這兩種分析方法還是在協(xié)議驗(yàn)證中作出了重要貢獻(xiàn)，檢測(cè)能力比早期的人為判斷有很大進(jìn)步。模型檢測(cè)方法的使用較晚，但應(yīng)用已經(jīng)比較廣泛了。該方法最

3、早被用于硬件驗(yàn)證，隨著上世紀(jì)末被引入安全協(xié)議領(lǐng)域后，經(jīng)歷了一個(gè)飛速發(fā)展的階段。模型檢測(cè)技術(shù)根據(jù)系統(tǒng)模型和驗(yàn)證屬性進(jìn)行狀態(tài)空間搜索，其優(yōu)勢(shì)在于自動(dòng)化程度高，用模型檢測(cè)工具進(jìn)行自動(dòng)分析，大大減少了人工干預(yù)，當(dāng)驗(yàn)證屬性不滿足時(shí)能夠提供相應(yīng)的反例。
　　本文首先介紹了密碼學(xué)和安全協(xié)議的理論基礎(chǔ)，重點(diǎn)介紹了形式化方法的理論和技術(shù)。接著介紹了模型檢測(cè)技術(shù)的工作原理，對(duì)模型檢測(cè)工具SMV的工作過程進(jìn)行實(shí)例說明。之后，采用基于理論證明的串空間技術(shù)