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

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

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

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

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

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