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

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

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

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

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

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

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

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