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

1、安全協(xié)議，是指在通信協(xié)議中應(yīng)用密碼學的手段隱藏或獲取信息，達到認證以及消息正確發(fā)送的目的的協(xié)議。而隨著互聯(lián)網(wǎng)的迅猛發(fā)展，安全協(xié)議的安全性成為網(wǎng)絡(luò)安全的關(guān)鍵。雖然安全協(xié)議是安全專家精心設(shè)計并仔細檢查過的，但由于協(xié)議之間消息交互存在著復雜的關(guān)系和制約，而且大部分的安全協(xié)議運行在復雜的分布式網(wǎng)絡(luò)環(huán)境中，因此，通常安全協(xié)議都存在一些不容易發(fā)現(xiàn)的安全漏洞。
　　 模型檢測的基本思想是用狀態(tài)轉(zhuǎn)移系統(tǒng)S 表示系統(tǒng)的行為，用模態(tài)時序邏輯公式F

2、描述系統(tǒng)的性質(zhì)。這樣“系統(tǒng)是否具有所期望的性質(zhì)”就轉(zhuǎn)化為數(shù)學問題“狀態(tài)轉(zhuǎn)移系統(tǒng)S是否是公式F的一個模型?”，用公式表示為S|–F。
　　 本文主要將基于時序認知邏輯的模型檢測的思想運用到安全協(xié)議的檢測中，主要內(nèi)容包括：
　　 首先，用Spi 演算來描述協(xié)議主體的行為，然后通過本文提出的規(guī)則，將其轉(zhuǎn)換成一個狀態(tài)轉(zhuǎn)移系統(tǒng)，作為本文的模型M。
　　 其次，對K算子進行了重新定義，加入到CTL 當中，形成了KCTL 邏輯