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

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

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

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

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