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

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

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

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