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

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

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

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