【正文】 : process user 。 進程 2ASSIGN 賦值聲明 ASSIGN init (semaphore) : = 0 。 semaphore 變量賦初值SPEC AG ( = entering ? AF = critical) CTL 表達式含義： 任何時候只要進程 1 的 state 變量一旦取值 entering 那么進程 1 一定進入臨界區(qū) 27MODULE user user 模塊VAR 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 進程只有當 proc2 在 critical 區(qū)域時才能被執(zhí)行。這條路徑表示CTL 表達的系統(tǒng)屬性是錯誤的，因為 proc1 一直沒有進入它的 critical 區(qū)域。運行結(jié)果：specification is falseAG ( = entering AF . . . is false 系統(tǒng)屬性不滿足，下面是反例. semaphore = 0 變量取初值. = idle. = idlenext state : [executing process . proc1] 程序隨機選取 proc1 運行 28next state : . = entering proc1 中 state 變量被賦 enteringAF = critical is false : AF = critical 為假[executing process . proc2] 程序隨機選取 proc2 運行next state :[executing process . proc2]. = entering proc2 中 state 變量被賦值 enteringnext state :[executing process . proc1]. semaphore =1 semaphore 變量值發(fā)生了改變. = critical 引起 proc2 進入臨界區(qū)next state :. = exiting. semaphore = 0. = idle294 運行模式及 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ò)用戶的標識。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ā)過來的30隨機數(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ò)用戶的標識。Ri 是質(zhì)詢（即一個大的隨機數(shù)）,其中下表指明了發(fā)起質(zhì)詢的一方。Ei 是公鑰，這里 i 代表公鑰的所有者。Ks 是會話密鑰。使用公開密鑰密碼學的認證協(xié)議，可滿足被分析的密碼協(xié)議假設(shè)要求，故此我們在下面對使用公開密鑰密碼學的認證協(xié)議，用七種運行模式進行了詳盡的分析：（1） 運行模式 1運行模式 1 為使用公開密鑰密碼學的認證協(xié)議正常的運行模式，經(jīng)過分析可知這種運行模式下使用公開密鑰密碼學的認證協(xié)議運行只能為： 消息 1 A B: Eb(A,Ra)? 消息 2 B A: Ea(Ra,Rb,Ks) 消息 3 A B： Eb(Ks)這種運行模式下使用公開密鑰密碼學的認證協(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 的31公開密鑰 Ks，而只送出與 I 的公開密鑰 Kai，因此入侵者 I 不可能獲知 Ks 。這樣在這個運行模式中，入侵者 I 既沒有獲取他不應(yīng)該知道的信息，也沒有作任何冒充來欺騙 A 或 B。所以在這個運行模式中，使用公開密鑰密碼學的認證協(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é)議第一次運行（即會話 1）中，初始者 A 認為自己是在和響應(yīng)者 B進行通信，于是就送出了與運行模式 1 中相同的消息 ，入侵者 I 截取此消息并冒充 B，但 I 接收到這個用 B 的公開密鑰 Kb 加密的消息后，他無法解密消息 ，所以他也沒有辦法回送初始者 A 消息 ，協(xié)議運行 1 無法完成。協(xié)議運行 2 中，入侵者 I 以自身身份作為初始者與響應(yīng)者 B 進行通信，他無法欺騙響應(yīng)者 B。所以運行模式 3 中，使用公開密鑰密碼學的認證協(xié)議不存在攻擊。（4） 運行模式 4運行模式 4 中，入侵者 I 以自身身份作為響應(yīng)者與初始者 A 參與協(xié)議運行，另外它又冒充初始者 A 與響應(yīng)者 B 進行通信，協(xié)議運行的具體過程如下：消息 A→I: Eb(A,Ra)消息 I→A: 由于入侵者 I 不知道響應(yīng)者 B 的公開密鑰，所以無法給出消息 . 消息 I(A)→B： Eb(A,Ra) 消息 B→I(A)： Ea(Ra,Rb,Ks) 消息 I(A)→B：入侵者 I 冒充 B 無法給出消息 在協(xié)議運行 1 中，A 送出的消息 中的給出了自己的標識符 A 和質(zhì)詢隨機數(shù)Ra,并用 B 的公開密鑰加密。由于入侵者 I 不知道響應(yīng)者 B 的公開密鑰，所以無法給出消息 I 冒充初始者 A 與響應(yīng)者 B 進行協(xié)議 2 運行時，首先入侵者 I把消息 中的初始者身份賦為 A，以冒充初始者 A 與響應(yīng)者 B 通信。在 B 給 A(即冒充者 I)的消息 中給出了自己的用初始者 A 的公開密鑰加密的初始者 A 的質(zhì)詢隨機數(shù) Ra 和自己的質(zhì)詢隨機數(shù) Rb 以及自己建議的會話密鑰 Ks。由于 I 不知道 A 的公開密鑰 Ea，所以他既不能正確識別會話密鑰 Ks，也不能對 B 的建議的會話密鑰進行正確的加密，所以 I 無法冒充 A 給 B 給出正確的消息 。所以在這種運行模式下也不存在攻擊。（5） 運行模式 5運行模式 5 中，入侵者 I 既冒充響應(yīng)者 B 又冒充初始者 A，分別與初始者 A 和響應(yīng)者 B 進行通信，協(xié)議運行過程如下：消息 A→I(B)： Eb(A,Ra)32 消息 I(A)→B： Eb(A,Ra)消息 B→I(A)： Ea(Ra,Rb,Ks)消息 I(B)→A： Ea(Ra,Rb,Ks) 消息 A→I(B)： Eb(Ks)消息 I(A)→B： Eb(Ks)在協(xié)議運行 1 中，A 以為他在和 B 進行通信，所以送出的消息 ，其中給出了自己的標識符 A 和質(zhì)詢隨機數(shù) Ra,并用 B 的公開密鑰進行加密。入侵者 I 無法冒充B 在消息 中給 A 給出正確的消息。在這時，入侵者 I 又冒充 A 與 B 開始一個新的會話，給出剛才在消息 中 A 給自己的消息用來質(zhì)詢 B，B 不知道是 I 在冒充 A和自己通信，以為和自己通信的是 A，于是他用 A 的公開密鑰加密消息 中給出的質(zhì)詢隨機數(shù),并給出自己的質(zhì)詢隨機數(shù) Rb 和自己建議的會話密鑰 Ks。I 在收到這個消息以后又回到剛才和 A 的會話中，用剛才 B 給自己的回答來冒充 B 回答 A。由于剛才 B 以為自己是和 A 通信，于是給出了正確的消息，結(jié)果被 I 利用來欺騙 A。A看到 B(實際上是 I 冒充)的正確回答，就以為自己是在和 B 通信，于是 I 欺騙了 A并和他建立的通信。由此可見，這種運行模式存在攻擊。（6） 運行模式 6運行模式 6 中，入侵者 I 冒充響應(yīng)者 B 與初始者 A 進行通信，這種情況的特殊性在于在整個過程中沒有響應(yīng)者 B 參與運行，協(xié)議運行過程如下：