安全協(xié)議的形式化方法及其應用的研究.pdf

1、中國科學院計算技術研究所博士學位論文安全協(xié)議的形式化方法及其應用的研究姓名：華東明申請學位級別：博士專業(yè)：計算機系統(tǒng)結構指導教師：侯紫峰20050601安全協(xié)議的形式化方法及其應用的研究：摘要化和系統(tǒng)化地設計了一個基于對稱密鑰機制的安全協(xié)議和一個基于挑戰(zhàn)／響應機制進行相互身份認證和DifficHellman密鑰協(xié)商機制的安全協(xié)議；將該設計邏輯與BSw邏輯進行了比較。(3)在安全協(xié)議面向主體的分析邏輯的研究中，構建了面向主體的安全協(xié)議分析

2、邏輯，將擁有、信念和知識融合起來更真實地模擬主體在協(xié)議運行中的狀態(tài)，給出基于秘密和公開密鑰密碼系統(tǒng)的公理集，給出了蘭段論、必然律和理性推理規(guī)則；由主體的擁有集、信念集、知識集和通信行為構造安全協(xié)議的計算模型，給出該分析邏輯中形式語言的真值語義解釋，證明了該分析邏輯的可靠性；給出安全協(xié)議的分析步驟，通過對NeedhamSchroeder協(xié)議的分析檢驗了新的分析邏輯的推理能力，并與BAN和GNY邏輯對該協(xié)議的分析結論進行了比較。得出本邏輯比

3、它們有著更強的推理能力的結論。(4)在國家標準無線局域網(wǎng)認證和保密基礎設施咄I)的研究中，描述了WLAN中安全協(xié)議的特性，分析了它們中存在的安全缺陷，對WAPI和8021li進行了比較，運用本論文提出的安全協(xié)議分析邏輯對WAI協(xié)議進行了形式化分析和改進分析。(5)在可信計算的研究中，描述了可信平臺的特性和OIAP的會話過程，運用本論文提出的安全協(xié)議分析邏輯對OIAP進行了形式化分析和改進分析。關鍵詞：安全協(xié)議；身份認證；面向主體的軟件工