基于strand空間模型的安全協議分析與設計方法研究.pdf

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

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

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

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

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