安全協(xié)議形式化分析理論與應用研究.pdf

1、安全協(xié)議是一種運行在計算機網(wǎng)絡或分布式系統(tǒng)中、借助于密碼算法來達到密鑰分配和身份認證等安全目標的通信協(xié)議,是解決計算機網(wǎng)絡和分布式系統(tǒng)中安全問題的必要手段。然而，安全協(xié)議未必是安全的，它的安全性分析一直是一個復雜而困難的問題，對安全協(xié)議的研究已成為世界上信息與網(wǎng)絡安全方面的一個重要研究方向。實踐證明，形式化方法是安全協(xié)議安全性分析更為可靠和有效的途徑。
　　本文以安全協(xié)議作為研究對象，以DDMP理論為研究工具，對安全協(xié)議形式化分析

2、方法從理論和應用兩個層面展開研究，所取得的研究成果主要有：
　?。?）設計了安全協(xié)議形式化分析模型。給出了安全協(xié)議的系統(tǒng)模型，設計了安全協(xié)議形式化分析的一般模型SPFAM和基于DDMP理論的安全協(xié)議形式化分析模型DDMP-SPFAM。在模型圖的基礎上，給出了相應的模型算法，具體闡述了形式化分析遵循的步驟，對安全協(xié)議的形式化分析和設計提供了宏觀指導。
　　（2）研究了基于協(xié)議組合邏輯（PCL）的形式化分析方法。給出了基于PCL

3、證明協(xié)議安全屬性的一般方法，選取國際標準ISO/IEC DIS 11770-3中提出的重要認證協(xié)議Helsinki作為研究對象，討論了該協(xié)議存在的缺陷及受到的攻擊，改進協(xié)議，利用PCL對改進的協(xié)議方案進行形式化建模，并進行安全性證明。改進型的Helsinki協(xié)議基于PCL是安全的。
　?。?）研究了安全協(xié)議的組合性問題。討論了基于符號和基于計算復雜性的形式化分析領域中協(xié)議組合分析工具的代表PCL與UC，選取PCL作為協(xié)議組合分析的

4、工具；詳細闡述了PCL進行組合分析的過程；選擇典型的包含可信第三方的密鑰交換協(xié)議Otway-Rees展開討論，分析了協(xié)議本身的缺陷及其遭遇到的攻擊形式，提出了改進方案（AOR協(xié)議）；擴展PCL，利用PCL對改進后的AOR協(xié)議進行了形式化建模和模塊化安全性證明。AOR協(xié)議能滿足密鑰保密屬性。
　?。?）從非形式化和形式化兩個方面研究了安全協(xié)議設計方法。在非形式化方面，針對安全協(xié)議設計規(guī)范、原則展開討論；在形式化方面，闡述了協(xié)議演繹系