1、論文以串空間理論為基本架構(gòu)，因?yàn)榇臻g理論結(jié)合了多種形式化方法的思想和技術(shù)，本身體現(xiàn)了協(xié)議形式化分析領(lǐng)域的發(fā)展方向，而且可以用定理證明的手動(dòng)方法完成證明，得到可信的結(jié)果。該理論簡(jiǎn)潔易用，基于圖論對(duì)協(xié)議進(jìn)行描述，在協(xié)議證明中，可以使用圖形提供輔助說(shuō)明。在串空間理論中，攻擊者具有的原子行為用定義的攻擊者跡描述，它總結(jié)了攻擊者丟棄消息、生成消息、連接消息，以及攻擊者的密碼運(yùn)算能力。顯然，隨著攻擊者攻擊手段的不斷翻新和密碼學(xué)本身的發(fā)展，串空間理

2、論需要擴(kuò)展和完善。在論文中我們?cè)黾恿斯粽叩脑用枋?，增加了散列函?shù)、簽名驗(yàn)證和DH操作的原子行為，給出了基于口令猜測(cè)的原子攻擊。以及針對(duì)不同類(lèi)型的口令猜測(cè)，給出了由原子行為構(gòu)成的組合跡。這樣就擴(kuò)展了串空間理論分析安全協(xié)議的適用范圍。 基于Diffie-Hellman密鑰交換機(jī)制的安全傳輸層協(xié)議(TLS)，為通信應(yīng)用程序提供保密性和數(shù)據(jù)完整性。協(xié)議中涉及到加密、簽名、驗(yàn)證以及DH運(yùn)算等密碼運(yùn)算類(lèi)型，原始的串空間理論沒(méi)有把加密運(yùn)算

3、和簽名運(yùn)算區(qū)分開(kāi)，同時(shí)還缺乏其它的密碼原語(yǔ)的定義。因此用原始的串空間理論分析TLS協(xié)議很不方便。在擴(kuò)展定義的串空間模型中，增加了簽名、DH運(yùn)算和單向計(jì)算的原語(yǔ)類(lèi)型，并基于擴(kuò)展的串空間理論對(duì)TLS協(xié)議進(jìn)行了分析，給出的定理證明了TLS協(xié)議的密鑰協(xié)商的秘密性和通信主體雙方的可鑒別性。 將安全協(xié)議的口令猜測(cè)攻擊進(jìn)行了分類(lèi)，包括：簡(jiǎn)單的猜測(cè)攻擊、分層猜測(cè)攻擊、內(nèi)部猜測(cè)攻擊以及帶重放的猜測(cè)攻擊。針對(duì)每類(lèi)猜測(cè)攻擊給出了一個(gè)串空間理論分析框架

4、。為串空間理論新增加了四種口令猜測(cè)的攻擊原語(yǔ)，并利用組合跡概念對(duì)各類(lèi)猜測(cè)攻擊進(jìn)行了統(tǒng)一建模。用擴(kuò)展的串空間理論對(duì)GLNS協(xié)議進(jìn)行了分析，證明了該協(xié)議能抵御猜測(cè)攻擊。 在擴(kuò)展和完善串空間理論的研究中，我們發(fā)現(xiàn)在一個(gè)分布式的開(kāi)放網(wǎng)絡(luò)中，很多信息項(xiàng)在協(xié)議運(yùn)行前都是未知的。例如協(xié)議發(fā)起者和接收者在鑒別確認(rèn)之前，主體身份應(yīng)該視為未知。又如當(dāng)主體在接收到一個(gè)加密消息而在沒(méi)有解密之前，加密內(nèi)容應(yīng)該視為未知等等。這樣我們把協(xié)議變量引入到模型中形

5、成了一個(gè)新的協(xié)議模型，由于這個(gè)模型仍然以協(xié)議串為基礎(chǔ)，我們稱(chēng)它為帶變量的串空間模型。傳統(tǒng)的串空間采用代數(shù)方法，并引進(jìn)了兩種有向邊的概念，從而使協(xié)議進(jìn)程表示為一個(gè)無(wú)環(huán)的有向圖。語(yǔ)義豐富而且清晰，使得協(xié)議描述精確，從而給分析協(xié)議打下了良好的基礎(chǔ)。但是傳統(tǒng)的串空間不能刻畫(huà)“P剛剛說(shuō)過(guò)X”，“X是新鮮的”這樣的斷言，而時(shí)序邏輯則適合刻畫(huà)這樣的斷言。所以我們使用了時(shí)序和模態(tài)邏輯語(yǔ)言證明和推理協(xié)議性質(zhì)。由于邏輯語(yǔ)言直接使用一些判斷謂詞，因而用于表達(dá)

6、協(xié)議內(nèi)容和目標(biāo)時(shí)，則要直觀得多。而上一時(shí)刻算子和曾經(jīng)算子◆可以表示出剛剛發(fā)生過(guò)這樣的斷言等。 將模態(tài)邏輯和串空間模型結(jié)合起來(lái)，給出模態(tài)邏輯的串空間語(yǔ)義，并運(yùn)用該語(yǔ)義證明了模態(tài)邏輯的推理規(guī)則是正確的。給出了Helsinki協(xié)議的分析案例，結(jié)果表明給出的分析模型可有效地表達(dá)協(xié)議的安全需求。為了避免出現(xiàn)狀態(tài)空間爆炸問(wèn)題，提出了安全協(xié)議的多層分析模型，在證明一個(gè)復(fù)雜的安全協(xié)議的安全需求時(shí)，將一個(gè)復(fù)雜協(xié)議分割成幾個(gè)子協(xié)議，分別證明子協(xié)議的

7、正確性。然后，應(yīng)用交叉組合規(guī)則證明如果環(huán)境不變時(shí)，在子協(xié)議中成立的性質(zhì)，在子協(xié)議合并后仍然存立。用統(tǒng)一的時(shí)序邏輯框架對(duì)認(rèn)證Diffie-Hellman密鑰交換協(xié)議進(jìn)行了分析。 論文針對(duì)理想理論和認(rèn)證測(cè)試?yán)碚搶?duì)串空間模型進(jìn)行了擴(kuò)展。理想的概念是對(duì)串空間模型的進(jìn)一步深化和擴(kuò)展，串空間使用理想的概念來(lái)約束攻擊者的能力，該約束獨(dú)立于所分析的協(xié)議，可以證明出關(guān)于攻擊者能力的普適性結(jié)論。原來(lái)的理想概念只定義了關(guān)于聯(lián)結(jié)運(yùn)算和加密運(yùn)算的一個(gè)閉包

8、，由于實(shí)際的密碼運(yùn)算遠(yuǎn)不止這些，例如論文增加了單向散列運(yùn)算和陷門(mén)單向散列運(yùn)算和猜測(cè)攻擊原語(yǔ)。另外，將加密運(yùn)算和簽名運(yùn)算區(qū)分開(kāi)來(lái)，增加了簽名和驗(yàn)證類(lèi)型，從而豐富了模型的語(yǔ)義信息。由于在模型中增加了新的密碼運(yùn)算的類(lèi)型，因此論文對(duì)原來(lái)的理想概念進(jìn)行了調(diào)整?；谡撐牡臄U(kuò)展模型，得到了新的關(guān)于理想的誠(chéng)實(shí)性定理。串空間理論主要分析安全協(xié)議的可鑒別性、保密性以及唯一性。用認(rèn)證測(cè)試?yán)碚摲治鲭娮由虅?wù)協(xié)議的不可否認(rèn)性、公平性、以及可追究性，是該理論的一個(gè)新

9、的研究方向。 利用串空間理想模型，重點(diǎn)分析了幾個(gè)有代表性的安全協(xié)議，包括著名的具有雙向認(rèn)證功能的Otway-Rees認(rèn)證協(xié)議，在分布式網(wǎng)絡(luò)中廣泛使用的基于對(duì)稱(chēng)密鑰密碼技術(shù)的Kerberos認(rèn)證協(xié)議。利用理想模型對(duì)Otway-Rees認(rèn)證協(xié)議分析指出，形式分析可以輔助發(fā)現(xiàn)協(xié)議的設(shè)計(jì)缺陷。對(duì)Kerberos協(xié)議分析指出，協(xié)議存在猜測(cè)攻擊的缺陷，提出將DH密鑰交換算法和公鑰密碼體制引入到Kcrbcros認(rèn)證協(xié)議中。協(xié)議改進(jìn)的結(jié)果提高了

10、Kcrberos論證協(xié)議的安全性，可以避免遭受口令攻擊的危險(xiǎn)。 從理論上探討了將模型檢測(cè)與串空間結(jié)合在一起的綜合分析方法和優(yōu)勢(shì)。主要優(yōu)勢(shì)是可以發(fā)揮模型檢測(cè)的自動(dòng)狀態(tài)搜索的優(yōu)勢(shì)，但會(huì)出現(xiàn)狀態(tài)空間爆炸問(wèn)題，因此，需要研究狀態(tài)約簡(jiǎn)技術(shù)。論文進(jìn)一步完善了原來(lái)的模型檢測(cè)算法，通過(guò)增加刪減規(guī)則對(duì)狀態(tài)空間進(jìn)行約束，從而有效地控制自動(dòng)搜索過(guò)程中的狀態(tài)規(guī)模。同時(shí)，我們還提出了利用有限狀態(tài)機(jī)進(jìn)行推理的算法。在每一步狀態(tài)轉(zhuǎn)換中，誠(chéng)實(shí)主體可選擇執(zhí)行規(guī)則

11、庫(kù)中任一匹配的規(guī)則；攻擊者除了可選擇執(zhí)行任一匹配的推理規(guī)則外，還可選擇執(zhí)行任一攻擊規(guī)則。最后根據(jù)產(chǎn)生的不同路徑驗(yàn)證協(xié)議是否滿足安全需求。 總的來(lái)說(shuō)，本文圍繞串空間理論的研究，其工作主要有以下幾個(gè)方面： 1)對(duì)基本串空間理論進(jìn)行了擴(kuò)展和完善，加入了單向散列運(yùn)算和陷門(mén)單向散列運(yùn)算，增加了簽名和驗(yàn)證類(lèi)型，從而豐富了模型的語(yǔ)義信息。對(duì)基于口令的一類(lèi)的安全協(xié)議進(jìn)行了深入研究，給出了基于口令猜測(cè)的原子攻擊。并對(duì)口令猜測(cè)攻擊的各種類(lèi)型

12、在串空間模型中作了分類(lèi)，給出了由口令猜測(cè)原子行為構(gòu)成的組合跡。這樣就擴(kuò)展了串空間理論分析安全協(xié)議的適用范圍。 2)擴(kuò)展了串空間的理想模型，并得到了新的關(guān)于理想的誠(chéng)實(shí)性定理。針對(duì)原來(lái)的理想概念沒(méi)有包含更多的密碼原語(yǔ)，論文重新定義了原來(lái)的理想概念。電子商務(wù)協(xié)議因其特殊性而區(qū)別于一般的安全協(xié)議。用串空間的認(rèn)證測(cè)試?yán)碚撔问交治鲭娮由虅?wù)協(xié)議的性質(zhì)是本文研究的一個(gè)新的方向。基于認(rèn)證測(cè)試的思想，本文從認(rèn)證安全性的角度提出了電子商務(wù)協(xié)議的一般

13、設(shè)計(jì)方法和分析方法。 3)提出了一個(gè)新的有限狀態(tài)自動(dòng)驗(yàn)證算法，從理論上探討了將模型檢測(cè)與串空間結(jié)合在一起的綜合分析方法和優(yōu)勢(shì)。算法利用不可達(dá)理論和逆向生成技術(shù)，避免了狀態(tài)搜索過(guò)程中出現(xiàn)狀態(tài)爆炸的可能：逆向生成的可達(dá)串，使得對(duì)空間資源的要求大大降低，用實(shí)例證明算法的實(shí)際效果良好。 4)將協(xié)議變量引入到串空間模型中，形成了有變量參與運(yùn)算并以協(xié)議串為基礎(chǔ)的新的協(xié)議模型，我們稱(chēng)它為帶變量的串空間模型。由于將變量的匹配操作、替換操