【正文】 用同步認證方式，即需要各認證實體之間嚴格保持一個同步時鐘。 12（6）偽造攻擊入侵者通過偽造一條假協(xié)議消息進行攻擊。（3）中間人攻擊當攻擊者能夠中途截獲發(fā)送端的消息，讀出它們并將它們發(fā)送給接收端(反之亦然)時， “中間人”攻擊就可能發(fā)生。（1）重放攻擊重放攻擊主要指攻擊者利用其消息再生能力生成誠實用戶所期望的消息格式并重放，從而達到破壞協(xié)議安全性質的目的。但是，在一些情況下，合法用戶可以檢測到主動欺騙的存在并采取一定的防范措施。他可能在協(xié)議執(zhí)行中撒謊，或者根本不遵守協(xié)議。他們可能在協(xié)議中加入新的消息、刪除消息、替換消息、重發(fā)舊消息、干擾信道或修改計算機中存儲的消息。這種攻擊實際上屬于一種惟密文攻擊。一般對協(xié)議自身的攻擊可以分為被動攻擊和主動攻擊。造成認證協(xié)議存在安全漏洞的原因有很多，我們通過對協(xié)議的安全性進行分析，可以發(fā)現(xiàn)協(xié)議的設計漏洞，反過來可以進一步指導協(xié)議的設計。雖然公開密鑰認證協(xié)議中僅僅進行很少的幾組消息傳輸，但是其中的每一消息的組成都是經過巧妙設計的，而且這些消息之間有著復雜的相互作用和制約。（2）認證建立協(xié)議（Authentication Protocol） ，向一個實體提供對他想要進行通信的另一個實體的身份的某種程度的確信。因為將公開密鑰認證協(xié)議進行嚴格分類是很難的事情，從不同的角度出發(fā)，就有不同的分類方法。安全協(xié)議為了保證安全性，在設計時必須采用密碼技術。一個人可以通過執(zhí)行一系列的步驟來完成某項任務，但它不構成協(xié)議。所謂協(xié)議（Protocol） ，就是兩個或兩個以上的參與者為完成某項特定的任務而采取的一系列步驟。2 公開密鑰認證協(xié)議 公開密鑰認證協(xié)議的基本概念通過網絡來建立計算機系統(tǒng)之間的安全通信并證明此通信是安全的，不僅是一個日益受到關注的學術研究領域，而且也對社會生活具有非常重要的意義。公鑰密碼的快速實現(xiàn)是當前公鑰密碼研究中的一個熱點，包括算法優(yōu)化和程序優(yōu)化。而基于離散對數問題的公鑰密碼在目前技術下 512 比特模長就能夠保證其安全性。自從 1976 年公鑰密碼的思想提出以來，國際上已經提出了許多種公鑰密碼體制，但比較流行的主要有兩類：一類是基于大整數因子分解問題的，其中最典型的代表是 RSA；另一類是基于離散對數問題的，比如 ElGamal 公鑰密碼和影響比較大的橢圓曲線公鑰密碼。所以，網絡協(xié)議本身是否存在安全隱患是信息安全的一個重要因素。 關鍵詞：公開密鑰認證協(xié)議，模型檢測協(xié)議分析，形式方法，運行模式分析法， SMV 5AbstractAnalysis of security protocols has a significance to promote the information construction and the research of the work 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 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 protocol, Use the runningmode analysis approach based on the twoparty 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 twoparty protocol.?Keywords: Cryptographic protocolModel, checkingprotocol analysis, Formal methods，Runningmode, analysis approach， SMV 6目錄中文摘要 .........................................Ⅰ英文摘要 .........................................Ⅱ1 緒論 ...........................................1 本課題的開發(fā)背景以及開發(fā)意義............................... 1 國內外研究現(xiàn)狀............................................. 1 本課題研究的主要內容 ............................22 公開密鑰認證協(xié)議 ................................1 公開密鑰認證協(xié)議的基本概念................................. 1 公開密鑰認證協(xié)議分類....................................... 2 公開密鑰認證協(xié)議的安全性及其設計規(guī)范....................... 2 公開密鑰認證協(xié)議的安全性分析及攻擊 ...................3 安全協(xié)議設計規(guī)范 .....................................4 公開密鑰認證協(xié)議模型檢測分析技術的研究與進展............... 6 論文安排與研究成果......................................... 7 論文安排 .............................................8 主要研究成果 .........................................83 模型檢測技術及運行模式分析法研究 ...................9 引言....................................................... 9 模型檢測技術分析公開密鑰認證協(xié)議的基本理論................. 9 模型檢測技術分析公開密鑰認證協(xié)議的理論研究 ...........9 模型檢測技術的現(xiàn)狀及存在的問題.......................12 兩方公開密鑰認證協(xié)議運行模式分析法........................13 兩方公開密鑰認證協(xié)議運行模式分析法簡介...............13 對兩方公開密鑰認證協(xié)議運行模式的研究.................15 小結......................................................16 74 模型檢測工具 SMV.................................17 引言......................................................17 SMV 語言語法及 CTL 表達式...................................18 SMV 語言語法 ........................................18 時態(tài)邏輯 CTL.........................................20 SMV 實例.................................................215 運行模式及 SMV 分析公開密鑰認證協(xié)議實例研究..........24 引言......................................................24 公開密鑰認證協(xié)議..........................................24 運用模式法分析公開密鑰認證協(xié)議............................25 公開密鑰認證協(xié)議安全性檢測的 SMV 程序分析..................29 公開密鑰認證協(xié)議的消息的定義 ........................29 公開密鑰認證協(xié)議的有限狀態(tài) ..........................30 公開密鑰認證協(xié)議的 SMV 程序的數據結構 ................31 公開密鑰認證協(xié)議的主模塊框架和有限狀態(tài)屬性 ..........33 公開密鑰認證協(xié)議的安全性分析 ........................35 小結......................................................36 6 總 結 .........................................37參考文獻 ...............................................38致謝 ...................................................39畢業(yè)設計（論文）知識產權聲明 ...........................40畢業(yè)設計（論文）獨立性聲明 .............................41英文翻譯 ...............................................41譯文原文 ...............................................48 81 緒 論本章主要系統(tǒng)地介紹了公開密鑰認證協(xié)議的基本概念和公開密鑰認證協(xié)議的分類，討論了公開密鑰認證協(xié)議的安全性及其設計規(guī)范，概述了公開密鑰認證協(xié)議模型檢測技術分析公開密鑰認證協(xié)議安全性方法的重要意義、研究進展和現(xiàn)狀。? 研究了模型檢測技術以及公開密鑰認證協(xié)議運行模式分析法。圖表整潔，布局合理，文字注釋必須使用工程字書寫，不準用徒手畫3）畢業(yè)論文須用 A4 單面打印，論文 50 頁以上的雙面打印4）圖表應繪制于無格子的頁面上5）軟件工程類課題應有程序清單，并提供電子文檔1）設計（論文）2）附件：按照任務書、開題報告、外文譯文、譯文原文（復印件）次序裝訂3）其它 4基于公開密鑰認證協(xié)議安全性的分析與研究摘 要 公開密鑰認證協(xié)議安全性分析與研究對于促進我國信息化建設以及網絡安全和信息安全研究具有非常重要的意義。涉密論文按學校規(guī)定處理。對本文的研究做出重要貢獻的個人和集體，均已在文中以明確方式標明。對本研究提供過幫助和做出過貢獻的個人或集體，均已在文中作了明確的說明并表示了謝意。盡我所知，除文中特別加以標注和致謝的地方外，不包含其他人或組織已經發(fā)表或公布過的研究成果，也不包含我為獲得 及其它教育機構的學位或學歷而使用過的材料。除了文中特別加以標注引用的內容外，本論文不包含任何其他個人或集體已經發(fā)表或撰寫的成果作品。本人授權　　 　 　大學可以將本學位論文的全部或部分內容編入有關數據庫進行檢索，可以采用影印、縮印或掃描等復制手段保存和匯編本學位論文。、圖表要求：1）文字通順，語言流暢，書寫字跡工整，打印字體及大小符合要求，無錯別字，不準請他人代寫2）工程設計類題目的圖紙，要求部分用尺規(guī)繪制，部分用計算機繪制，所有圖紙應符合國家技術標準規(guī)范。研究成果如下：? 系統(tǒng)介紹了公開密鑰認證協(xié)議的基本概念及安全性分析的重要意義、研究進展和現(xiàn)狀。并在學習了 SMV 模型檢測工具的基礎上，研究了公開密鑰認證協(xié)議的 SMV 檢測程序的框架和數據結構。網絡作為現(xiàn)代信息傳遞的一個重要載體，其安全性是整個信息基礎架構的安全基礎，而網絡的安全性離不開安全的網絡協(xié)議。此次畢業(yè)設計主要運用模型檢測技術分析公開密鑰認證協(xié)議的理論與技術。一般建議使用 1024 比特模長，預計要保證 20 年的安全就要選擇 1280 比特的模長，增大模長帶來了實現(xiàn)上的難度。我國學者也提出了一些公鑰密碼，另外在公鑰密碼的快速實現(xiàn)方面也做了一定的工作，比如在 RSA 的快速實現(xiàn)和橢圓曲線公鑰密碼的快速實現(xiàn)方面都有所突破。（3） 嘗試運用模型檢測工具 SMV 系統(tǒng)對公開密鑰協(xié)議的安全性進行分析和研究。由于人們能夠熟練地使用這些協(xié)議來有效地完成所要做的事情，所以很少有人去深入地考慮它們。第二、協(xié)議至少需要兩個參與者。我們把為了完成某種安全任務的協(xié)議稱為安全協(xié)議。 公開密鑰認證協(xié)議分類到目前為止，還未有人對公開密鑰認證協(xié)議進行