基于本地會話的安全協(xié)議驗證邏輯及算法.pdf

1、安全協(xié)議是一種在不安全的公共網(wǎng)絡上為完成某種不可泄漏的信息交換而建立的通信協(xié)議．所謂網(wǎng)絡的不安全性，是指黑客的存在，他可以監(jiān)聽，阻止和偽造正在網(wǎng)上傳輸?shù)男畔?，他們的標準模型稱為Dolev-Yao模型[1].雖然安全協(xié)議使用密碼系統(tǒng)來確保其安全性，但是，他們中的漏洞很多時候是由于其設計中可能的邏輯錯誤造成，而不是由于其加密算法不可靠(如[2]就是一個典型的例子)．并且安全協(xié)議驗證問題是個公認的難題．因此，如何開發(fā)出相應的協(xié)議驗證工具，使得

2、協(xié)議的潛在攻擊能自動地被發(fā)現(xiàn)，或者某些安全的屬性可以被證明在無窮會話下都成立，是個研究的熱點． 安全協(xié)議的自動驗證問題，有兩種方法，一種是基于證偽的，另一種是證明的．證偽的方法先假定一個協(xié)議的有窮會話，然后在此會話中搜索潛在的攻擊漏洞，這種方法無法證明某些安全性質在協(xié)議的無窮會話中成立；證明的方法則彌補這個缺陷，它著眼于證明某些安全屬性在協(xié)議的任意無窮會話中都成立．基于證偽的方法有很多相應的自動驗證工具，而證明的方法也很多，但是

3、他們比較難自動化實現(xiàn)，而且他們不適合驗證大規(guī)模的協(xié)議如SET purchasephase protocol；另外一個缺陷就是他們無法驗證BAN邏輯[3]中著重提出的認知規(guī)范，如“Alice知道Bob知道Alice說過某些信息”． 本文的內容是提出一種基于本地會話的安全協(xié)議驗證邏輯LLS(Logic ofLocal Seesions)和相應的自動驗證算法及工具簡介．LLS基于安全協(xié)議的證明，并且著眼于上述的兩個問題的解決．它可以

4、實現(xiàn)協(xié)議的完全自動化驗證并可以驗證復雜協(xié)議的相關安全屬性． 本文的主要工作如下： ●我們首先定義一個描述安全協(xié)議分析的加密信息交換(CryptographicMessage Exchange)模型并結合Dolev-Yao模型，探討了里面的一些相應的重要性質．在此基礎上，我們將給出了一個稱為“實例化空間(InstantiationSpace)”的安全協(xié)議驗證邏輯的語義模型． ●在實例化空間(Instantiat

5、ion Space)語義模型基礎上，我們提出了一系列與安全屬性相關的LLS驗證公理，并證明他們在此語義模型下的正確性．這些公理比現(xiàn)有的一些驗證邏輯，如[4]中的謂詞source以及[5]中的challenge-response axiom schema和send-receive axiom schema，能描述更一般的情形(詳見備注5.1和5.2)． ●為了驗證多層的認知規(guī)范，我們引入了可觀察理論(Observation Th

6、eory)．這是一個符號化的Kripke模型，而且在這個理論基礎上，多層的認知規(guī)范問題可以很方便地轉化成SAT處理，為驗證協(xié)議的多層認知規(guī)范提供了一個簡潔和方便的符號化算法驗證途徑．我們還進一步研究了分布式知識(Distributed Knowledge)，公共知識Common Knowledge)等等的基于SAT的算法． ●由于本文的邏輯系統(tǒng)在算法上的可行性，對應的工具SPV(Security Pro-tocol Verif

7、ier)已經(jīng)開發(fā)成功，并且可以驗證復雜的協(xié)議．由于在此語義基礎上的公理集是純命題邏輯的，且所需要的驗證目標可以很方便地轉化成可滿足性問題(SAT)，從而可以利用工業(yè)上快速高效的SAT求解器實現(xiàn)．使用SPV，我們可以高效驗證復雜的包括工業(yè)級的安全協(xié)議性質，驗證的規(guī)范包括在CAPSL (Common Authentication Protocol Specifica-tion Language(CAPSL)，http：//www．csl．s