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

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

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

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