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

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

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

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

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