基于模型檢測的安全協(xié)議自動驗證方法研究.pdf

1、安全協(xié)議，是以密碼學(xué)為基礎(chǔ)的信息交換協(xié)議。由于安全目標(biāo)本身的復(fù)雜性、協(xié)議運(yùn)行環(huán)境的復(fù)雜性以及攻擊者模型的復(fù)雜性等多方面的原因，有必要借助形式化的分析方法或工具來完成對安全協(xié)議的分析和驗證。
　　在所有形式化方法中，模型檢測是最具工業(yè)前景的技術(shù)，被用于驗證系統(tǒng)性質(zhì)。SPIN是一款卓越的模型檢測工具，具有很強(qiáng)的系統(tǒng)建模能力，且在驗證效率上的表現(xiàn)也十分出眾，因此被許多學(xué)者與專家推崇和使用。
　　本文詳細(xì)介紹了SPIN模型檢測技術(shù)的

2、理論基礎(chǔ)、SPIN模型檢測工具的安裝和使用方法、SPIN所使用的建模語言Promela語言及其細(xì)節(jié)、線性時序邏輯的語法和語義，并討論了Dolev-Yao攻擊者模型的通用建模方法。本文所做的主要工作和創(chuàng)新之處主要有以下幾個方面：
　　1.討論了模型檢測的原理，及其在安全協(xié)議自動驗證中的應(yīng)用。
　　2.在Windows環(huán)境下，搭建了模型檢測工具SPIN的運(yùn)行平臺，為今后同類研究的實(shí)驗工作提供了基礎(chǔ)。
　　3.對SPIN的建

3、模語言Promela進(jìn)行了全面的介紹，詳細(xì)講述了它的簡單和復(fù)合數(shù)據(jù)類型、運(yùn)算符、通道機(jī)制以及各種流程控制語句，特別著重介紹了Promela語言的一些細(xì)節(jié)。這為今后同類研究工作應(yīng)用Promela語言提供了參考。
　　4.討論了安全協(xié)議驗證工作中，具有重要意義的Dolev-Yao攻擊者模型，并給出了形式化定義，以及行為刻畫的框架。這為今后同類研究在建立相同的攻擊者模型時，提供了統(tǒng)一的框架與標(biāo)準(zhǔn)，大大減少了人為刻畫的成分。
　　5