【導(dǎo)讀】指導(dǎo)下進行的研究工作及取得的成果。盡我所知，除文中特別加以標(biāo)注。和致謝的地方外，不包含其他人或組織已經(jīng)發(fā)表或公布過的研究成果，了明確的說明并表示了謝意。的規(guī)定，即：按照學(xué)校要求提交畢業(yè)設(shè)計（論文）的印刷本和電子版本；閱覽服務(wù)；學(xué)?？梢圆捎糜坝　⒖s印、數(shù)字化或其它復(fù)制手段保存論文；在不以贏利為目的前提下，學(xué)?？梢怨颊撐牡牟糠只蛉績?nèi)容。對本文的研究做出重。要貢獻的個人和集體，均已在文中以明確方式標(biāo)明。本人完全意識到本。聲明的法律后果由本人承擔(dān)。文被查閱和借閱。本人授權(quán)大學(xué)可以將本學(xué)位論文的全部。涉密論文按學(xué)校規(guī)定處理。類論文正文字數(shù)不少于萬字。家技術(shù)標(biāo)準規(guī)范。系統(tǒng)介紹了公開密鑰認證協(xié)議的基本概念及安全性分析的重要意義、研究進展和。給出了運用模型檢測工具SMV分析公開密鑰認證協(xié)議的方法。性，成功地發(fā)現(xiàn)了該協(xié)議的安全漏洞。

　　

【正文】 一樣，這可以通過后面的例子理解這一點。概括地說， SMV輸入語言是一種描述并發(fā)的語言。 時態(tài)邏輯 CTL 模型檢測主要是驗證某一模型生成的有限狀態(tài)系統(tǒng)是否滿足模型所要求的屬性。在 SMV 中，有限狀態(tài)系統(tǒng)的屬性是作為一個時態(tài)邏輯 CTL 表達式公式給出的。在時態(tài)邏輯中，公式的真值是時間的函數(shù)。在 SMV 中，系統(tǒng)的 詳細說明作為一個暫時邏輯CTL 表達式公式被給出， CTL表達式通過關(guān)鍵字 SPEC 引出，其聲明的語法定義為： dec1 : : “SPEC ” ctlform CTL 公式的語法如下： ctlform : : expr 。 。 布爾表達式 27 | “! ” ctlform 。 。 邏輯反 | ctlform1 “amp。 ” ctlform2 。 。 邏輯與 | ctlform1 “| ” ctl form2 。 。 邏輯或 | ctlform1 “ ? ” ctlform2 。 。 邏輯蘊涵 | ctlform1 “ ? ” cltform2 。 。 邏輯等價 | “E ” pathform 。 。 存在路徑量詞 | “A ” pathform 。 。 全局路徑量詞 路徑語法是： pathform : : “X ” ctlform 。 。 下一 時間（ next time） “F ” ctlform 。 。 最終（ eventually） “G ” ctlform 。 。 全局（ globally） ctlform1 “U ” ctlform2 。 。 直到（ until） 如果有多個 SPEC 聲明，則詳細說明就是所有 SPEC 聲明的邏輯乘。 SMV 實例 下面的 SMV例子是使用一個變量信號 semaphore來執(zhí)行兩個異步進程之間的相互的排斥 。每個進程都有四個狀態(tài)： idle（空閑） , entering（進入） , critical（臨界） , exiting（退出）。 entering 狀態(tài)表示進程想進入它的臨界區(qū)域，如果信號量semaphore 是零的話，它將進入臨界狀態(tài)，并置 semaphore 為 1，當(dāng)退出它的臨界區(qū)域，進程將重新設(shè)置 semaphore 變量為 0。 MODULE main 主模塊 VAR semaphore : boolean 。 公用變量 semaphore proc1 : process user 。 進程 1 proc2 : process user 。 進程 2 ASSIGN 賦值聲明 ASSIGN init (semaphore) : = 0 。 semaphore 變量賦初值 SPEC AG ( = entering ? AF = critical) CTL 表達式含義： 任何時候只要進程 1 的 state 變量一旦取值 entering 那么進程 1一定進入臨界區(qū) MODULE user user 模塊 VAR 28 state : {idle, entering, critical, exiting} 。 狀態(tài)變量取值集合 ASSIGN init (state) : = idle 。 state 變量賦初值 next (state) : = state 變量下一步取值 case case 分支語句 state = idle : {idle, entering} 。 state = entering amp。 !semaphore : critical 。 state = critical : {critical, exiting} 。 state = exiting : idle 。 1 : state 。 esac 。 next (semaphore) : = semaphore 變量下一步取值 case state = entering : 1 。 state = exiting : 0 。 1 : semaphore 。 esac 。 FAIRNESS 迫使 user 進程無限運行 running 整個程序的意思是，如果 proc1 想進入它的 critical 區(qū)域，它最終可以做到。這種情況下的模型檢測輸出結(jié)果如下。這個反例顯示了一條 proc1 進入 entering 狀態(tài)的路徑，后接了一個循環(huán)： proc2 重復(fù)進入它的 critical 區(qū)域以及返回它的 idle狀態(tài)，而 proc1 進程只有當(dāng) proc2 在 critical 區(qū)域時才能被執(zhí)行。這條路徑表示 CTL表達的系統(tǒng)屬性是錯誤的，因為 proc1 一直沒有進入它的 critical 區(qū)域。 運行結(jié)果： specification is false AG ( = entering AF . . . is false 系統(tǒng)屬性不滿足，下面是反例 . semaphore = 0 變量取初值 . = idle . = idle next state : [executing process . proc1] 程序隨機選取 proc1 運行 next state : 29 . = entering proc1 中 state 變量被賦 entering AF = critical is false : AF = critical 為假 [executing process . proc2] 程序隨機選取 proc2運行 next state : [executing process . proc2] . = entering proc2中 state 變量被賦值 entering next state : [executing process . proc1] . semaphore =1 semaphore 變量值發(fā)生了改變 . = critical 引起 proc2 進入臨界區(qū) next state : . = exiting . semaphore = 0 . = idle 30 4 運行模式及 SMV 分析公開密鑰認證協(xié)議實例研究 引言 公開密鑰認證協(xié)議的安全性是計算機網(wǎng)絡(luò)安全的重要基礎(chǔ)，但迄今為止公開密鑰認證協(xié)議的安全性的論證仍是一個懸而未決的問題，為此需要對公開密鑰認證協(xié)議的安全性分析進行深入研究和探索。實踐證明對于公開密鑰認證協(xié)議分析來講 ,模型 檢測是一條非常成功的途徑。本章也正是基于模型檢測技術(shù) , 運用運行模式分析法對自行設(shè)計的僅有兩個主體 (初始者和響應(yīng)者 )參與的兩方公開密鑰認證協(xié)議公開密鑰認證協(xié)議進行了安全分析，并進一步研究了公開密鑰認證協(xié)議的 SMV 檢測程序，驗證了模型檢測的有效性。 公開密鑰認證協(xié)議 記號表示此協(xié)議： A? B: Eb(A,Ra) B? A: Ea(Ra,Rb,Ks) A? B： Eb(Ks) 其中， A， B 是分別代表兩個網(wǎng)絡(luò)用戶的標(biāo)識。 Ri 是質(zhì)詢（即一個大的隨機數(shù)） ,其中下表指明了發(fā)起質(zhì)詢的一方。 Ei 是公鑰，這里 i代表公鑰的所有者。 Ks 是會話密鑰。 協(xié)議的目的是使初始者 A 和響應(yīng)者 B之間建立一個互相的認證的密鑰，即確認進行通信的雙方是初始者 A 和響應(yīng)者 B，而不是和入侵者 I進行通信。 參與協(xié)議的主體有兩個：初始者 A和響應(yīng)者 B。整個協(xié)議由三個消息組成，其中Ks 表示初始者 A 和響應(yīng)者 B之間所共有的秘密密鑰（沒有第三者知道的密鑰）， Ea 是A 的公鑰， Ra表示 A 產(chǎn)生的一個隨機數(shù)， Eb 是 B 的公鑰， Rb表示 B產(chǎn)生的一個隨機數(shù)，協(xié)議的具體運行步驟如下： （ 1）初始者 A 要想與響應(yīng)者 B 通信，則 A 首先給響應(yīng)者 B 送出消息 1，其中 A表示 A 自己的身份， Ra表示初始者 A產(chǎn)生的一個隨機數(shù)。 （ 2）響應(yīng)者 B在接受到消息 1 后，得知是初始者 A要與自己通信并給出了隨機數(shù) Ra，則送出消息 2 給初始者 A，其中 Rb是響應(yīng)者 B 產(chǎn)生的隨機數(shù)， Ra是在接受到的消息 1 中初始者 A 產(chǎn)生的隨機數(shù)， Ks (Ra)表示響應(yīng)者 B用他們的共開密鑰 Ks 加密隨機數(shù) Ra。 （ 3）初始者 A在接受到消息 2 后，驗證響應(yīng)者 B 對隨機數(shù) Ra的加密是否正確。如果正確的話即可以證 明正在與自己通信的是響應(yīng)者 B（應(yīng)為公開密鑰是在安全的情況下建立的，不會有第三者知道并正確加密隨機數(shù) Ra），并對響應(yīng)者 B發(fā)過來的隨機 31 數(shù) Rb 用公開密鑰 Ks 進行加密并送給響應(yīng)者 B。響應(yīng)者 B在接受到初始者 A發(fā)送過來的密文后進行必要的檢查。如果正確的話即可以證明正在與自己通信的是初始者 A（應(yīng)為公開密鑰是在安全的情況下建立的，不會有第三者知道并正確加密隨機數(shù)Rb），于是初始者 A和響應(yīng)者 B 之間的公開密鑰 Ks 產(chǎn)生。 運用模式法分析公開密鑰認證協(xié)議 行模式分析法分析公開密鑰認證協(xié)議的方法。進一步我們就可以用此方法對其它的兩方協(xié)議進行類似的分析研究，從而判斷一個兩方公開密鑰認證協(xié)議是否存在攻擊。 在這里，我們使用下面的記號表示此協(xié)議： A? B: Eb(A,Ra) B? A: Ea(Ra,Rb,Ks) A? B： Eb(Ks) 其中， A， B 是分別代表兩個網(wǎng)絡(luò)用戶的標(biāo)識。 Ri 是質(zhì)詢（即一個大的隨機數(shù)） ,其中下表指明了發(fā)起質(zhì)詢的一方。 Ei 是公鑰，這里 i代表公鑰的所有者。 Ks 是會話密鑰。 使用公開密鑰密碼學(xué)的認證協(xié)議，可滿足被分析的密碼協(xié)議假設(shè)要求，故此我們在下面對使用公開密鑰密碼學(xué)的認證協(xié)議，用七種運行模式進行了詳盡的分析： （ 1） 運行模式 1 運行模式 1 為使用公開密鑰密碼學(xué)的認證協(xié)議正常的運行模式，經(jīng)過分析可知這種運行模式下使用公開密鑰密碼學(xué)的認證協(xié)議運行只能為： 消息 1 A? B: Eb(A,Ra) 消息 2 B? A: Ea(Ra,Rb,Ks) 消息 3 A? B： Eb(Ks) 這種運行模式下使用公開密鑰密碼學(xué)的認證協(xié)議是安全的，不存在攻擊。 （ 2） 運行模式 2 運行模式 2 中，入侵者 I 以自身身份參與協(xié)議運行，但未有任何冒充，經(jīng)過分析知道，公開密鑰認證議運行具體過程為： 消息 A? I: Eb(A,Ra) 消息 I? A：入侵者 I 冒充 B無法給出消息 。會話終止。 在以上運行過程中，入侵者 I 以自身身份分別作為響應(yīng)者和初始者分別與 A、 B進行通信。在協(xié)議第一次運行（即會話 1）中，初始者 A 的響應(yīng)者為 I，那么他認為是和 I 通信，對于消息 中的會話密鑰數(shù)據(jù)域 A 不會送出初始者 A 與響應(yīng)者 B的公 32 開密鑰 Ks，而只送出與 I 的公開密鑰 Kai，因此入侵者 I不可能獲知 Ks 。這樣在這個運行模式中，入侵者 I 既沒有獲取他不應(yīng)該知道的信息，也沒有作任何冒充來欺騙A 或 B。所以在這個運行模式中，使用公開密鑰密碼學(xué)的認證協(xié)議是安全的，沒有攻擊。 （ 3） 運行模式 3 運行模式 3 中，入侵者 I冒充響應(yīng)者 B與初始者 A 通信，并且它還以自身身份作為初始者與響應(yīng)者 B 進行通信。協(xié)議運行 過程如下： 消息 A→ I(B)： Eb(A,Ra) 消息 I(B)→ A：入侵者 I冒充 B 無法給出消息 。會話終止。 首先，在協(xié)議第一次運行（即會話