【文章內容簡介】 安全。因為實際應用中，存在著許多未知的攻擊方法，這種對公開密鑰認證協議的非形式化分析方法只能發(fā)現協議中是否存在著已知的缺陷，而不能全面客觀地來分析公開密鑰認證協議，可能導致不安全的協議經分析是安全 的這樣錯誤的結論。 八十年代以后，隨著對公開密鑰認證協議安全性分析的進一步探索研究，公開密鑰認證協議的形式化分析成為研究熱點。安全協議的形式化分析是采用一種正規(guī)的、標準的方法對協議進行分析，以檢查協議是否滿足其安全目標。這種方法的出發(fā)點是希望將公開密鑰認證協議形式化，然后借助于人工推導，甚至計算機的輔助分析，來判別公開密鑰認證協議是否安全可靠。形式化分析方法和攻擊檢驗方式相比，它能全面、深刻地檢測到公開密鑰認證協議中細微的漏洞。形式化分析方法不僅能發(fā)現現有的攻擊方法對協議構成的威脅，而且還可能通過對公開密鑰 認證協議的安全性分析，發(fā)現協議中細微的漏洞，從而發(fā)現對公開密鑰認證協議新的攻擊方法。 模型檢測技術（ Model Checking Technology）是屬于一般目的的公開密鑰認證協議的形式化分析方法，它是驗證有限狀態(tài)系統(tǒng)的自動化分析工具，常用于硬件電路設計和通信協議。目前模型檢測技術也是一種十分有效的協議形式化分析工具。 模型檢測技術最早是用于分析和模擬硬件工作過程的形式化方法，隨著形式化方法的日益進步和應用領域的推廣，現已應用于軟件分析和通信協議模擬等多個領域，但用于安全協議的分析還是近幾年新的應用。關 于模型檢測的研究越來越受到人們的關注，因為它對協議的自動驗證和協議的工程化設計具有指導意義。 在 1996 年，英國學者 Gavin Lowe 首先使用 CSP 和模型檢測技術對公開密鑰認證協議進行分析 [13]，在這篇文章中， Gavin Lowe 首次采用 CSP 模型和 CSP 模型檢測工具 FDR(故障偏差精煉檢測器， Failures Divergences Refinement Checker)來分析 NeedhanSchroeder 公鑰協議，并成功地找到一個 BAN 類邏輯等分析方法以前未發(fā)現的攻擊。 模型檢測技術應用 于網絡安全協議分析的成功，使學者們相繼投入到這個領域。自 97 年起，計算機科學家及密碼學家開始陸續(xù)應用模型檢測這種新的形式方法來分析網絡安全協議的安全性，對多個網絡安全協議進行了分析，成功地發(fā)現了許多攻擊。 在文獻 [17]中 Steve Schneider 用 CSP 研究了公開密鑰認證協議的安全性質，在文獻 [18]中 和 基于對 CSP 和 FDR研究，認為它們是公開密鑰認證協議完美的檢測工具。 在文獻 [19]中 等提出了一種通用的模型檢測器，構造了他們的 模型及代數理論，并證明該模型的有效性。文中并對 NeedhanSchroeder 公鑰協議進行了分析，也成功地發(fā)現了文獻 [20]所找到的攻擊。 在文獻 [21]中 等設計了一種通用的狀態(tài)計數工具 Murф，并用它來分析公開密鑰認證協議可能達到的狀態(tài)，進一步得出公開密鑰認證協議是否安全的結論。文中分析了 NeedhamSchroeder 協議、 Kerberos 協議和 TMN 協議，并找到了這些協議所有 15 已知的攻擊。 在文獻 [22]中 Zhe Dang 等用 ASTRAL 這種實時系統(tǒng)形式化描述語言 構造了模型檢測器，文中并對 NeedhamSchroeder 公鑰協議和 TMN 協議進行了分析，也成功地發(fā)現了 Gavin Lowe 所找到的所有攻擊。 英國學者 Gavin Lowe 在模型檢測上做出了非凡的創(chuàng)造性成果，相應的結論可參見 [20][13]。其中文獻 [22]是一篇關于模型檢測大全性的文章，文中試圖為模型檢測技術提供一個完整地解決方案。 目前對于協議分析來講，模型檢測已經證明是一條非常成功的途徑，這種方法發(fā)現了協議的許多以前未發(fā)現的新的攻擊，極大地促進了網絡安全協議分析與設計的研究工作。但模型檢測仍然存 在著許多需要進一步研究的問題，最主要的問題在于：模型檢測適用于有限狀態(tài)系統(tǒng)地分析工具，如何將公開密鑰認證協議說明成有限狀態(tài)系統(tǒng)，而又沒有增加或減少公開密鑰認證協議的安全性。這是一個需要繼續(xù)深入研究和探索的核心問題。 論文安排與研究成果 本論文是在結合國家自然科學基金項目“公開密鑰認證協議的模型檢測分析”的基礎上，圍繞著公開密鑰認證協議的模型檢測技術進行了深入的研究，本論文的工作成果如下： 論文安排 第二章： 指出模型檢測技術分析公開密鑰認證協議的現狀； 研究模型檢測技術分析公開密鑰認證協議 的基本理論； 介紹兩方公開密鑰認證協議運行模式分析法并對其進行研究。 第三章： 介紹模型檢測工具 SMV。 第四章 介紹公開密鑰認證協議； 運用運行模式分析法分析公開密鑰認證協議安全性； 嘗試使用 SMV 檢測兩方公開密鑰認證協議的模型檢測。 主要研究成果 以下是我們取得的一些成果： (1) 系統(tǒng)的介紹了公開密鑰認證協議的一些基本概念和公開密鑰認證協議安全性分析的重要意義、研究進展和現狀。 16 (2)研究了模型檢測技術和公開密鑰認證協議運行模式分析法。 (3)給出了運用模型檢測工具 SMV 分析公開密鑰認證 協議的方法。 (4)運用運行模式分析法分析了公開密鑰認證協議，并嘗試使用 SMV 研究了公開密鑰認證協議的安全性檢測。 17 2 模型檢測技術及運行模式分析法研究 本章首先介紹了模型檢測技術和模型檢測技術在公開密鑰認證協議分析領域取得的研究成果；隨后引出了以此技術為理論依據的公開密鑰認證協議運行模式分析法，并對其運行模式作了進一步的研究。 引言 模型檢測技術原是用于分析和模擬硬件工作過程的形式化方法，隨著形式化方法的推廣和應用，模型檢測技術現已用于軟件分析和通信協議模擬等多個領域，但用于公開密鑰認證協議 的分析還是近幾年比較新的應用。 在 1996 年，英國學者 Gavin Lowe 首先使用 CSP 和模型檢測技術對公開密鑰認證協議進行分析 [20]。并首次采用 CSP 模型和 CSP 模型檢測工具 FDR(故障偏差精煉檢測器， Failures Divergences Refinement Checker)，來分析 NeedhamSchroeder 公鑰協議。在這個模型中，協議參與者被說明成 CSP 中的進程 (process)，消息說明成事件（ event），進而將協議說明成一個通信順序進程的集合，這些進程并行運行而且和他們的環(huán)境交互作 用，其對公開密鑰認證協議的驗證是從協議說明中抽取一個模型（通常是一個有限狀態(tài)轉換系統(tǒng)），然后用 FDR 檢測，從而證明協議的安全性。此方法成功地找到 NeedhamSchroeder 協議的一個以前從未發(fā)現的攻擊。 模型檢測的成功，使研究者們相繼投入到這個領域。實踐證明對于公開密鑰認證協議安全性分析來講，模型檢測是一條非常成功的途徑。 模型檢測技術分析公開密鑰認證協議的基本理論 模型檢測技術分析公開密鑰認證協議的理論研究 模型檢測技術可以抽象地描述為：給定一個模型 M 和邏輯描述的性質 P，檢查 模型 M中性質 P是否成立。模型檢測技術對協議進行驗證與分析，是通過檢查在惡意攻擊者存在的情況下，協議運行的所有可能的路徑，來判斷協議是否實現了其安全保證；如果沒有，將給出攻擊者的攻擊路徑。 模型檢測用于有限狀態(tài)系統(tǒng)的分析，要用模型檢測技術分析公開密鑰認證協議，就要研究如何為公開密鑰認證協議構造有限狀態(tài)系統(tǒng)。目前，模型檢測技術分析公開密鑰認證協議的基本方法主要采用英國學者 Gavin Lowe 研究成果，即：生成一個協議運行的小系統(tǒng)模型（通常是一個有限狀態(tài)轉換系統(tǒng)），以及一個可與協議互操作的攻擊者模型，并用狀態(tài)探測 工具檢測系統(tǒng)是否進入一個不安全狀態(tài)，即是否存在對協 18 議的攻擊。并且基于代數理論證明：如果小系統(tǒng)是安全的，那么協議是安全的。 這種方法提出了將大系統(tǒng)中協議安全的性質研究約化為小系統(tǒng)中協議安全性質的研究，這是目前這一領域的最新理論研究成果。使用該方法發(fā)現了公開密鑰認證協議許多以前未發(fā)現的新的攻擊，極大地促進了公開密鑰認證協議分析與設計的研究工作。 （ 1）模型檢測對被分析協議的基本假設： 任何一個系統(tǒng)都有其賴以存在的假設條件，用以避免結論的不當使用以及對一些限制的理解，同樣，用模型檢測技術分析公開密鑰認證協議 ，對協議是有一定要求的，因為只有能用有限狀態(tài)描述且滿足一定條件的協議才能模型檢測，并不是所有的公開密鑰認證協議都能用模型檢測技術來分析。在文獻 [26]中給出了能被模型檢測技術所分析的公開密鑰認證協議的基本假設，具體描述如下： 1)加密部分從文字形式上是可以區(qū)分的 公開密鑰認證協議中所用到的加密項從文字上就可以區(qū)分。這意味著一個主體接收到一個加密項就知道這個加密項屬于哪個消息，是消息的哪一部分。這個假設可以防止入侵者重置協議中的消息，也能防止入侵者用另一條消息對原消息進行替換。 這個條件很容易滿足，例如只要在 每個加密項中放入項的編號即可。 2)身份的可確定性 參與協議運行的所有主體的身份是可以通過協議運行中的加密項推導出來的。這樣一個主體當他接收了一個加密項后，他就可以確定這個加密項是否為他而發(fā)。更進一步，如果這個加密項起源于一個誠實的主體，接收者可以判斷出誰是加密項的產生者，誰是這個加密項的接收者。 假設 1 和假設 2 容易滿足，只要在每個加密項中明顯包含每個主體的身份即可：更進一步說，如果消息是來自誠實主體，那么接收方就能確定誰是消息的發(fā)送方和誰是消息的接收方。 這兩個假設條件可避免許多攻擊，并且也使公開密鑰認證 協議的分析更容易。 3)協議運行時不用協議運行期間建立的任何臨時秘密 如果一個特別的數據項不是那種要保持為秘密的數據項，那么一個監(jiān)視通信的第三者就能夠從有該數據項參與的運行中獲知此數據項的值（或者這個值是公共信息，第三者早已知道它）；更進一步，如果一個特別的密鑰不是那種要保持為秘密的密鑰，那么一個監(jiān)視通信的第三者就能夠通過持有該密鑰的逆參與的運行中獲知此密鑰的數值（或者明顯得到，或者通過加密某些數據項）。 （ 2）模型檢測對基于模型的假設： 1)完善加密假設 協議采用的密碼系統(tǒng)是完美的，不考慮密碼系統(tǒng)被攻破的 情況等。 2)入侵者的知識和能力 ①可竊聽及中途攔截系統(tǒng)中傳送的任何消息； ②可解密用他自己加密密鑰（公鑰或單鑰）加密的消息； ③在系統(tǒng)中可插入新的消息； 19 ④即使不知道加密部分的內容，也可重放他所看到的任何消息（其中可改變明文部分）； ⑤可運用他知道的所有知識（如臨時值等），并可產生新的臨時值等。 （ 3）模型檢測的結論 運用模型檢測技術分析公開密鑰認證協議，就要構造小系統(tǒng)模型，關于小系統(tǒng)的定義和安全性質的定義和結論如下： 1)小系統(tǒng)的定義： 所謂小系統(tǒng)是指參與協議運行的各主體都是唯一的（例如，一個初 始者，一個響應者），作用也是唯一的。這些主體也都是誠實的：他們嚴格按照協議規(guī)定和遵循自己的身份參與協議運行，并不與入侵者運行協議。 2)安全性破壞定義： 定義 1（強安全性破壞）： 一個誠實的主體相信在協議運行中用到的一個值是僅他和另外誠實主體之間的共享秘密，但入侵者知道這個值。 定義 2（一般安全性破壞）： 一個誠實的主體相信在一個完整協議運行中用到的一個值是僅他和另外誠實主體之間的共享秘密，但入侵者知道這個值。 小系統(tǒng)理論旨在解決：在協議及其環(huán)境條件下，如果小系統(tǒng)是安全的，那么大系統(tǒng)也是安全的。文獻 [19]中用大量篇幅，創(chuàng)建了一套基于代數方法的理論，并證明了如下結論： 如果在某一特定的小系統(tǒng)中不存在對協議強安全性破壞的攻擊，那么對任意系統(tǒng)也不存在強安全性破壞的攻擊，當然也就不存在攻擊導致一般安全性破壞的攻擊，即如果小系統(tǒng)是安全的，那么協議是安全的。 小系統(tǒng)理論理論大大減少了安全協議分析的工作量，并從理論上增強了協議分析結果的可信任度。這個理論結果極大地促進了模型檢測技術在安全協議分析領域的廣泛應用，使安全協議形式化分析的主流從邏輯方法轉向了模型檢測，進而使安全協議的形式化分析更上一層樓。 模型檢測技 術的現狀及存在的問題 用模型檢測技術分析網絡安全協議，只要對被分析的協議在小系統(tǒng)上進行強安全性破壞分析，就可以保證協議在任意系統(tǒng)上的安全性。這一理論大大減少了公開密鑰認證協議分析的工作量，并從理論上保證了人們對協議分析結果的信心。 所以對于協議安全性分析來講，模型檢測技術已經證明是一條非常成功的途徑。這種方法發(fā)現了協議的許多以前未發(fā)現的新的攻擊。但模型檢測技術仍然存在著一些問題： （ 1） 現有方法是否作到了理論上所要求的強安全型破壞分析？ （ 2） 如何評價和衡量不同的檢測方法和檢測工具？ （ 3） 這種分析方法對協議的種類有所限制， 對具有滿足以下情況的協議不能進 20 行分析指導： 1)黑匣協議 。 2)采用 非標準的加密方式的協議。 3)消息中包含長期秘密項的協議，如主體的私鑰等這類協議，目前模型檢測無法分析。 我們將用于若干次協議運行的數據項，如主體的公開密鑰、秘密密鑰等定義為長期項。而將主體在一次協議運行中引入的短期數據項，如臨時值，短期密鑰等定義為短期項。長期項和