基于strand空間模型的安全協(xié)議分析與設(shè)計(jì)方法研究.pdf

1、因特網(wǎng)因其開放的協(xié)議徹底改變了計(jì)算機(jī)網(wǎng)絡(luò)，同時(shí)也帶來了新的風(fēng)險(xiǎn)和威脅。保護(hù)計(jì)算機(jī)網(wǎng)絡(luò)最好的方法就是使用快速的自動(dòng)化程序阻止攻擊者的入侵。手工的不能防止未知類型攻擊的方式是不能起到充分保護(hù)的作用的。使用基于共享攻擊信息以及機(jī)構(gòu)間合作的主動(dòng)安全管理的方法可以解決這個(gè)問題。安全區(qū)域協(xié)作是一個(gè)建立在可信區(qū)域相互合作和協(xié)同的框架，它能夠保護(hù)系統(tǒng)免遭潛在的攻擊并通過交換安全信息和區(qū)間合作來預(yù)報(bào)和響應(yīng)攻擊。在這種動(dòng)態(tài)的強(qiáng)安全體系結(jié)構(gòu)中，為了保護(hù)網(wǎng)絡(luò)中

2、傳送的區(qū)域策略免受攻擊，需要建立安全通信系統(tǒng)，密碼算法和安全協(xié)議是其核心。然而，攻擊一個(gè)成熟的密碼算法的代價(jià)比攻擊一個(gè)有缺陷的安全協(xié)議所需的代價(jià)要巨大的多，往往個(gè)人或小團(tuán)體難以完成，安全協(xié)議往往是攻擊者的首先攻擊目標(biāo)。因此，分析、設(shè)計(jì)安全有效的安全協(xié)議是計(jì)算機(jī)通訊領(lǐng)域中一個(gè)極為重要的研究課題。 安全協(xié)議是很多分布式系統(tǒng)安全的基礎(chǔ)，它負(fù)責(zé)密鑰分發(fā)和身份認(rèn)證，安全協(xié)議自身的漏洞會(huì)對(duì)通信的安全造成嚴(yán)重的威脅?，F(xiàn)有的許多協(xié)議在設(shè)計(jì)上普遍

3、存在著某些安全缺陷，安全協(xié)議的形式化分析檢驗(yàn)技術(shù)就成為目前研究的熱點(diǎn)。但現(xiàn)有的各種方法主要用于分析某個(gè)具體的安全協(xié)議的安全性，而不是致力于在設(shè)計(jì)之初就確保協(xié)議的安全性。因此使用形式化方法指導(dǎo)安全協(xié)議的設(shè)計(jì)，對(duì)于滿足復(fù)雜任務(wù)的密碼協(xié)議有著重要的意義。 在形式化方法中，基于Strand空間模型的安全協(xié)議分析，可以利用該模型中包含的確切的因果關(guān)系信息，使對(duì)協(xié)議安全性質(zhì)的證明十分簡(jiǎn)潔。認(rèn)證檢驗(yàn)是Thayer開發(fā)出的手工驗(yàn)證密碼協(xié)議的方法

4、，可以通過使用加密和隨機(jī)數(shù)達(dá)到認(rèn)證和新鮮性，同時(shí)他也提出了使用認(rèn)證檢驗(yàn)這種安全協(xié)議的形式化分析方法來指導(dǎo)安全協(xié)議設(shè)計(jì)的可能性，并對(duì)現(xiàn)有的一些協(xié)議作了再現(xiàn)。 本文通過對(duì)基于Strand空間模型理論的研究，提出圍繞認(rèn)證檢驗(yàn)在安全通信或電子商務(wù)中建立具體情況下特定安全目標(biāo)的協(xié)議，設(shè)計(jì)的過程既是通過strand空間和認(rèn)證檢驗(yàn)對(duì)可信主體證明的過程。 本文第四部分創(chuàng)建了ATSP(anAuthenticationTest-basedS

5、ecureProtocol)作為利用認(rèn)證檢驗(yàn)技術(shù)設(shè)計(jì)安全協(xié)議的實(shí)例。首先確立明確的設(shè)計(jì)目標(biāo)，即在一個(gè)三方協(xié)議交換中為指定主體提供認(rèn)證和兩兩之間的機(jī)密性。ATSP必須同時(shí)提供不可否認(rèn)保證。這里不考慮公平性。然后設(shè)計(jì)相應(yīng)的輸入檢驗(yàn)滿足ATSP的所有認(rèn)證屬性，設(shè)計(jì)驗(yàn)證的結(jié)果完成一個(gè)簡(jiǎn)單的電子商務(wù)事務(wù)，驗(yàn)證其達(dá)到購(gòu)買請(qǐng)求、授權(quán)支付以及接收支付款項(xiàng)的基本安全性能。 總之，本文是安全通信中，向建立具體安全目標(biāo)安全協(xié)議的一個(gè)嘗試，通過設(shè)計(jì)輸入