基于線空間模型的安全協(xié)議形式化分析.pdf

1、安全協(xié)議，又稱密碼協(xié)議，是指運行在計算機網(wǎng)絡(luò)或者分布式系統(tǒng)環(huán)境下，依賴應(yīng)用密碼學(xué)技術(shù)完成身份認證、密鑰分配或者電子交易等任務(wù)的協(xié)議。它的正確性是網(wǎng)絡(luò)和分布式系統(tǒng)應(yīng)用安全的基礎(chǔ)，針對這些協(xié)議進行形式化分析長期以來一直是安全領(lǐng)域的重要研究課題。 安全協(xié)議形式化分析的目標(biāo)是協(xié)議的關(guān)聯(lián)性、保密性，以及與電子商務(wù)相關(guān)的不可否認性、公平性和時限性等，論文的研究工作主要針對其中的基本屬性——關(guān)聯(lián)性和保密性展開。大部分已有的分析方法或者采用信仰

2、邏輯等推理技術(shù)，或者采用狀態(tài)檢測等定理證明技術(shù)，前者分析能力較弱，而后者存在狀態(tài)爆炸問題。因此，目前研究的一個趨勢是綜合應(yīng)用多種分析手段，取長補短，以達到最好的分析效果。與之相對應(yīng)，論文提出了一種新的基于挑戰(zhàn)一響應(yīng)的分析方法，該方法采用線空間模型作為底層的語義模型、采用認證邏輯作為基本分析手段，并融合了Athena算法、認證測試等多種技術(shù)。全部研究內(nèi)容可以劃分為四個層面，分別是建立語義模型、提出分析手段、設(shè)計自動化工具和協(xié)議分析應(yīng)用。

3、 在語義模型方面，采用線空間模型作為底層語義模型，給出了協(xié)議關(guān)聯(lián)性和保密性的明確的形式化定義。將保密性分析分解為顯式泄密和隱性泄密問題，其中隱性泄密分析依賴于關(guān)聯(lián)性的判斷；而關(guān)聯(lián)性的分析被總結(jié)為協(xié)議Strand之間的存在關(guān)系和Strand參數(shù)的一致性問題。 在分析手段方面，充分利用認證邏輯、Athena算法、認證測試等現(xiàn)有研究成果，并從中提取出新鮮性、唯一生成，測試和Nonce驗證等共有的概念，指出安全協(xié)議本質(zhì)上是協(xié)議主體

4、采用密碼學(xué)方法通過挑戰(zhàn)一響應(yīng)來對協(xié)議其他方的存在做出判斷，同時完成一些數(shù)據(jù)如會話密鑰的協(xié)商的過程，挑戰(zhàn)一響應(yīng)是協(xié)議分析中最小的有效單位。在此基礎(chǔ)上，提出了一種新的形式化分析方法。 在自動化工具方面，采用Prolog語言設(shè)計并實現(xiàn)了一個基于認證邏輯的協(xié)議分析工具，可以有效推導(dǎo)并判斷協(xié)議在特定的目標(biāo)上是否滿足需求，在自動化工具設(shè)計領(lǐng)域進行了初步但有益的嘗試。 在協(xié)議分析應(yīng)用方面，針對五個具有代表性的安全協(xié)議給出了形式化的分析