基于公開密鑰認(rèn)證協(xié)議安全性的分析與研究本科畢業(yè)論文

1、 . . . 1 / 43題目：基于公開密鑰認(rèn)證協(xié)議安全性題目：基于公開密鑰認(rèn)證協(xié)議安全性的分析與研究的分析與研究 . . . 1 / 43畢業(yè)設(shè)計（論文）原創(chuàng)性聲明和使用授權(quán)說明畢業(yè)設(shè)計（論文）原創(chuàng)性聲明和使用授權(quán)說明原創(chuàng)性聲明原創(chuàng)性聲明本人重承諾：所呈交的畢業(yè)設(shè)計（論文） ，是我個人在指導(dǎo)教師的指導(dǎo)下進(jìn)行的研究工作與取得的成果。盡我所知，除文中特別加以標(biāo)注和致的地方外，不包含其他人或組織已經(jīng)發(fā)表或公布過的研究成果，也不包含我為獲得與其它教育機(jī)構(gòu)的學(xué)位或?qū)W歷而使用過的材料。對本研究提供過幫助和做出過貢獻(xiàn)的個人或集體，均已在文中作了明確的說明并表示了意。作 者 簽 名：日 期：指導(dǎo)教師簽名：

2、日期：使用授權(quán)說明使用授權(quán)說明本人完全了解大學(xué)關(guān)于收集、保存、使用畢業(yè)設(shè)計（論文）的規(guī)定，即：按照學(xué)校要求提交畢業(yè)設(shè)計（論文）的印刷本和電子版本；學(xué)校有權(quán)保存畢業(yè)設(shè)計（論文）的印刷本和電子版，并提供目錄檢索與閱覽服務(wù)；學(xué)?？梢圆捎糜坝?、縮印、數(shù)字化或其它復(fù)制手段保存論文；在不以贏利為目的前提下，學(xué)校可以公布論文的部分或全部容。作者簽名： 日 期：學(xué)位論文原創(chuàng)性聲明學(xué)位論文原創(chuàng)性聲明本人重聲明：所呈交的論文是本人在導(dǎo)師的指導(dǎo)下獨(dú)立進(jìn)行研究所取得的研究成果。除了文中特別加以標(biāo)注引用的容外，本論文不包含任何其他個人或集體已經(jīng)發(fā)表或撰寫的成果作品。對本文的研究做出重要貢獻(xiàn)的個人和集體，均已在文中以明確

3、方式標(biāo)明。本人完全意識到本聲 . . . 2 / 43明的法律后果由本人承擔(dān)。作者簽名： 日期： 年 月 日學(xué)位論文使用授權(quán)書學(xué)位論文使用授權(quán)書本學(xué)位論文作者完全了解學(xué)校有關(guān)保留、使用學(xué)位論文的規(guī)定，同意學(xué)校保留并向國家有關(guān)部門或機(jī)構(gòu)送交論文的復(fù)印件和電子版，允許論文被查閱和借閱。本人授權(quán)大學(xué)可以將本學(xué)位論文的全部或部分容編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索，可以采用影印、縮印或掃描等復(fù)制手段保存和匯編本學(xué)位論文。涉密論文按學(xué)校規(guī)定處理。作者簽名：日期： 年 月 日導(dǎo)師簽名： 日期： 年 月 日注意事項1.設(shè)計（論文）的容包括：1）封面（按教務(wù)處制定的標(biāo)準(zhǔn)封面格式制作）2）原創(chuàng)性聲明3）中文摘要（300 字

4、左右） 、關(guān)鍵詞4）外文摘要、關(guān)鍵詞5）目次頁（附件不統(tǒng)一編入）6）論文主體部分：引言（或緒論） 、正文、結(jié)論7）參考文獻(xiàn)8）致9）附錄（對論文支持必要時）2.論文字?jǐn)?shù)要求：理工類設(shè)計（論文）正文字?jǐn)?shù)不少于 1 萬字（不包括圖紙、程序清單等） ，文科類論文正文字?jǐn)?shù)不少于 1.2 萬字。3.附件包括：任務(wù)書、開題報告、外文譯文、譯文原文（復(fù)印件） 。4.文字、圖表要求： . . . 3 / 431）文字通順，語言流暢，書寫字跡工整，打印字體與大小符合要求，無錯別字，不準(zhǔn)請他人代寫2）工程設(shè)計類題目的圖紙，要求部分用尺規(guī)繪制，部分用計算機(jī)繪制，所有圖紙應(yīng)符合國家技術(shù)標(biāo)準(zhǔn)規(guī)。圖表整潔，布局合理，文字

5、注釋必須使用工程字書寫，不準(zhǔn)用徒手畫3）畢業(yè)論文須用 A4 單面打印，論文 50 頁以上的雙面打印4）圖表應(yīng)繪制于無格子的頁面上5）軟件工程類課題應(yīng)有程序清單，并提供電子文檔5.裝訂順序1）設(shè)計（論文）2）附件：按照任務(wù)書、開題報告、外文譯文、譯文原文（復(fù)印件）次序裝訂3）其它基于公開密鑰認(rèn)證協(xié)議安全性的分析與研究基于公開密鑰認(rèn)證協(xié)議安全性的分析與研究摘摘 要要公開密鑰認(rèn)證協(xié)議安全性分析與研究對于促進(jìn)我國信息化建設(shè)以與網(wǎng)絡(luò)安全和信息安全研究具有非常重要的意義。本文主要研究運(yùn)用模型檢測技術(shù)和基于模型檢測技術(shù)的運(yùn)行模式分析法，并研究了公開密鑰認(rèn)證協(xié)議的理論與技術(shù)。在此基礎(chǔ)上，對公開密鑰認(rèn)證協(xié)議進(jìn)行

6、了運(yùn)行模式的手工分析。研究成果如下：系統(tǒng)介紹了公開密鑰認(rèn)證協(xié)議的基本概念與安全性分析的重要意義、研究進(jìn)展和現(xiàn)狀。研究了模型檢測技術(shù)以與公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法。給出了運(yùn)用模型檢測工具 SMV 分析公開密鑰認(rèn)證協(xié)議的方法。研究了公開密鑰認(rèn)證協(xié)議，運(yùn)用運(yùn)行模式分析法分析公開密鑰認(rèn)證協(xié)議的安全性，成功地發(fā)現(xiàn)了該協(xié)議的安全漏洞。并在學(xué)習(xí)了 SMV 模型檢測工具的基礎(chǔ)上，研究了公開密鑰認(rèn)證協(xié)議的 SMV 檢測程序的框架和數(shù)據(jù)結(jié)構(gòu)。關(guān)鍵詞：關(guān)鍵詞：公開密鑰認(rèn)證協(xié)議，模型檢測協(xié)議分析，形式方法，運(yùn)行模式分析法， SMV . . . 4 / 43AbstractAbstractAnalysis of s

7、ecurity protocols has a significance to promote the information construction and the research of the network and the information security in our country. This dissertation focuses on the theory and the technique of the model checking of the security protocols. Following are the main results of this

8、thesis:Introduce the basic conception, the significance, the evolvement and the state of the cryptographic protocols analysis.Study the methods of model checking and running modes.Give the method of model checking by using the sofeware of Symbolic Model Verifier to analysis protocol.Design the proto

9、col, Use the running-mode analysis approach based on the two-party cryptographic protocols to analyze the protocol, and design a SMV program to check the TW protocol.In the basis of the SMV program of protocol, Design the general program of SMV to check the two-party protocol.Keywords:Keywords: Cryp

10、tographic protocolModel, checkingprotocol analysis, Formal methods，Running-mode, analysis approach， SMV . . . 5 / 43目錄目錄中文摘要英文摘要.1 緒論11.1 本課題的開發(fā)背景以與開發(fā)意義.11.2 國外研究現(xiàn)狀.11.3 本課題研究的主要容22 公開密鑰認(rèn)證協(xié)議11.1 公開密鑰認(rèn)證協(xié)議的基本概念.11.2 公開密鑰認(rèn)證協(xié)議分類.21.3 公開密鑰認(rèn)證協(xié)議的安全性與其設(shè)計規(guī).21.3.1 公開密鑰認(rèn)證協(xié)議的安全性分析與攻擊 31.3.2 安全協(xié)議設(shè)計規(guī) 41.4 公開密鑰認(rèn)證協(xié)

11、議模型檢測分析技術(shù)的研究與進(jìn)展.61.5 論文安排與研究成果.71.5.1 論文安排 81.5.2 主要研究成果 83 模型檢測技術(shù)與運(yùn)行模式分析法研究93.1 引言.93.2 模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的基本理論.93.2.1 模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的理論研究 93.2.2 模型檢測技術(shù)的現(xiàn)狀與存在的問題.12 . . . 6 / 433.3 兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法.133.3.1 兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法簡介.133.3.2 對兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式的研究.153.4 小結(jié).164 模型檢測工具 SMV174.1 引言.174.2SMV 語言語法

12、與 CTL 表達(dá)式.184.2.1 SMV 語言語法 184.2.2 時態(tài)邏輯 CTL204.3 SMV 實(shí)例.215 運(yùn)行模式與 SMV 分析公開密鑰認(rèn)證協(xié)議實(shí)例研究245.1 引言.245.2 公開密鑰認(rèn)證協(xié)議.245.3 運(yùn)用模式法分析公開密鑰認(rèn)證協(xié)議.255.4 公開密鑰認(rèn)證協(xié)議安全性檢測的 SMV 程序分析.295.4.1 公開密鑰認(rèn)證協(xié)議的消息的定義 295.4.2 公開密鑰認(rèn)證協(xié)議的有限狀態(tài) 305.4.3 公開密鑰認(rèn)證協(xié)議的 SMV 程序的數(shù)據(jù)結(jié)構(gòu) 315.4.4 公開密鑰認(rèn)證協(xié)議的主模塊框架和有限狀態(tài)屬性 335.4.5 公開密鑰認(rèn)證協(xié)議的安全性分析 355.5 小結(jié).366

13、 總結(jié)37參考文獻(xiàn) 38致 39畢業(yè)設(shè)計（論文）知識產(chǎn)權(quán)聲明 40畢業(yè)設(shè)計（論文）獨(dú)立性聲明 41英文翻譯 41譯文原文 48 . . . 7 / 431 緒 論本章主要系統(tǒng)地介紹了公開密鑰認(rèn)證協(xié)議的基本概念和公開密鑰認(rèn)證協(xié)議的分類，討論了公開密鑰認(rèn)證協(xié)議的安全性與其設(shè)計規(guī)，概述了公開密鑰認(rèn)證協(xié)議模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議安全性方法的重要意義、研究進(jìn)展和現(xiàn)狀。最后列舉了本文的主要研究工作，給出了本文的容安排。1.11.1 本課題本課題研究的背景、目的與意義研究的背景、目的與意義現(xiàn)代社會計算機(jī)和互聯(lián)網(wǎng)技術(shù)正在不斷的改變著人類社會的面貌，隨著計算機(jī)和網(wǎng)絡(luò)技術(shù)的不斷發(fā)展，與之伴隨而來的是信息和

14、網(wǎng)絡(luò)的安全問題。網(wǎng)絡(luò)作為現(xiàn)代信息傳遞的一個重要載體，其安全性是整個信息基礎(chǔ)架構(gòu)的安全基礎(chǔ)，而網(wǎng)絡(luò)的安全性離不開安全的網(wǎng)絡(luò)協(xié)議。所以，網(wǎng)絡(luò)協(xié)議本身是否存在安全隱患是信息安全的一個重要因素。因此，作為信息安全的一項重要研究容，公開密鑰認(rèn)證協(xié)議的安全性分析與研究。對于促進(jìn)信息化建設(shè)以與網(wǎng)絡(luò)安全和信息安全研究具有非常重要的意義。此次畢業(yè)設(shè)計主要運(yùn)用模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的理論與技術(shù)。1.2.1.2.國外研究現(xiàn)狀國外研究現(xiàn)狀自從 1976 年公鑰密碼的思想提出以來，國際上已經(jīng)提出了許多種公鑰密碼體制，但比較流行的主要有兩類：一類是基于大整數(shù)因子分解問題的，其中最典型的代表是 RSA；另一類是基

15、于離散對數(shù)問題的，比如 ElGamal 公鑰密碼和影響比較大的橢圓曲線公鑰密碼。由于分解大整數(shù)的能力日益增強(qiáng)，所以對 RSA 的安全帶來了一定的威脅。目前 768 比特模長的 RSA 已不安全。一般建議使用 1024 比特模長，預(yù)計要保證 20 年的安全就要選擇 1280 比特的模長，增大模長帶來了實(shí)現(xiàn)上的難度。而基于離散對數(shù)問題的公鑰密碼在目前技術(shù)下 512 比特模長就能夠保證其安全性。特別是橢圓曲線上的離散對數(shù)的計算要比有限域上的離散對數(shù)的計算更困難，目前技術(shù)下只需要 160 比特模長即可，適合于智能卡的實(shí)現(xiàn)，因而受到國外學(xué)者的廣泛關(guān)注。國際上制定了橢圓曲線公鑰密碼標(biāo)準(zhǔn) IEEEP1363

16、，RSA 等一些公司聲稱他們已開發(fā)出了符合該標(biāo)準(zhǔn)的橢圓曲線公鑰密碼。我國學(xué)者也提出了一些公鑰密碼，另外在公鑰密碼的快速實(shí)現(xiàn)方面也做了一定的工作，比如在 RSA 的快速實(shí)現(xiàn)和橢圓曲線公鑰密碼的快速實(shí)現(xiàn)方面都有所突破。公鑰密碼的快速實(shí)現(xiàn)是當(dāng)前公鑰密碼研究中的一個 . . . 8 / 43熱點(diǎn)，包括算法優(yōu)化和程序優(yōu)化。另一個人們所關(guān)注的問題是橢圓曲線公鑰密碼的安全性論證問題1.31.3 主要研究容：主要研究容：（1） 了解安全協(xié)議的基本概念和密碼協(xié)議的安全性分析。（2） 研究運(yùn)用公開密鑰協(xié)議運(yùn)行模式分析法，用此方法對公開密鑰協(xié)議進(jìn)行分析。（3） 嘗試運(yùn)用模型檢測工具 SMV 系統(tǒng)對公開密鑰協(xié)議的安全

17、性進(jìn)行分析和研究。2 公開密鑰認(rèn)證協(xié)議2.1 公開密鑰認(rèn)證協(xié)議的基本概念通過網(wǎng)絡(luò)來建立計算機(jī)系統(tǒng)之間的安全通信并證明此通信是安全的，不僅是一個日益受到關(guān)注的學(xué)術(shù)研究領(lǐng)域，而且也對社會生活具有非常重要的意義。在現(xiàn)實(shí)生活中，人們對協(xié)議并不陌生，人們都在自覺或不自覺地使用著各種協(xié)議。例如，在處理國際事物時，國家政府之間通常要遵守某種協(xié)議；在法律上，當(dāng)事人之間常常要按照規(guī)定的法律程序去處理糾紛；在打撲克、訂貨、投票或到銀行存款或取款時，都要遵守特定的協(xié)議。由于人們能夠熟練地使用這些協(xié)議來有效地完成所要做的事情，所以很少有人去深入地考慮它們。所謂協(xié)議（Protocol） ，就是兩個或兩個以上的參與者為完

18、成某項特定的任務(wù)而采取的一系列步驟。這個定義包含三層含義：第一、協(xié)議自始至終是有序的過程，每一步驟必須依此執(zhí)行。在前一步?jīng)]有執(zhí)行完之前，后面的步驟不可能執(zhí)行。第二、協(xié)議至少需要兩個參與者。一個人可以通過執(zhí)行一系列的步驟來完成某項任務(wù)，但它不構(gòu)成協(xié)議。第三、通過執(zhí)行協(xié)議必須能夠完成某項任務(wù)。即使某些東西看似協(xié)議，但沒有完成任何任務(wù)，也不能成為協(xié)議，只不過是浪費(fèi)時間的空操作。我們把為了完成某種安全任務(wù)的協(xié)議稱為安全協(xié)議。安全協(xié)議為了保證安全性，在設(shè)計時必須采用密碼技術(shù)。因此，我們也將安全協(xié)議稱作公開密鑰認(rèn)證協(xié)議。所以，我們可給公開密鑰認(rèn)證協(xié)議再下一個定義：公開密鑰認(rèn)證協(xié)議公開密鑰認(rèn)證協(xié)議是建立在密

19、碼體制基礎(chǔ)上的一種交互通信的協(xié)議，它運(yùn)行在計算機(jī)通信網(wǎng)或分布式系統(tǒng)中，借助于密碼算法來達(dá)到密鑰分配、身份認(rèn)證等目的。 . . . 9 / 431.2 公開密鑰認(rèn)證協(xié)議分類到目前為止，還未有人對公開密鑰認(rèn)證協(xié)議進(jìn)行過詳細(xì)的分類。因?yàn)閷⒐_密鑰認(rèn)證協(xié)議進(jìn)行嚴(yán)格分類是很難的事情，從不同的角度出發(fā)，就有不同的分類方法。例如，根據(jù)公開密鑰認(rèn)證協(xié)議的功能，可以將其分為認(rèn)證協(xié)議、密鑰建立（交換、分配）協(xié)議、認(rèn)證的密鑰建立（交換、分配）協(xié)議等；根據(jù) ISO 的七層參考模型，又可以將其分成高層協(xié)議和低層協(xié)議；按照協(xié)議中所采用的密碼算法的種類，又可以分成雙鑰（或公鑰）協(xié)議、單鑰協(xié)議或混合協(xié)議等；根據(jù)參與協(xié)議的主體

20、個數(shù)可分為兩方協(xié)議、三方協(xié)議和多方協(xié)議等。一般認(rèn)為比較合理的分類方法是應(yīng)該按照公開密鑰認(rèn)證協(xié)議的功能來分類，而不管協(xié)議具體采用何種密碼技術(shù)。固把公開密鑰認(rèn)證協(xié)議分成以下幾類：（1）密鑰建立協(xié)議（Key Establishment Protocol） ，用于完成建立公開密鑰。（2）認(rèn)證建立協(xié)議（Authentication Protocol） ，向一個實(shí)體提供對他想要進(jìn)行通信的另一個實(shí)體的身份的某種程度的確信。（3）認(rèn)證的密鑰建立協(xié)議（Authenticated Key Establishment Protocol） ，與另一身份已被證實(shí)或可被證實(shí)的實(shí)體之間建立共享秘密。 1.3 公開密鑰認(rèn)證協(xié)

21、議的安全性與其設(shè)計規(guī)公開密鑰認(rèn)證協(xié)議是許多分布系統(tǒng)安全的基礎(chǔ)。確保這些協(xié)議能夠安全地運(yùn)行是極為重要的。雖然公開密鑰認(rèn)證協(xié)議中僅僅進(jìn)行很少的幾組消息傳輸，但是其中的每一消息的組是經(jīng)過巧妙設(shè)計的，而且這些消息之間有著復(fù)雜的相互作用和制約。在設(shè)計公開密鑰認(rèn)證協(xié)議時，人們通常采用不同的密碼體制。而且所設(shè)計的協(xié)議也常常應(yīng)用于許多不同的通信環(huán)境。但是，現(xiàn)有的許多協(xié)議在設(shè)計上普遍存在著某些安全缺陷。造成認(rèn)證協(xié)議存在安全漏洞的原因有很多，我們通過對協(xié)議的安全性進(jìn)行分析，可以發(fā)現(xiàn)協(xié)議的設(shè)計漏洞，反過來可以進(jìn)一步指導(dǎo)協(xié)議的設(shè)計。1.3.1 公開密鑰認(rèn)證協(xié)議的安全性分析與攻擊在分析協(xié)議的安全性時，常用的方法是對協(xié)議

22、施加各種可能的攻擊來測試協(xié)議的安全程度。公開密鑰認(rèn)證協(xié)議攻擊的目標(biāo)通常有三個：第一個是協(xié)議中所采用的密碼算法；第二個是算法和協(xié)議中所采用的密碼技術(shù)；第三個是協(xié)議本身。由于我們本課題只討論公開密鑰認(rèn)證協(xié)議本身的安全性，因此我們將只考慮對協(xié)議自身的攻擊，而假設(shè)協(xié)議中所采用的密碼算法和密碼技術(shù)均是安全的。一般對協(xié)議自身的攻 . . . 10 / 43擊可以分為被動攻擊和主動攻擊。被動攻擊是指協(xié)議外部的實(shí)體對協(xié)議執(zhí)行的部分或整個過程實(shí)施竊聽。攻擊者對協(xié)議的竊聽并不影響協(xié)議的執(zhí)行，他所做的是對協(xié)議的消息進(jìn)行觀察，并試圖從中獲得協(xié)議中涉與的各方的某些信息。他們收集協(xié)議各方之間傳遞的消息，并對其進(jìn)行密碼分析

23、。這種攻擊實(shí)際上屬于一種惟密文攻擊。被動攻擊的特點(diǎn)是很難檢測，因此我們在設(shè)計協(xié)議時應(yīng)該盡量防止被動攻擊，使公開密鑰認(rèn)證協(xié)議對于被動攻擊是安全的，而不是試圖檢測它們。主動攻擊對公開密鑰認(rèn)證協(xié)議來說具有更大的危險性。在這種攻擊中，攻擊者試圖改變協(xié)議執(zhí)行中的某些消息以達(dá)到獲取信息、破壞系統(tǒng)或獲得對資源的非授權(quán)的訪問。他們可能在協(xié)議中加入新的消息、刪除消息、替換消息、重發(fā)舊消息、干擾信道或修改計算機(jī)中存儲的消息。在網(wǎng)絡(luò)環(huán)境下，當(dāng)通信各方彼此互不信賴時，這種攻擊對協(xié)議的威脅顯得更為嚴(yán)重。協(xié)議的攻擊者不一定是局外人，他可能就是一個合法用戶，可能是一個系統(tǒng)管理者，可能是幾個人聯(lián)手對協(xié)議發(fā)起攻擊，也可能就是協(xié)

24、議中的一方。若主動攻擊者是協(xié)議涉與的一方，我們稱其為騙子（Cheater） 。他可能在協(xié)議執(zhí)行中撒謊，或者根本不遵守協(xié)議。騙子也可以分為主動騙子和被動騙子。被動騙子遵守協(xié)議，但試圖獲得協(xié)議之外更多的信息；主動騙子則不遵守協(xié)議，對正在執(zhí)行的協(xié)議進(jìn)行干擾，試圖冒充它方或欺騙對方，以達(dá)到各種非法目的。如果運(yùn)行協(xié)議的參與者多數(shù)都是主動騙子，那么就很難保證協(xié)議的安全性。但是，在一些情況下，合法用戶可以檢測到主動欺騙的存在并采取一定的防措施。在實(shí)際應(yīng)用中，對協(xié)議的攻擊方法是多種多樣的。對不同類型的公開密鑰認(rèn)證協(xié)議，存在著不同的攻擊方法。我們很難將所有攻擊方法一一列出，這里僅僅對幾個常用的攻擊方法進(jìn)行簡單介

25、紹。（1）重放攻擊重放攻擊主要指攻擊者利用其消息再生能力生成誠實(shí)用戶所期望的消息格式并重放，從而達(dá)到破壞協(xié)議安全性質(zhì)的目的。防止重放攻擊的關(guān)鍵是保證消息的新鮮性。（2）業(yè)務(wù)流分析攻擊業(yè)務(wù)流分析的目標(biāo)是通過檢查數(shù)據(jù)包中未加密的字段和未保護(hù)的包的屬性來發(fā)現(xiàn)受保護(hù)會話的信息。例如，通過檢查未加密的 IP 源和目的地址（甚至 TCP 端口）或檢查網(wǎng)絡(luò)流量，業(yè)務(wù)流分析者就能確定哪些通信方在進(jìn)行交互、使用什么類型的服務(wù)、有時甚至能發(fā)現(xiàn)有關(guān)商家或個人用戶的信息。（3）中間人攻擊當(dāng)攻擊者能夠中途截獲發(fā)送端的消息，讀出它們并將它們發(fā)送給接收端(反之亦然)時， “中間人”攻擊就可能發(fā)生。為實(shí)施“中間人”攻擊，攻擊

26、者將必須破解密鑰，而這是一項比針對加密算法的攻擊還難的工作。（4） “剪一貼”攻擊 . . . 11 / 43此攻擊的大致過程是：首先，從一些包含敏感數(shù)據(jù)的包中切下一段密文；然后，再把這段密文拼接到另外一段密文中，被拼接的這段密文是經(jīng)過仔細(xì)選擇的，使得接收端非常有可能泄漏出經(jīng)過解密后的明文。（5）截獲攻擊入侵者通過截獲協(xié)議中傳輸?shù)南⑦M(jìn)行攻擊。（6）偽造攻擊入侵者通過偽造一條假協(xié)議消息進(jìn)行攻擊。1.3.2 安全協(xié)議設(shè)計規(guī)在協(xié)議的設(shè)計過程中，我們通常要求協(xié)議具有足夠的復(fù)雜性以抵御交織攻擊。另一方面，我們還要盡量使協(xié)議保持足夠的經(jīng)濟(jì)性和簡單性，以便可應(yīng)用于低層網(wǎng)絡(luò)環(huán)境。如何設(shè)計公開密鑰認(rèn)證協(xié)議才能

27、滿足安全性、有效性、完整性和公平性的要求呢？這就需要對我們的設(shè)計空間規(guī)定一些邊界條件。歸納起來，常見的安全協(xié)議的設(shè)計規(guī)如下：(1)采用一次隨機(jī)數(shù)來替代時戳在已有的許多安全協(xié)議設(shè)計中，人們多采用同步認(rèn)證方式，即需要各認(rèn)證實(shí)體之間嚴(yán)格保持一個同步時鐘。在某些網(wǎng)絡(luò)環(huán)境下，保持這樣的同步時鐘不難，但對于某些網(wǎng)絡(luò)環(huán)境卻十分困難。因此，建議在設(shè)計公開密鑰認(rèn)證協(xié)議時，應(yīng)盡量地采用一次隨機(jī)數(shù)來取代時戳，即采用異步認(rèn)證方式。(2)具有抵御常見攻擊的能力對于所設(shè)計的協(xié)議，我們必須能夠證明它們對于一些常見的攻擊方法，如已知或選擇明文攻擊、交織攻擊等是安全的。換言之，攻擊者永遠(yuǎn)不能從任何“回答”消息中，或修改過去的某

28、個消息，而推出有用的密碼消息。(3)適用于任何網(wǎng)絡(luò)結(jié)構(gòu)的任何協(xié)議層所設(shè)計的協(xié)議不但必須能夠適用于低層網(wǎng)絡(luò)機(jī)制，而且還必須能用于應(yīng)用層的認(rèn)證。這就意味著協(xié)議中包含的密碼消息必須要盡可能的短。如果協(xié)議采用了分組加密算法，那么我們期望此密碼消息的長度等同于一組密文的長度。(4)適用于任何數(shù)據(jù)處理能力所設(shè)計的協(xié)議不但能夠在智能卡上使用，而且也能夠在僅有很小處理能力和無專用密碼處理芯片的低級網(wǎng)絡(luò)終端和工作站上（如 PC 機(jī)）上使用。這意味著協(xié)議必須具有盡可能少的密碼運(yùn)算。(5)可采用任何密碼算法協(xié)議必須能夠采用任何已知的和具有代表性的密碼算法。這些算法可以是對稱加密算法（如 DES，IDEA） ，也可以

29、是非對稱加密算法（如 RSA） 。(6)不受出口的限制目前，各國政府對密碼產(chǎn)品的進(jìn)出口都進(jìn)行了嚴(yán)格的控制。在設(shè)計公開密鑰認(rèn)證協(xié)議時，應(yīng)該盡量做到使其不受任何地理上的限制?，F(xiàn)在，大多數(shù)規(guī)定是針對分 . . . 12 / 43組加密/解密算法的進(jìn)出口加以限制的。然而，對于那些僅僅用于數(shù)據(jù)完整性保護(hù)和認(rèn)證功能的技術(shù)的進(jìn)出口往往要容易得多。因此，對于某種技術(shù)，如果它僅依賴于數(shù)據(jù)完整性和認(rèn)證技術(shù)而非數(shù)據(jù)加密函數(shù)，它取得進(jìn)出口許可證的可能性就較大。例如，如果協(xié)議僅提供消息認(rèn)證碼功能，而不需要對大量的數(shù)據(jù)進(jìn)行加密和解密，那么就容易獲得進(jìn)出口權(quán)。這就要求我們在設(shè)計協(xié)議時，盡量避免采用加密和解密函數(shù)。(7)便于

30、進(jìn)行功能擴(kuò)充協(xié)議對各種不同的通信環(huán)境具有很高的靈活性，允許對其進(jìn)行可能的功能擴(kuò)展，起碼對一些比較顯然應(yīng)具有的功能加以擴(kuò)展。特別是，協(xié)議在方案上應(yīng)該能夠支持多用戶（多于兩個）之間的密鑰共享。另一個明顯的擴(kuò)展是它應(yīng)該允許在消息中加載額外的域，進(jìn)而可以將其作為協(xié)議的一部分加以認(rèn)證。(8)最少的安全假設(shè)在進(jìn)行協(xié)議設(shè)計時，我們常常要首先對網(wǎng)絡(luò)環(huán)境進(jìn)行風(fēng)險分析，作出適當(dāng)?shù)某跏及踩僭O(shè)。例如，各通信實(shí)體應(yīng)該相信它們各自產(chǎn)生的密鑰是好的，或者網(wǎng)絡(luò)中心的認(rèn)證服務(wù)器是可信賴的，或者安全管理員是可信賴的，等等。但是，初始假設(shè)越多，協(xié)議的安全性就越差。因此，我們應(yīng)盡可能地減少初始安全假設(shè)的數(shù)目。以上八條協(xié)議設(shè)計規(guī)并不

31、是一成不變的，我們可以根據(jù)實(shí)際情況作出相應(yīng)的補(bǔ)充或調(diào)整。但是，遵循上面提出的八條規(guī)是設(shè)計一個好協(xié)議的基礎(chǔ)。1.4 公開密鑰認(rèn)證協(xié)議模型檢測分析技術(shù)的研究與進(jìn)展協(xié)議安全性分析是揭示公開密鑰認(rèn)證協(xié)議中存在漏洞的重要途徑。目前，對公開密鑰認(rèn)證協(xié)議進(jìn)行安全性分析的方法主要有兩種：一種是攻擊檢驗(yàn)方法；另一種是采用形式化分析的方法。攻擊檢驗(yàn)方法也稱非形式化分析方法，是公開密鑰認(rèn)證協(xié)議早期的主要分析方法。這種方法對協(xié)議進(jìn)行分析一般是根據(jù)已知的各種攻擊方法對協(xié)議進(jìn)行攻擊，以攻擊是否有效來檢驗(yàn)公開密鑰認(rèn)證協(xié)議是否安全。因?yàn)閷?shí)際應(yīng)用中，存在著許多未知的攻擊方法，這種對公開密鑰認(rèn)證協(xié)議的非形式化分析方法只能發(fā)現(xiàn)協(xié)議

32、中是否存在著已知的缺陷，而不能全面客觀地來分析公開密鑰認(rèn)證協(xié)議，可能導(dǎo)致不安全的協(xié)議經(jīng)分析是安全的這樣錯誤的結(jié)論。八十年代以后，隨著對公開密鑰認(rèn)證協(xié)議安全性分析的進(jìn)一步探索研究，公開密鑰認(rèn)證協(xié)議的形式化分析成為研究熱點(diǎn)。安全協(xié)議的形式化分析是采用一種正規(guī)的、標(biāo)準(zhǔn)的方法對協(xié)議進(jìn)行分析，以檢查協(xié)議是否滿足其安全目標(biāo)。這種方法的出發(fā)點(diǎn)是希望將公開密鑰認(rèn)證協(xié)議形式化，然后借助于人工推導(dǎo)，甚至計算機(jī)的輔助分析，來判別公開密鑰認(rèn)證協(xié)議是否安全可靠。形式化分析方法和攻擊檢驗(yàn)方式相比，它能全面、深刻地檢測到公開密鑰認(rèn)證協(xié)議中細(xì)微的漏洞。形式化分析方法不僅能發(fā)現(xiàn)現(xiàn)有的攻擊方法對協(xié)議構(gòu)成的威脅，而且還可能通過對公

33、開密鑰認(rèn)證協(xié)議的安全性分析，發(fā)現(xiàn)協(xié)議中細(xì)微的漏洞，從而發(fā)現(xiàn)對公開密鑰認(rèn)證協(xié)議新的攻擊方 . . . 13 / 43法。模型檢測技術(shù)（Model Checking Technology）是屬于一般目的的公開密鑰認(rèn)證協(xié)議的形式化分析方法，它是驗(yàn)證有限狀態(tài)系統(tǒng)的自動化分析工具，常用于硬件電路設(shè)計和通信協(xié)議。目前模型檢測技術(shù)也是一種十分有效的協(xié)議形式化分析工具。模型檢測技術(shù)最早是用于分析和模擬硬件工作過程的形式化方法，隨著形式化方法的日益進(jìn)步和應(yīng)用領(lǐng)域的推廣，現(xiàn)已應(yīng)用于軟件分析和通信協(xié)議模擬等多個領(lǐng)域，但用于安全協(xié)議的分析還是近幾年新的應(yīng)用。關(guān)于模型檢測的研究越來越受到人們的關(guān)注，因?yàn)樗鼘f(xié)議的自動驗(yàn)

34、證和協(xié)議的工程化設(shè)計具有指導(dǎo)意義。 在 1996 年，英國學(xué)者 Gavin Lowe 首先使用 CSP 和模型檢測技術(shù)對公開密鑰認(rèn)證協(xié)議進(jìn)行分析13，在這篇文章中，Gavin Lowe 首次采用 CSP 模型和 CSP 模型檢測工具 FDR(故障偏差精煉檢測器，F(xiàn)ailures Divergences Refinement Checker)來分析 Needhan-Schroeder 公鑰協(xié)議，并成功地找到一個 BAN 類邏輯等分析方法以前未發(fā)現(xiàn)的攻擊。 模型檢測技術(shù)應(yīng)用于網(wǎng)絡(luò)安全協(xié)議分析的成功，使學(xué)者們相繼投入到這個領(lǐng)域。自 97 年起，計算機(jī)科學(xué)家與密碼學(xué)家開始陸續(xù)應(yīng)用模型檢測這種新的形式方

35、法來分析網(wǎng)絡(luò)安全協(xié)議的安全性，對多個網(wǎng)絡(luò)安全協(xié)議進(jìn)行了分析，成功地發(fā)現(xiàn)了許多攻擊。 在文獻(xiàn)17中 Steve Schneider 用 CSP 研究了公開密鑰認(rèn)證協(xié)議的安全性質(zhì)，在文獻(xiàn)18中 A.W.Roscoe 和 M.H.Goldsmith 基于對 CSP 和 FDR 研究，認(rèn)為它們是公開密鑰認(rèn)證協(xié)議完美的檢測工具。 在文獻(xiàn)19中 W.Marrero 等提出了一種通用的模型檢測器，構(gòu)造了他們的模型與代數(shù)理論，并證明該模型的有效性。文中并對 Needhan-Schroeder 公鑰協(xié)議進(jìn)行了分析，也成功地發(fā)現(xiàn)了文獻(xiàn)20所找到的攻擊。 在文獻(xiàn)21中 J.C.Mitchell 等設(shè)計了一種通用的狀

36、態(tài)計數(shù)工具 Mur，并用它來分析公開密鑰認(rèn)證協(xié)議可能達(dá)到的狀態(tài)，進(jìn)一步得出公開密鑰認(rèn)證協(xié)議是否安全的結(jié)論。文中分析了 Needham-Schroeder 協(xié)議、Kerberos 協(xié)議和 TMN 協(xié)議，并找到了這些協(xié)議所有已知的攻擊。在文獻(xiàn)22中 Zhe Dang 等用 ASTRAL 這種實(shí)時系統(tǒng)形式化描述語言構(gòu)造了模型檢測器，文中并對 Needham-Schroeder 公鑰協(xié)議和 TMN 協(xié)議進(jìn)行了分析，也成功地發(fā)現(xiàn)了 Gavin Lowe 所找到的所有攻擊。英國學(xué)者 Gavin Lowe 在模型檢測上做出了非凡的創(chuàng)造性成果，相應(yīng)的結(jié)論可參見2013。其中文獻(xiàn)22是一篇關(guān)于模型檢測大全性的文

37、章，文中試圖為模型檢測技術(shù)提供一個完整地解決方案。目前對于協(xié)議分析來講，模型檢測已經(jīng)證明是一條非常成功的途徑，這種方法發(fā)現(xiàn)了協(xié)議的許多以前未發(fā)現(xiàn)的新的攻擊，極促進(jìn)了網(wǎng)絡(luò)安全協(xié)議分析與設(shè)計的研究工作。但模型檢測仍然存在著許多需要進(jìn)一步研究的問題，最主要的問題在于：模型檢測適用于有限狀態(tài)系統(tǒng)地分析工具，如何將公開密鑰認(rèn)證協(xié)議說明成有限狀態(tài)系統(tǒng)，而又沒有增加或減少公開密鑰認(rèn)證協(xié)議的安全性。這是一個需要繼續(xù)深入 . . . 14 / 43研究和探索的核心問題。1.5 論文安排與研究成果本論文是在結(jié)合國家自然科學(xué)基金項目“公開密鑰認(rèn)證協(xié)議的模型檢測分析”的基礎(chǔ)上，圍繞著公開密鑰認(rèn)證協(xié)議的模型檢測技術(shù)進(jìn)行

38、了深入的研究，本論文的工作成果如下：1.5.1 論文安排第二章：指出模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的現(xiàn)狀；研究模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的基本理論；介紹兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法并對其進(jìn)行研究。第三章：介紹模型檢測工具 SMV。第四章介紹公開密鑰認(rèn)證協(xié)議；運(yùn)用運(yùn)行模式分析法分析公開密鑰認(rèn)證協(xié)議安全性；嘗試使用 SMV 檢測兩方公開密鑰認(rèn)證協(xié)議的模型檢測。1.5.2 主要研究成果以下是我們?nèi)〉玫囊恍┏晒?1) 系統(tǒng)的介紹了公開密鑰認(rèn)證協(xié)議的一些基本概念和公開密鑰認(rèn)證協(xié)議安全性分析的重要意義、研究進(jìn)展和現(xiàn)狀。(2)研究了模型檢測技術(shù)和公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法。(3)給出了運(yùn)

39、用模型檢測工具 SMV 分析公開密鑰認(rèn)證協(xié)議的方法。(4)運(yùn)用運(yùn)行模式分析法分析了公開密鑰認(rèn)證協(xié)議，并嘗試使用 SMV 研究了公開密鑰認(rèn)證協(xié)議的安全性檢測。 . . . 15 / 432 模型檢測技術(shù)與運(yùn)行模式分析法研究本章首先介紹了模型檢測技術(shù)和模型檢測技術(shù)在公開密鑰認(rèn)證協(xié)議分析領(lǐng)域取得的研究成果；隨后引出了以此技術(shù)為理論依據(jù)的公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法，并對其運(yùn)行模式作了進(jìn)一步的研究。2.1 引言模型檢測技術(shù)原是用于分析和模擬硬件工作過程的形式化方法，隨著形式化方法的推廣和應(yīng)用，模型檢測技術(shù)現(xiàn)已用于軟件分析和通信協(xié)議模擬等多個領(lǐng)域，但用于公開密鑰認(rèn)證協(xié)議的分析還是近幾年比較新的應(yīng)用。在

40、 1996 年，英國學(xué)者 Gavin Lowe 首先使用 CSP 和模型檢測技術(shù)對公開密鑰認(rèn)證協(xié)議進(jìn)行分析20。并首次采用 CSP 模型和 CSP 模型檢測工具 FDR(故障偏差精煉檢測器，F(xiàn)ailures Divergences Refinement Checker)，來分析 Needham-Schroeder公鑰協(xié)議。在這個模型中，協(xié)議參與者被說明成 CSP 中的進(jìn)程(process)，消息說明成事件（event） ，進(jìn)而將協(xié)議說明成一個通信順序進(jìn)程的集合，這些進(jìn)程并行運(yùn)行而且和他們的環(huán)境交互作用，其對公開密鑰認(rèn)證協(xié)議的驗(yàn)證是從協(xié)議說明中抽取一個模型（通常是一個有限狀態(tài)轉(zhuǎn)換系統(tǒng)） ，然后用

41、 FDR 檢測，從而證明協(xié)議的安全性。此方法成功地找到 Needham-Schroeder 協(xié)議的一個以前從未發(fā)現(xiàn)的攻擊。模型檢測的成功，使研究者們相繼投入到這個領(lǐng)域。實(shí)踐證明對于公開密鑰認(rèn)證協(xié)議安全性分析來講，模型檢測是一條非常成功的途徑。2.2 模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的基本理論2.2.1 模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的理論研究模型檢測技術(shù)可以抽象地描述為：給定一個模型 M 和邏輯描述的性質(zhì) P，檢查模型M 中性質(zhì) P 是否成立。模型檢測技術(shù)對協(xié)議進(jìn)行驗(yàn)證與分析，是通過檢查在惡意攻擊者存在的情況下，協(xié)議運(yùn)行的所有可能的路徑，來判斷協(xié)議是否實(shí)現(xiàn)了其安全保證；如果沒有，將給出攻擊者

42、的攻擊路徑。模型檢測用于有限狀態(tài)系統(tǒng)的分析，要用模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議，就要研究如何為公開密鑰認(rèn)證協(xié)議構(gòu)造有限狀態(tài)系統(tǒng)。目前，模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議的基本方法主要采用英國學(xué)者 Gavin Lowe 研究成果，即：生成一個協(xié)議運(yùn)行的小系統(tǒng)模型（通常是一個有限狀態(tài)轉(zhuǎn)換系統(tǒng)） ，以與一個可與協(xié)議互操作的攻擊者模型，并用狀態(tài)探測工具檢測系統(tǒng)是否進(jìn)入一個不安全狀態(tài)，即是否存在 . . . 16 / 43對協(xié)議的攻擊。并且基于代數(shù)理論證明：如果小系統(tǒng)是安全的，那么協(xié)議是安全的。這種方法提出了將大系統(tǒng)中協(xié)議安全的性質(zhì)研究約化為小系統(tǒng)中協(xié)議安全性質(zhì)的研究，這是目前這一領(lǐng)域的最新理論研究成果

43、。使用該方法發(fā)現(xiàn)了公開密鑰認(rèn)證協(xié)議許多以前未發(fā)現(xiàn)的新的攻擊，極促進(jìn)了公開密鑰認(rèn)證協(xié)議分析與設(shè)計的研究工作。（1 1）模型檢測對被分析協(xié)議的基本假設(shè)：）模型檢測對被分析協(xié)議的基本假設(shè)：任何一個系統(tǒng)都有其賴以存在的假設(shè)條件，用以避免結(jié)論的不當(dāng)使用以與對一些限制的理解，同樣，用模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議，對協(xié)議是有一定要求的，因?yàn)橹挥心苡糜邢逘顟B(tài)描述且滿足一定條件的協(xié)議才能模型檢測，并不是所有的公開密鑰認(rèn)證協(xié)議都能用模型檢測技術(shù)來分析。在文獻(xiàn)26中給出了能被模型檢測技術(shù)所分析的公開密鑰認(rèn)證協(xié)議的基本假設(shè)，具體描述如下：1)加密部分從文字形式上是可以區(qū)分的公開密鑰認(rèn)證協(xié)議中所用到的加密項從文字上

44、就可以區(qū)分。這意味著一個主體接收到一個加密項就知道這個加密項屬于哪個消息，是消息的哪一部分。這個假設(shè)可以防止入侵者重置協(xié)議中的消息，也能防止入侵者用另一條消息對原消息進(jìn)行替換。這個條件很容易滿足，例如只要在每個加密項中放入項的編號即可。2)身份的可確定性參與協(xié)議運(yùn)行的所有主體的身份是可以通過協(xié)議運(yùn)行中的加密項推導(dǎo)出來的。這樣一個主體當(dāng)他接收了一個加密項后，他就可以確定這個加密項是否為他而發(fā)。更進(jìn)一步，如果這個加密項起源于一個誠實(shí)的主體，接收者可以判斷出誰是加密項的產(chǎn)生者，誰是這個加密項的接收者。假設(shè) 1 和假設(shè) 2 容易滿足，只要在每個加密項中明顯包含每個主體的身份即可：更進(jìn)一步說，如果消息是

45、來自誠實(shí)主體，那么接收方就能確定誰是消息的發(fā)送方和誰是消息的接收方。這兩個假設(shè)條件可避免許多攻擊，并且也使公開密鑰認(rèn)證協(xié)議的分析更容易。3)協(xié)議運(yùn)行時不用協(xié)議運(yùn)行期間建立的任何臨時秘密如果一個特別的數(shù)據(jù)項不是那種要保持為秘密的數(shù)據(jù)項，那么一個監(jiān)視通信的第三者就能夠從有該數(shù)據(jù)項參與的運(yùn)行中獲知此數(shù)據(jù)項的值（或者這個值是公共信息，第三者早已知道它） ；更進(jìn)一步，如果一個特別的密鑰不是那種要保持為秘密的密鑰，那么一個監(jiān)視通信的第三者就能夠通過持有該密鑰的逆參與的運(yùn)行中獲知此密鑰的數(shù)值（或者明顯得到，或者通過加密某些數(shù)據(jù)項） 。（2 2）模型檢測對基于模型的假設(shè)：）模型檢測對基于模型的假設(shè)：1)完善加

46、密假設(shè)協(xié)議采用的密碼系統(tǒng)是完美的，不考慮密碼系統(tǒng)被攻破的情況等。2)入侵者的知識和能力可竊聽與中途攔截系統(tǒng)中傳送的任何消息； . . . 17 / 43可解密用他自己加密密鑰（公鑰或單鑰）加密的消息；在系統(tǒng)中可插入新的消息；即使不知道加密部分的容，也可重放他所看到的任何消息（其中可改變明文部分） ；可運(yùn)用他知道的所有知識（如臨時值等） ，并可產(chǎn)生新的臨時值等。（3 3）模型檢測的結(jié)論）模型檢測的結(jié)論運(yùn)用模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議，就要構(gòu)造小系統(tǒng)模型，關(guān)于小系統(tǒng)的定義和安全性質(zhì)的定義和結(jié)論如下：1)小系統(tǒng)的定義：所謂小系統(tǒng)是指參與協(xié)議運(yùn)行的各主體都是唯一的（例如，一個初始者，一個響應(yīng)者）

47、，作用也是唯一的。這些主體也都是誠實(shí)的：他們嚴(yán)格按照協(xié)議規(guī)定和遵循自己的身份參與協(xié)議運(yùn)行，并不與入侵者運(yùn)行協(xié)議。2)安全性破壞定義：定義 1（強(qiáng)安全性破壞）：一個誠實(shí)的主體相信在協(xié)議運(yùn)行中用到的一個值是僅他和另外誠實(shí)主體之間的共享秘密，但入侵者知道這個值。定義 2（一般安全性破壞）：一個誠實(shí)的主體相信在一個完整協(xié)議運(yùn)行中用到的一個值是僅他和另外誠實(shí)主體之間的共享秘密，但入侵者知道這個值。小系統(tǒng)理論旨在解決：在協(xié)議與其環(huán)境條件下，如果小系統(tǒng)是安全的，那么大系統(tǒng)也是安全的。文獻(xiàn)19中用大量篇幅，創(chuàng)建了一套基于代數(shù)方法的理論，并證明了如下結(jié)論：如果在某一特定的小系統(tǒng)中不存在對協(xié)議強(qiáng)安全性破壞的攻擊，

48、那么對任意系統(tǒng)也不存在強(qiáng)安全性破壞的攻擊，當(dāng)然也就不存在攻擊導(dǎo)致一般安全性破壞的攻擊，即如果小系統(tǒng)是安全的，那么協(xié)議是安全的。小系統(tǒng)理論理論大大減少了安全協(xié)議分析的工作量，并從理論上增強(qiáng)了協(xié)議分析結(jié)果的可信任度。這個理論結(jié)果極促進(jìn)了模型檢測技術(shù)在安全協(xié)議分析領(lǐng)域的廣泛應(yīng)用，使安全協(xié)議形式化分析的主流從邏輯方法轉(zhuǎn)向了模型檢測，進(jìn)而使安全協(xié)議的形式化分析更上一層樓。2.2.2 模型檢測技術(shù)的現(xiàn)狀與存在的問題用模型檢測技術(shù)分析網(wǎng)絡(luò)安全協(xié)議，只要對被分析的協(xié)議在小系統(tǒng)上進(jìn)行強(qiáng)安全性破壞分析，就可以保證協(xié)議在任意系統(tǒng)上的安全性。這一理論大大減少了公開密鑰認(rèn)證協(xié)議分析的工作量，并從理論上保證了人們對協(xié)議分

49、析結(jié)果的信心。所以對于協(xié)議安全性分析來講，模型檢測技術(shù)已經(jīng)證明是一條非常成功的途徑。這種方法發(fā)現(xiàn)了協(xié)議的許多以前未發(fā)現(xiàn)的新的攻擊。但模型檢測技術(shù)仍然存在著一些問題：（1） 現(xiàn)有方法是否作到了理論上所要求的強(qiáng)安全型破壞分析？ . . . 18 / 43（2） 如何評價和衡量不同的檢測方法和檢測工具？（3） 這種分析方法對協(xié)議的種類有所限制，對具有滿足以下情況的協(xié)議不能進(jìn)行分析指導(dǎo)：1)黑匣協(xié)議。2)采用非標(biāo)準(zhǔn)的加密方式的協(xié)議。3)消息中包含長期秘密項的協(xié)議，如主體的私鑰等這類協(xié)議，目前模型檢測無法分析。我們將用于若干次協(xié)議運(yùn)行的數(shù)據(jù)項，如主體的公開密鑰、秘密密鑰等定義為長期項。而將主體在一次協(xié)議

50、運(yùn)行中引入的短期數(shù)據(jù)項，如臨時值，短期密鑰等定義為短期項。長期項和短期項是不同類型的數(shù)據(jù)項。因此，模型檢測分析公開密鑰認(rèn)證協(xié)議仍然存在著不少問題需要解決，其關(guān)鍵在于模型檢測只能分析有限狀態(tài)系統(tǒng)，這必然對公開密鑰認(rèn)證協(xié)議有所要求，因?yàn)閰f(xié)議要能用有限狀態(tài)系統(tǒng)來描述。并且模型檢測技術(shù)本身也存在著諸如可以生成現(xiàn)實(shí)的攻擊路徑，但很難辨別攻擊造成的原因等問題。未來的研究趨勢是如何擴(kuò)大模型檢測分析公開密鑰認(rèn)證協(xié)議的種類并采用混合分析技術(shù)。2.3 兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法2.3.1 兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法簡介運(yùn)行模式分析法由模型檢測技術(shù)分析公開密鑰認(rèn)證協(xié)議若干結(jié)論推導(dǎo)而來。模型檢測技術(shù)分

51、析公開密鑰認(rèn)證協(xié)議的基本方法是構(gòu)造一個運(yùn)行協(xié)議的小系統(tǒng)模型（通常是一個有限狀態(tài)系統(tǒng)） ，同時結(jié)合一個通常意義下的入侵者模型，他能與協(xié)議交互作用，利用狀態(tài)探測工具來發(fā)現(xiàn)系統(tǒng)是否進(jìn)入一個不安全狀態(tài)，也就是說是否對協(xié)議存在一個攻擊。這種方法發(fā)現(xiàn)了公開密鑰認(rèn)證協(xié)議許多以前未發(fā)現(xiàn)的新的攻擊，極促進(jìn)了公開密鑰認(rèn)證協(xié)議分析與設(shè)計的研究工作。在文獻(xiàn)19中基于代數(shù)方法證明了對于一個構(gòu)造的小系統(tǒng)，若協(xié)議在小系統(tǒng)中是安全的，則可以不用考慮任意系統(tǒng)。因?yàn)橐粋€公開密鑰認(rèn)證協(xié)議如果在任意一個系統(tǒng)上有攻擊的話，那么它一定有攻擊在小系統(tǒng)上。這樣只要對被分析的協(xié)議在小系統(tǒng)上進(jìn)行安全分析，就可以保證協(xié)議在任意系統(tǒng)上的安全性。這大

52、大減少了公開密鑰認(rèn)證協(xié)議分析的工作量，并從理論上保證了人們對協(xié)議分析結(jié)果的信心。對公開密鑰認(rèn)證協(xié)議構(gòu)造小系統(tǒng)模型時，對于小系統(tǒng)的分析規(guī)模必須要進(jìn)行恰當(dāng)?shù)闹付?。文獻(xiàn)22中給出當(dāng)對一個公開密鑰認(rèn)證協(xié)議執(zhí)行有限狀態(tài)模型檢測時，有一些涉與分析對象和分析規(guī)模的參數(shù)必須在系統(tǒng)中說明，它們是：（1）參與協(xié)議運(yùn)行的誠實(shí)主體的個數(shù)；（2）每個誠實(shí)主體的身份；（3）每個誠實(shí)主體所能運(yùn)行協(xié)議的次數(shù)； . . . 19 / 43（4）入侵者的身份和能運(yùn)行協(xié)議的次數(shù)。（5）入侵者的初始知識和獲取信息的能力等。對于兩方公開密鑰認(rèn)證協(xié)議（即參與協(xié)議運(yùn)行的只有兩個主體，初始者和響應(yīng)者） ，文獻(xiàn)18中定義了如下的小系統(tǒng)（有限狀

53、態(tài)系統(tǒng)）：參與協(xié)議運(yùn)行的主體集合：初始者 A，響應(yīng)者 B，入侵者 I。其中 A 和 B 是誠實(shí)的主體，他們將嚴(yán)格按照初始者和響應(yīng)者的身份參與協(xié)議運(yùn)行，并且 A 和 B 只運(yùn)行一次公開密鑰認(rèn)證協(xié)議，而入侵者 I 則不受此限制，他既可以以自己本來身份 I參與協(xié)議運(yùn)行，也可以冒充 A 和 B 的身份以 I(A)和 I(B)方式參與協(xié)議運(yùn)行，并可以多次運(yùn)行公開密鑰認(rèn)證協(xié)議。在此小系統(tǒng)前提下，兩方公開密鑰認(rèn)證協(xié)議所有可能的初始者集合和所有可能的響應(yīng)者集合如下所示：初始者集合：A，I，I(A)；響應(yīng)者集合：B，I，I(B)。模型檢測試圖檢查協(xié)議運(yùn)行的所有可能的路徑，對于只有合法用戶 A、B 與入侵者 I

54、的兩方公開密鑰認(rèn)證協(xié)議，根據(jù)對 A、B、I 身份和運(yùn)行次數(shù)的限制，可以得出對于兩方公開密鑰認(rèn)證協(xié)議初始者和響應(yīng)者所有可能的運(yùn)行模式，共有十四種。下面是雙方公開密鑰認(rèn)證協(xié)議運(yùn)行模式的運(yùn)用，其中 XY 表示一次兩方協(xié)議運(yùn)行，X是協(xié)議的初始者，Y 是協(xié)議的響應(yīng)者。這十四種運(yùn)行模式具體描述如下：（1） AB在這種運(yùn)行模式中，A 和 B 運(yùn)行一次協(xié)議，其中 A 作為初始者，B 作為響應(yīng)者，這是協(xié)議正常運(yùn)行情況。（2） AB II這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，A 和 I 運(yùn)行一次協(xié)議，I 和 I 自己運(yùn)行一次協(xié)議。（3） AI這種運(yùn)行模式只有一次協(xié)議運(yùn)行，即 A 和 I 運(yùn)行一次協(xié)議。（4） AI

55、 IB這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，A 和 I 運(yùn)行一次協(xié)議，I 和 B 運(yùn)行一次協(xié)議。（5） AI I(A) B這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，A 和 I 運(yùn)行一次協(xié)議，I 冒充 A 和 B運(yùn)行一次協(xié)議。（6） AI II這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，A 和 I 運(yùn)行一次協(xié)議，I 和 I 自己運(yùn)行一次協(xié)議。（7） AI(B)在這種運(yùn)行模式中，A 和冒充 B 的 I 運(yùn)行協(xié)議。（8） AI(B) IB . . . 20 / 43這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，A 和冒充 B 的 I 運(yùn)行協(xié)議，I 和 B 運(yùn)行一次協(xié)議。（9） AI(B) I(A)B這種運(yùn)行模式包含了

56、兩個并行運(yùn)行的協(xié)議，A 和冒充 B 的 I 運(yùn)行協(xié)議，I 冒充 A和 B 運(yùn)行一次協(xié)議。（10）AI(B) II這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，A 和冒充 B 的 I 運(yùn)行協(xié)議，I 和 I 自己運(yùn)行一次協(xié)議。（11）IB在這種運(yùn)行模式中，I 和 B 運(yùn)行一次協(xié)議。（12）IB II這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，I 和 B 運(yùn)行一次協(xié)議，I 和 I 自己運(yùn)行一次協(xié)議。（13）I(A) B在這種運(yùn)行模式中，I 冒充 A 和 B 運(yùn)行一次協(xié)議。（14）I(A) B II這種運(yùn)行模式包含了兩個并行運(yùn)行的協(xié)議，I 冒充 A 和 B 運(yùn)行一次協(xié)議，I 和 I自己運(yùn)行一次協(xié)議。對于兩方公開密鑰

57、認(rèn)證協(xié)議生成的小系統(tǒng)進(jìn)行安全性分析，只要模型檢測這 14種可能的運(yùn)行模式，如果小系統(tǒng)不存在攻擊的話，則協(xié)議是安全的。2.3.2 對兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式的研究通過研究兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式中的這十四種運(yùn)行模式，我們可以發(fā)現(xiàn)有些運(yùn)行模式是不需要進(jìn)行分析的。例如對于兩方公開密鑰認(rèn)證協(xié)議，II 這種情況對于入侵者 I 來講是不能增加任何知識的，故此運(yùn)行情況中有 II 的都可以不用分析，屬于這種情況的有運(yùn)行模式（2） 、模式（6） 、模式（10） 、模式（12） 、模式（14） 。對于運(yùn)行模式（3） 、模式（11） ，協(xié)議只有一次運(yùn)行，A 或 B 都清楚自己正和一個合法用戶 I 運(yùn)行協(xié)議，

58、同時入侵者 I 以自身身份參與運(yùn)行可以知道這一次協(xié)議運(yùn)行中的所有信息，沒有可騙的第三方，因此也不必分析。這樣對于兩方公開密鑰認(rèn)證協(xié)議只要分析剩余的 7 種運(yùn)行模式即可。也就是說如果對這 7 種運(yùn)行模式進(jìn)行分析，協(xié)議沒有攻擊的話，則整個協(xié)議就是安全的，但有一個前提：對被分析的兩方公開密鑰認(rèn)證協(xié)議必須滿足本章中所給出的對公開密鑰認(rèn)證協(xié)議的所有假設(shè)，否則無法從理論上保證分析結(jié)果的正確性。這 7 種運(yùn)行模式列舉如下：（1）AB（2）AI IB . . . 21 / 43（3）AI I(A) B（4）AI(B) IB（5）AI(B) I(A)B（6）AI(B)（7）I(A) B2.4 小結(jié)本章主要介紹了

59、模型檢測技術(shù)和基于模型檢測技術(shù)的兩方公開密鑰認(rèn)證協(xié)議運(yùn)行模式分析法，并對此方法所需分析的運(yùn)行模式進(jìn)行了研究。運(yùn)用運(yùn)行模式分析法分析公開密鑰認(rèn)證協(xié)議有如下好處：(1)使用運(yùn)行模式法分析公開密鑰認(rèn)證協(xié)議時，可以獨(dú)立于任何模型檢測工具來分析符合要求的兩方公開密鑰認(rèn)證協(xié)議，并且可以檢測不同模型檢測工具在分析兩方公開密鑰認(rèn)證協(xié)議時是否完全覆蓋了這些運(yùn)行模式，從而保證分析的完整性和正確性。(2)使用運(yùn)行模式法分析公開密鑰認(rèn)證協(xié)議時，可以脫離任何模型檢測工具，手工分析符合要求的兩方公開密鑰認(rèn)證協(xié)議。這對于分析簡單的兩方公開密鑰認(rèn)證協(xié)議更為方便。 . . . 22 / 433 模型檢測工具 SMV3.1 引言

60、SMV 系統(tǒng)是一項為了要檢測有限狀態(tài)系統(tǒng)是否符合 CTL（Computation Tree Logic）邏輯所表達(dá)的系統(tǒng)屬性的工具。SMV 的輸入語言允許被設(shè)計成有限狀態(tài)系統(tǒng)的描述，它的圍包括從全同步到全異步，以與從具體到抽象。這種語言提供了模塊分層描述，以與復(fù)用組成功能的定義。CTL 邏輯允許一種豐富的時態(tài)屬性，它包括安全性、靈活性、直接性以與死鎖的解除等等。SMV 使用 OBDD 基礎(chǔ)的符號模型檢測等算法來有效指定在 CTL 中的表達(dá)是否是滿意的。模型檢測工具通過在模型中建立一個包含所有狀態(tài)的圖的方式來驗(yàn)證系統(tǒng)性質(zhì)。在 SMV 中，模型檢測程序只檢測那些從初始狀態(tài)可以到達(dá)的狀態(tài)的路徑是否滿