1、 第十五章 安全協議的形式化分析技術 邏輯推理 形式化語言 形式化分析方法 形式化分析方法應用 邏輯推理 由前提推出結論。前提和結論都是命題。 命題的真或假由命題的內容是否符合客觀實際確定。 演繹邏輯 當前提的“真”蘊涵結論的“真”，稱前提和結論之間有可推導性關系。即前提和結論之間的推理是正確的。 研究怎樣的前提和結論之間具有可推導性關系。 歸納邏輯 只要求得到的結論本身是協調的，與前提是協調的。 前提的“真”并不蘊涵結論的“真”。 邏輯推理的正確性 命題的內容：“真”/“假”，內容決定命題的“真”/“假”。 命題的形式：即邏輯形式。由內容抽象出來。 邏輯形式決定前提和結論的之間的可推導性關系

2、。 不關心前提和結論的真假，而關注前提的真是否蘊涵結論的真。 形式語言 使用自然語言陳述并分析命題常常引出歧義。 需要構造一種符號語言形式語言，描述由命題內容抽象出來的命題邏輯形式。 形式語言使用符號來構造公式 由公式來精確地表示命題的邏輯形式 語義和語法 語義涉及符號和符號表達式的涵義(給符號某種解釋) 語法涉及符號表達式的形式結構，但不考慮任何對形式語言的解釋。 形式語言的語義和語法既有聯系，又有區分。 集合論 數理邏輯 圖論：有限狀態圖 網論：Petri網模型 代數系統：代數系統形式化模型 安全協議的基本概念安全協議特指使用密碼學技術的密碼協議所謂協議，就是兩個或者兩個以上的參與者為完成

3、某項特定的任務而采取的一系列步驟。 協議的定義包含三層含義：1. 協議自始至終是有序的過程，每一個步驟必須執行，在前一步沒有執行完之前，后面的步驟不可能執行；在參與者之間呈現為消息處理和消息交換交替進行的一系列步驟。2. 協議至少需要兩個參與者；一個人可以執行一系列的步驟來完成一項任務，但它不構成協議。3. 通過協議必須能夠完成某項任務。 安全協議使用密碼學技術，協議參與者可能是可以信任的人，也可能是攻擊者和完全不信任的人。密碼協議包含某種密碼算法。 網絡通信中常用的密碼協議按照其完成的功能分成以下四類： 密鑰交換協議 在參與協議的兩個或者多個實體之間建立共享的秘密通道，常用于建立在一次通信中

4、所使用的會話密鑰。協議可以采用對稱密碼體制，也可以采用非對稱密碼體制，例如Diffie-Hellman密鑰交換協議。認證協議 認證協議中包括實體認證（身份認證）協議、消息認證協議、數據源認證和數據目的認證協議等，用來防止假冒、篡改、否認等攻擊。認證和密鑰交換協議 協議將認證和密鑰交換協議結合在一起，是網絡通信中最普遍應用的安全協議。常見的有Needham-Schroeder協議、分布認證安全服務（DASS）協議、ITU-T X.509認證協議等等。電子商務協議 電子商務協議中，主體利益目標往往是不一致的，電子商務協議關注的就是公平性，即協議應保證交易雙方都不能通過損害對方利益而得到它不應得的利

5、益。常見的電子商務協議有SET協議等。Alice與ob確定兩個大素數n和g，這兩個整數不保密， Alice與ob 可以使用不安全信道確定這兩個數Alice選擇另一個大隨機數x，并計算A如下： A=gx mod nAlice將發給obob選擇另一個大隨機數y，并計算B如下： B=gy mod nob將發給Alice計算秘密密鑰K1如下： K1=Bx mod n計算秘密密鑰K2如下： K2=Ay mod n 介于應用層和傳輸層之間 為上層提供安全性IPSSL ChangeCipher SpecProtocolSSL AlertProtocolApplication ProtocolTCPSSL R

6、ecordProtocolSSL HandshakeProtocolHTTPLDAPIMAP 協議分為兩層 上層：TLS握手協議、TLS密碼變化協議、TLS警告協議 底層：TLS記錄協議 上層協議是用于管理SSL密鑰信息的交換，下層提供基本的安全服務 TLS握手協議 客戶和服務器之間相互認證 協商加密算法和密鑰 它提供連接安全性，有三個特點 身份認證，至少對一方實現認證，也可以是雙向認證 協商得到的共享密鑰是安全的，中間人不能夠知道 協商過程是可靠的 TLS記錄協議 建立在可靠的傳輸協議(如TCP)之上 它提供連接安全性，有兩個特點 保密性，使用了對稱加密算法 完整性，使用HMAC算法 用來封

7、裝高層的協議 信息在信息在InternetInternet上的安全傳輸，保證網上傳輸的上的安全傳輸，保證網上傳輸的數據不被黑客竊聽數據不被黑客竊聽 訂單信息和個人賬號信息的隔離，在將包括消費訂單信息和個人賬號信息的隔離，在將包括消費者賬號信息的訂單送到商家時，商家只能看到訂者賬號信息的訂單送到商家時，商家只能看到訂貨信息，而看不到消費者的賬戶信息貨信息，而看不到消費者的賬戶信息 消費者和商家的相互認證，以確定通信雙方的身消費者和商家的相互認證，以確定通信雙方的身份，一般由第三方機構負責為在線通信雙方提供份，一般由第三方機構負責為在線通信雙方提供信用擔保信用擔保 要求軟件遵循相同的協議和消息格式

8、，使不同廠要求軟件遵循相同的協議和消息格式，使不同廠家開發的軟件具有兼容和互操作功能，并且可以家開發的軟件具有兼容和互操作功能，并且可以運行在不同的硬件和操作系統平臺上運行在不同的硬件和操作系統平臺上Desktop computerCard HolderHow SET with Credit Card WorksServerMerchant ServerAcquiring BankCard Issuer Bank876543219CACertificate Authority00- cardholder registration132- purchase request- merchant p

9、asses signed, encrypted authorization to the acquirer for check- card validation with issuer4- issuer authorizes and signs transaction5- acquirer authorizes merchant and signs the transaction6- cardholder receives the goods and a receipt7- merchant deposit the transaction to his account8- merchant g

10、ets paid9- cardholder receives bill from card issuer 如果將安全協議所處環境視為一個系統，那么這個系統中，一般而言包括一些發送和接收消息的誠實的主體和一個攻擊者，以及用于管理消息發送和接收的規則。誠實主體誠實主體誠實主體誠實主體環境/攻擊者通信通信通信通信 評估一個安全協議是否安全就是檢查其所欲達到的安全性質是否遭到攻擊者的破壞。 認證性 聲稱者使用僅為其與驗證者知道的密鑰封裝的一個消息 聲稱者使用私鑰對消息簽名，驗證者使用公鑰來驗證 聲稱者通過可信第三方來證明自己。 秘密性 保護協議消息不被泄露給非授權擁有此消息的人，即使是攻擊者觀測到了消

11、息的格式，它也無法從中得到消息的內容或提煉出有用的信息。 保證協議消息秘密性的最直接的方法是對消息進行加密。 安全協議中，一般不考慮具體的密碼算法的執行細節，但在實際應用中這往往有可能造成協議秘密性的缺陷。 完整性保護協議消息不被非法篡改、刪除和替代。常用的方法有封裝和簽名SSL和IKE等協議中就涉及到保護協議消息完整性的具體實現細節 不可否認性目的是通過通信主體提供參與協議交換的證據來保證其合法利益不受侵害，即協議主體必須對自己的合法行為負責，而不能也無法事后否認。協議必須具有兩個特點：證據的正確性、交易的公平性。在不可否認性之中還可引申出其他一些相關性質，如適時中止性、公平性、可追究性等。

12、 安全協議的安全性 安全協議是許多分布式系統安全的基礎，確保這些協議的安全運行是極為重要的。 安全協議有若干幾個消息傳遞，消息之間存在著復雜的相互作用和制約； 協議中使用多種不同的密碼體制， 目前的許多安全協議存在安全缺陷。原因有兩個： 協議設計者誤解或者采用了不恰當的技術； 協議設計者對環境要求的安全需求研究不足。 對協議的安全性進行分析和研究是一個重要的課題。 S.Gritzalis和D.Spinellis根據安全缺陷產生的原因和相應的攻擊方法對安全缺陷進行了分類：基本協議缺陷： 協議設計中沒有或很少考慮防范攻擊者。口令/密鑰猜測缺陷： 弱口令導致攻擊者能夠進行口令猜測攻擊；或者弱密鑰使攻

13、擊者能夠破解該密鑰。 陳舊（stale）消息缺陷： 協議設計中對消息的新鮮性沒有充分考慮，從而使攻擊者能夠進行消息重放攻擊，包括消息源的攻擊、消息目的的攻擊等等。 并行會話缺陷 協議對并行會話攻擊缺乏防范，從而導致攻擊者通過交換適當的協議消息能夠獲得所需要的重要消息。 內部協議缺陷 協議可達性存在問題，協議的參與者中至少有一方不能夠完成所有必須的動作而導致缺陷。 密碼系統缺陷 協議中使用的密碼算法的安全強度導致協議不能完全滿足所要求的機密性、認證等需求而產生的缺陷。 安全協議的安全性是一個很難解決的問題，許多廣泛應用的安全協議后來都被發現存在安全缺陷。 從安全協議的分析和設計角度來看，應當對協

14、議的安全性作出認真的分析和驗證。 安全協議的分析方法攻擊檢驗方法；形式化的分析方法。 攻擊檢驗方法 搜集使用目前的對協議的有效攻擊方法，逐一對安全協議進行攻擊，檢驗安全協議是否具有抵抗這些攻擊的能力。 在分析的過程中主要使用自然語言和示意圖，對安全協議所交換的消息進行剖析。 這種分析方法對已知的攻擊非常有效的。 不能發現協議中未知的安全隱患。 形式化的分析方法 采用各種形式化的語言或者模型，為安全協議建立模型，并按照給定的假設和規則，分析、驗證方法證明協議的安全性。 近幾年來，密碼學家提出了許多關于安全協議的形式化分析方法，以檢驗協議中是否存在安全缺陷。 形式化的分析方法是目前研究的熱點，但是

15、就其實用性來說，還有待進一步突破。 安全協議的形式化分析有助于： 界定安全協議的邊界，即協議系統與其運行環境的界面 更準確地描述安全協議的行為。 更準確地定義安全協議的特性。 證明安全協議滿足其說明，以及證明安全協議在什么條件下不能滿足其說明。1）通用的形式化描述語言 使用通用的、不是為分析安全協議專門設計的形式化描述語言和協議校驗工具建立安全協議的模型并進行校驗。主要思想是將安全協議看作一般的協議，并試圖證明協議的正確性。 采用的工具和模型與驗證一般協議的類似，例如使用有限狀態圖、Petri網模型、LOTOS語言等等。 方法的主要缺點是僅證明協議的正確性而不是安全性。2）專家系統 設計專用的

16、專家系統來制定安全協議的校驗方案并進行協議檢驗，從而對協議的安全性作出結論。 主要思想是針對所設計的協議而開發專用的專家系統，通過專家系統發現協議是否能夠達到不合理的狀態（比如密鑰的泄露等等）。 這種技術能夠識別缺陷但是不能證明協議的安全性，也不能發現未知的缺陷。3）安全需求模型 基于知識和信任邏輯，針對具體協議建立相應的形式化安全需求模型 依據給定的邏輯初設和公理規則對該模型進行形式化分析推理 通過推理獲取的結果來推斷協議能否完成預期的目標、證明協議結論的正確性。 形式系統的組成（初始符號、形式規則、公理、變形規則） 這種方法是目前為止使用最廣泛的一種方法，最著名的是BAN邏輯。BAN邏輯是

17、基于知識和信任的形式邏輯模型，進行基于知識和信任的分析。BAN邏輯假設協議的安全是完整性和新鮮度的函數，使用邏輯規則來對協議的屬性進行跟蹤和分析。 通常，BAN邏輯只能推出給定初設的協議結果，對一般的安全性的證明依賴于給定攻擊模型的初設。 使用BAN邏輯分析安全協議的步驟如下：協議的理想化轉化；假設所有的協議初始狀態；使用邏輯規則對系統的狀態作出斷言；運用邏輯原理得到關于信任的斷言；4）代數系統形式化模型 基于密碼學系統的代數特性開發協議的形式化模型 將安全協議系統當作一個代數系統模型，表示出協議的參與者的各種狀態，然后分析某種狀態的可達性。 Michael Merritt已經證明了代數模型可

18、以用來分析安全協議。 美國海軍研究實驗室（Navy Research Lab.）開發的協議分析器是這種方法中最成功的一個應用，可以用來在各種協議中尋找新的和已知的缺陷。 安全協議分析的問題形式化分析方法在安全協議的應用是研究的熱點。目前應用并不廣泛的主要原因,是需要事先建立安全協議的安全性形式化模型。該過程比較復雜困難。目前并沒有一種方法能夠給出安全協議安全性的充分而且必要的理論證明。由于安全協議本身的復雜性，上述每一類方法都有不同的側重點，或多或少地存在不足之處。使用上述方法分析安全協議的時候，應當仔細分析協議的特點、應用環境和需求，綜合使用這些分析方法，以得到一個比較合理的結果。 由Bur

19、rows, Abadi & Needham提出，從而解決了SPA（Security Protocol Analysis)問題上邁出一大步。 它是關于主體信仰以及用于從已有信仰推出新的信仰的推理規則的邏輯。這種邏輯通過對認證協議的運行進行形式化分析，來研究認證雙方通過相互發送和接收消息能否從最初的信仰逐漸發展到協議運行最終要達到的目的認證雙方的最終信仰，其目的是在一個抽象層次上分析分布網絡系統中認證協議的安全問題。 如在協議執行結束時未能建立起關于諸如共享通信密鑰、對方身份等信任時，則表明這一協議有安全缺陷。 BAN邏輯包含believing、seeing、controlling和say

20、ing message語句，并以一種自然結構進行語義描述。 Burrows, Abadi & Needham定義一種基于信任的邏輯精確地表示這些信任找準、抓住導致信任的原因 BAN通過形式化的方法回答以下問題協議在工作嗎？協議能否使用？協議達到了預定的目標嗎？協議比別的協議需要更多的安全假設嗎？協議做了不必要的事嗎？ BAN邏輯形式化分析方法重點放在對協議涉及的通信各方的信任以及由這些信任的進一步推演所得到的通信結果上 不考慮由程序執行時所引入的錯誤如死鎖，甚至密碼系統的不正確使用問題 考慮到入侵的可能性，并不試圖去處理不信任的參與方的認證，也不檢測加密方案及未經授權的密碼體系。 BA

21、N邏輯形式推理過程1. 給出協議的消息序列描述；2. 對協議進行理想化轉換；【】3. 分析理想化的協議模型；4. 判斷結論。 BAN邏輯的符號、語法、語義、規則(1)BAN形式體系建立在多種類的模型邏輯上在BAN邏輯中區分幾種對象 主體(principals) 加密密鑰(encryption keys) 公式(formulas)，也稱為語句(statements)。 BAN邏輯的符號、語法、語義、規則(2)公式或語句的連接符(conjunction)用逗號表示【例如】(X,Y)表示X和Y的結合具有結合性和交換性BAN邏輯認為消息(message)和語句(statements)是一樣的。VR03

22、04-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabQPYXVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabXP XPXPXP )X(#VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabQPKPKQPXVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabKXYX)X(HVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab

23、 1.1P.XQPXP,QPPKK 1.2P.XQPXP,QP1KK 1.3P.XQPXP,QPPYY 要保證這個規則是合理的，我們則必須保證P自己沒有說過X；這就要將公式XK表示成XK from Q，并且要求Q不能是P 消息含義規則消息含義規則關心消息的解釋。其中三分之二關心加密消息的解釋。它們關心解釋如何得到消息源的信任 VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 1.4P.XQPY ,XQPVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 1.5P.XPXP,QPPKK 1.6P.XPXP,QP1K

24、K 1.7P.XPXP,PPKK 1.8P.XPY,XP 1.9P.XPXPYVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 2.1P.XQPXQP,X#P 2.2P.Y,X#PX#PVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 3.1P.XPXQP,XQP 3.2P.Y,XPYP,XP 3.3P.XPY,XP 3.4P.XQPY ,XQPVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 4.1P.XQPXP),X(HQPQ擁有消息XVR0304-DOC0-學習討

25、論：形式化分析方法 北京航空航天大學計算機學院 VR LabVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabbsKabK,A:BA VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabbsKabK,A:BA bsabKKBA:BABAabKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Labn1KnK1X,.,XVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院

26、VR LabTAAATKTBBBTKBATAABKBTBABKAAN#ABN#BBATABK 協議的初始必須是不變的，以保證每個協議的成功。 典型的，初始假設都是陳述兩個主體之間共享什么樣的密鑰，哪個主體產生新鮮的隨機值，哪個主體在某些特定的方式下是可信任的。 在大多數的情況下，初始假設是標準和明顯的。一旦所有的初始假設被寫出，驗證協議就等同于對作為結論的公式做出證明。 VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBAAABKBABABKBABAABKBAABABK 認證協議經常是建立某些用共享會話密鑰的基礎，所以，我們可得到認證協議的目標這樣的結

27、論描述。 因此，如果認為A和B之間有密鑰K，認證則是完成了A相信K是A與B之間的通信密鑰，B相信K是A與B之間的通信密鑰。 一些協議可能要求的比這更多 VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabVR0304-DOC0-學習討論：形式化分析方法VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBASA,:asbsKKabsabsAKLTBKLTAS, ,:abbsKaKabsTAAKLTBA, ,:abKaTAB1:SABMessage 1Message 2Message 3Message 4The Kerb

28、eros ProtocolVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabasbsababKKKsKsBATBATAS, ,:fromABATBATBAababbsabKKaKKs, ,:fromBBATABababKKa,:VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabSAAasKSBBbsKSASasKSBSbsKBASabKBASBKBASAK)(#sTB)(#sTA)(#aTBVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBAAabKBABabKBABAab

29、KBAABabKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabThe main steps of the proof are as follows: A receives Message 2. The annotation rules yield thatasbsababKKKsKsBATBATA,),( ,holds afterward. Since we have the hypothesisSAAasKthe message-meaning rule for shared keys applies and yields the followin

30、g:),),( ,(bsababKKsKsBATBATSAOne of our rules to break conjunctions (omitted here) then produces)( ,(BATSAabKsVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabMoreover, we have the following hypothesis(假設):)(#sTAThe nonce-verification rule applies and yields:),(BATSAabKsAgain, we break a conjunction, to

31、 obtain the following:BASAabKThen, we instantiate K to Kab in the hypothesis:BASAKderiving the more concrete:BASAabKFinally, the jurisdiction rule p3.1 applies, and yields the following:BAAabKThis concludes the analysis of Message 2.VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBABabKBAABabKVR0304-DO

32、C0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBAAabKBABabKBABAabKBAABabKBABAabKVR0304-DOC0-學習討論：形式化分析方法ABNc,A,B,Ka(Na,Nc,A,B)KDCM1M2M3M4M5Ka(Na,Nc,A,B)Kb(Nb,Nc,A,B)Nc,Ka(Na,Kab),Kb(Nb,Kab)Ka(Na,Kab)KabVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab1. ATKABAMNBAM,2. BTATKBKABAMNBAMNBAM,3. BTATKABBKABAKNKNM,4. AT

33、KABAKNM,VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab1. ATKABAMNBAM,ATKCANNB,2. BTATKBKABAMNBAMNBAM,),(BTATKCBKCANNNNT 3. BTATKABBKABAKNKNM,),(BTABATABKCKBKCKANABANNBBANB4. ATKABAKNM,ATABKCKANBBANA,VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabTAAATKTBBBTKTATATKBATAABKTBTBTKBATABKBATBABKXBTAXATBANA#B

34、NB#CNA#VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBABAABKBAABABKBAAABKBABABKCNBACNABVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBANTBTBBBANBABBTBTABKBKKKB,)(#)(#,BABNBBANBABBTABKBKKBBATBBABBATBABABABKKK)(#,BABBATBBATBABABABKKK,P3.1P1.1P2.1VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBAAABKCNBACNA

35、B因為缺少| #()cBNVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabCNABBAAABKCNBABABABKVR0304-DOC0-學習討論：形式化分析方法VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab4. ABKBN 1. ANBA,2. ATBTKKABABAKAKBN, ,3. BTKABKA,5. ABKB1NVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabM2.

36、ATBTABABABATBTKKKKKAKKABABABABABANAKAKBN),(#,M3. BTABBTKKKABBABKA,M4. BfromBANANABABABKKBKB,M5. fromABANBNABABABKKBKB,1 將消息寫成“收到”形式VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabTAAATKTBBBTKTATATKBATAABKTBTBTKBATABKBATBABK)(BATAABK#)(BATABK#ANA #BN#B )(BABABK#)(BATBABK#VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大

37、學計算機學院 VR LabBAAABKBABABKBABAABKBAABABK)(#BAAABK)(#BABABKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 1 .),(#),( ,(),(#),( ,(,CBABABANTABABABANATAABTABABABATBTABABABATKKKKAKKKKKAKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab2 .)(),(#),( ,(),(#CBATABABABANTANAABBTABABABKKKKKAAVR0304-DOC0-學習討論：形式化分析方

38、法 北京航空航天大學計算機學院 VR Lab4 .).(#3 .,)(#),(CBAACBAABATABATAABABABABKKKKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab5 .)()(),(CBATBTfromBABTBBABBTABBTKKKKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab6 .)()(),(#CBATBBATBBABABABABKKK)(BABABK#VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab7 .)(#),(),(CBABBAT

39、BBATBBATBABABABABKKKK)(BABABK)(BAAABKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab8 .)( ,()( ,(),(CBANBABfromBANABAAABABABABKBKKBKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab9 .)()( ,(),(#CBABABANBABAAABABABKKBK10.).(CBAABABKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab3 .CBAAABK7 .CBABABK9 .CBABAA

40、BK10.CBAABABK4 .).(#CBAAABK)(#BABABKVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab)(#BNB VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabBAAABKBATBABKBAABKATABKKABA,N)(BABABK#VR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR Lab 協議的理想化過于依賴分析時的直覺，協議的理想化使得在原始協議與理想化協議之間

41、存在一個潛在的語義鴻溝。 Ban邏輯分析的正確性嚴重依賴于前幾步，但前三步在有效達成目標上存在問題。即使對協議行為做出了準確的解釋，也不能保證能夠正確理解協議設計者的真正意圖，因而雖然對主體行為的理解不存在任何歧義，但仍可能存在對同一協議有兩種理想化的結果。 BAN不夠完備，即BAN邏輯不能查出協議的所有問題，只能證偽。 BAN邏輯系統沒有為協議理想化過程提供標準的轉換格式，這就使得對同一個協議由于分析者的不同理解而得到不同的理想化版本。 不合理的假設認為參與協議運行的主體都是誠實的。實際上許多合理協議并不滿足主體誠實性假設，且誠實概念也缺乏良好規范的定義初始狀態假設難以確定，而假設對分析結論

42、的正確得出至關重要。沒有形式化規則來確定假設，從而無法確認和自動驗證假設的正確性和有效性。 BAN邏輯為認證協議的設計提供了可參考的準則。認證主體用會話密鑰加密另一個認證主體所知的明文信息，來表示已獲得了會話密鑰。協議中會話密鑰的使用必須以新鮮性為保證，以防密鑰重放。認證協議中，在傳送包含關鍵的敏感信息的消息中，盡可能以顯式表現出參與協議的各個主體，使接收的主體能清晰地意識到其它主體的存在。在協議中可信服務器的信仰很重要，因此區分服務器作用的強弱是十分必要的。 1994年Syverson和Orschot提出了SVO邏輯，它的出現標志著BAN及BAN類邏輯的成熟。1996年，他們又在SVO邏輯的

43、公理，以及語義上有進行了更準確的定義。SVO邏輯吸收了BAN類邏輯系統的優點，同時又具有十分簡潔的推理規則和公理。它為邏輯系統建立了用于推證合理性的理論模型。在形式化語義方面，它具有極好的擴展能力。 定義T為初始術語集合，包括互不相交的常量符號集合：主體、共享密鑰、公鑰、私鑰以及序列號等。基于此，n維函數表示有n個變量的函數，如加、解密函數等。SVO邏輯將語言劃分為集合T上的消息語言MT和公式語言FT。消息語言MT 是滿足下列性質的最小語言集合：1.如果XT，則X是消息。2.如果X1，Xn是消息，F是任意一個n維函數，則F(X1，Xn)是消息。3.如果是公式，則是消息。 公式語言FT是滿足下列

44、性質的最小公式集合：1.如果P是原始命題，則P是公式。2.如果，是公式，則和是公式。3.P believes 和P controls 是公式，其中P是主體，是公式。4.P sees X，P says X，P said X，P received X和fresh(X)是公式，其中P是主體，X是消息。5. Shared(P，K，Q)，PK(P，K)，PK(P，K) ，PK(P，K)和P has K是公式，其中P是主體，K是密鑰。（其中PK(P，K)指公開密鑰，K是主體P的公鑰，而K1指相應的私鑰。PK(P，K)，PK(P，K) ，PK(P，K)分別表示用于加密，簽名和密鑰協商的公開密鑰。）SV(X,

45、 K, Y) 是公式，其中X，Y是消息，K是密鑰。（SV(X, K, Y)指簽名驗證，即X為簽名后得到消息，K為簽名驗證密鑰，Y為被簽名的消息。） P says X: X is a message P said recently. Like BAN P said X but must P must have said X since beginning of current epoch. P has X: X is a message P can see. Initially available to P Received by P Freshly generated by P Constru

46、ctible by P from the above PK(P,K): K is a public key of P. The matching secret key K-1 will never be discovered by any principal but P or a principal trusted by P. Original BAN notion is refined to cover different types of public key functionality. PKy(P,K): K is a public ciphering key of P. Only P

47、 can read messages encrypted with K. PKs(P,K): K is a public signature key of P. K verifies messages signed by K-1 are from P. PKd(P,K): K is a public key-agreement key of P. A Diffie-Hellman key formed with K is shared with P. XK: X signed with key K. Notationally distinguish: Encrypted messages fr

48、om signed messages. XK: Not short for XK from P . No longer assume: Principals can recognize own messages. Still assume: Encryption messages are uniquely readable and verifiable as such by holders of the right keys. X *p: X according to P. Used for messages that P doesnt know/recognize Example: XK w

49、here P does not know K P will recognize XK *p as the same thing if received again.SVO邏輯遵從兩條基本推理規則：Modus Ponens (MP)：( )Necessitation (Nec)： P believes SVO邏輯共有20條公理：對于任一主體P和公式，有：Ax1：P believes P believes ( ) P believes Ax2：P believes P believes (P believes )公理Ax1表示主體相信由其已有的信任關系邏輯推導出的所有信仰結果。公理Ax2表示主體表

50、明其信任的是什么。密鑰用于推斷消息發送者的身份。Ax3：shared(P，K，Q)R received XQk Q said X Q sees X Ax4：(PK(Q，K)R received X SV(X, K,Y) Q said X 公理Ax3中上標Q暗示消息是Q產生并發送的，而不是P。 公理Ax4中PK(Q，K)表示K是主體Q的數字簽名驗證密鑰。此公理表明如果主體R收到一個簽名消息，并且R知道簽名的驗證公鑰是K，它就可以確認消息發方的身份。會話密鑰是由密鑰協商密鑰是良好的得到的。Ax5：(PK(P，Kp)PK(Q，Kq) shared(P，Kp,q，Q)Ax6： F0(K,K) / F0

51、(K,K)公理Ax5中KpqF0(Kp，Kq1 )F0(Kp-1,Kq)，F0指密鑰協商函數，如Diffie-Hellman密鑰交換。F0(K, K ) implicitly names the (Diffie-Hellman) function that combines K with K-1 to form a shared key.公理Ax6中PK(R，KR)表示KR是R用于密鑰協商的公開密鑰，而KR-1是R保存的秘密密鑰。該公理表示兩個公式邏輯上是相等的。也就是說，邏輯注意到密鑰協商的對稱性。主體對接收到的一個級聯的加密消息并用有效的密鑰解密。Ax 7：P received (X1，X

52、n) P received XiAx 8：P receivedXk P sees K1 P received XAx 9：P received Xk P received X其中Xk 表示標準的加密模式，Xk 表示被簽名的消息。AX9中，Principals are assumed to possess public keys (for convenience) 主體只要接收到一個消息就看到了這個消息，并且看到了這個消息的每一部分。主體還可以看到從已看到的消息計算得到的消息。Ax10：P received X P sees XAx11：P sees (X1，Xn) P sees XiAx12：

53、P sees X1 P sees Xn P sees (F (X1，Xn) 如果一個主體理解一個消息，并看到此消息的一個函數，那么它理解它所看到的。Ax13：P believes (P sees F(X) P believes (P sees X)F可視為加解密函數，K為參數。一個主體說過一個級聯消息，那么它一定說過且看到消息的每一部分。Ax14：P said (X1，Xn) P said Xi P sees XiAx15：P says (X1，Xn) P said (X1，Xn) P says XiAx16：P controls P says 如果消息的一部分是新鮮，那么整個消息也是新鮮的。

54、有關新鮮消息的任何一對一函數（如加密解密函數）也是新鮮的。Ax17：fresh(Xi) fresh(X1，Xn)Ax18：fresh(X1，Xn) fresh(F(X1，Xn)F must genuinely depend on all components F genuinely depends on the value of X infeasible to compute value of F withoutvalue of X 隨機數-驗證公理 (Nonce-Verification)新鮮性促使已經被說的消息為當前時間點所說的消息。Ax19：fresh (X)P said X P say

55、s X( Symmetric goodness of shared keys)如果K是P、Q之間的良好密鑰當且僅當K是Q、P之間的良好密鑰。Ax20：shared(P，K，Q)shared(Q，K，P) P has K P sees KVR0304-DOC0-學習討論：形式化分析方法 北京航空航天大學計算機學院 VR LabSVO邏輯的協議句法分析技術與BAN邏輯的分析技術同屬于推理結構的分析方法。但SVO邏輯不需要BAN邏輯的協議理想化過程，而重點具體化了協議前提的確定過程。SVO邏輯對協議的形式化分析分為以下三步： 給出協議所基于的前提。 形式化說明協議將達成的安全目標。1. 運用公理和推

56、理規則及其前提，從協議的前提進行推證直至驗證協議是否滿足其最終運行目標。 第一類前提是初始假設，即在協議的初始狀態時就為真的假設。例如每個主體對其產生的隨機數的新鮮性的信任；主體對其與服務器共享的長期密鑰的良好性的信任；主體關于服務器對它發送的密鑰的質量和新鮮性具有權威的信任等。 如：消息SA：Ts, B, Ka,bKa,s第一類前提有：A believe fresh(Ts)；A believe S controls share(A, Ka,b ,B) ；A believe share(A, Ka,s, S) 第二類前提反映主體對在協議運行期間發送的消息的接收，可以直接從協議描述得到。在證明過

57、程中經常不使用這類前提，但它們有助于形成后邊的前提。 如：上例為 A received Ts, B, Ka,bKa,s 第三類前提反映每個主體對其收到消息的理解。主體不可能完全理解其所收到的消息的每一部分。如由于分發（distributed）密鑰具有隨機性，故收到它的主體（而不是產生它的主體）必然不能理解它（unrecognizable）。通過考慮主體對其在第二類前提中的接收到子消息的理解，很容易得到這一類前提。如：上例為 A believes A received Ts, B, *s Ka,s 第四類前提反映接收主體對收到消息加入的解釋。這是BAN邏輯中理想化步驟的主要替代部分（primar

58、y replacement）。這類前提還與具體協議的特征有關。如: 上例為 A believes （A received Ts, B, *s Ka,s A received Ts, B, share(A, Ka,b ,B),fresh(Ka,b) Ka,s） 不可否認協議的實現包括證據的生成、證據的交換、證據的驗證以及糾紛的解決，方法一般有兩種：一是雙方進行同時（或接近同時）的秘密交換;另一種借鑒可信第三方（TTP）。經常采用TTP方式。 兩個基本證據：NRO（Non-repudiation of Origin)發方不可否認。用于證明發方的確發送了消息，由發方提供。NRR（Non-repudi

59、ation of Receipt)收方不可否認。用于證明收方的確收到了消息，由收方提供。 如有TTP介入，則還需要下面兩個證據：NRS（Non-repudiation of Submission)提交不可否認。用于證明已提交給了TTP，由提交方提供。NRD（Non-repudiation of Delivery)傳遞不可否認。證明TTP已交給了意定的接收者，由TTP提供。Zhou和Gollmann在文獻5提出了一個不可否認協議（ZG協議），具體描述為：M1 AB： fNRO,B,L,C,NROM2 BA: fNRR,A,L,C,NRRM3 ATTP: fNRS,B,L,K,NRS_KM4 BT

60、TP: fNRD,A,B,L,K,NRD_KM5 ATTP: fNRD,A,B,L,K,NRD_KA:不可否認協議交換的發起者。B：不可否認協議交換的接收者。TTP：可提供網絡服務的在線可信第三方。M：A發送給B的消息。C：A發送給B的密文。K：A定義的消息密鑰。L：協議輪標志SI：表示主體I的簽名私鑰。fNRO,fNRR,fNRS及fNRD:用于標識生成特定消息的協議步驟的標志，為方便起見記為f1,f2,f3,f4.: ftp操作符。NROSA(fNRO,B,L,C)NRR=SB(fNRR,A,L,C)NRS_K=SA(fNRS,B,L,K)NRD_K=STTP(fNRO,A,B,L,K)消息M的傳輸分兩步