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

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

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

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