第十五章安全協(xié)議形式化分析

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

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

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

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

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

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

7、裝高層的協(xié)議 信息在信息在InternetInternet上的安全傳輸，保證網(wǎng)上傳輸?shù)纳系陌踩珎鬏?，保證網(wǎng)上傳輸?shù)臄?shù)據(jù)不被黑客竊聽數(shù)據(jù)不被黑客竊聽 訂單信息和個人賬號信息的隔離，在將包括消費(fèi)訂單信息和個人賬號信息的隔離，在將包括消費(fèi)者賬號信息的訂單送到商家時，商家只能看到訂者賬號信息的訂單送到商家時，商家只能看到訂貨信息，而看不到消費(fèi)者的賬戶信息貨信息，而看不到消費(fèi)者的賬戶信息 消費(fèi)者和商家的相互認(rèn)證，以確定通信雙方的身消費(fèi)者和商家的相互認(rèn)證，以確定通信雙方的身份，一般由第三方機(jī)構(gòu)負(fù)責(zé)為在線通信雙方提供份，一般由第三方機(jī)構(gòu)負(fù)責(zé)為在線通信雙方提供信用擔(dān)保信用擔(dān)保 要求軟件遵循相同的協(xié)議和消息格式

8、，使不同廠要求軟件遵循相同的協(xié)議和消息格式，使不同廠家開發(fā)的軟件具有兼容和互操作功能，并且可以家開發(fā)的軟件具有兼容和互操作功能，并且可以運(yùn)行在不同的硬件和操作系統(tǒng)平臺上運(yùn)行在不同的硬件和操作系統(tǒng)平臺上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 如果將安全協(xié)議所處環(huán)境視為一個系統(tǒng)，那么這個系統(tǒng)中，一般而言包括一些發(fā)送和接收消息的誠實(shí)的主體和一個攻擊者，以及用于管理消息發(fā)送和接收的規(guī)則。誠實(shí)主體誠實(shí)主體誠實(shí)主體誠實(shí)主體環(huán)境/攻擊者通信通信通信通信 評估一個安全協(xié)議是否安全就是檢查其所欲達(dá)到的安全性質(zhì)是否遭到攻擊者的破壞。 認(rèn)證性 聲稱者使用僅為其與驗(yàn)證者知道的密鑰封裝的一個消息 聲稱者使用私鑰對消息簽名，驗(yàn)證者使用公鑰來驗(yàn)證 聲稱者通過可信第三方來證明自己。 秘密性 保護(hù)協(xié)議消息不被泄露給非授權(quán)擁有此消息的人，即使是攻擊者觀測到了消

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

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

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

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

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

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

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

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

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

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

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

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

23、 1.1P.XQPXP,QPPKK 1.2P.XQPXP,QP1KK 1.3P.XQPXP,QPPYYVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 1.4P.XQPY ,XQPVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 1.5P.XPXP,QPPKK 1.6P.XPXP,QP1KK 1.7P.XPXP,PPKK 1.8P.XPY,XP 1.9P.XPXPYVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 2.1P.XQPXQP,X#P 2.2P.Y,X#PX#

24、PVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 3.1P.XPXQP,XQP 3.2P.Y,XPYP,XP 3.3P.XPY,XP 3.4P.XQPY ,XQPVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 4.1P.XQPXP),X(HQPQ擁有消息XVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院

25、 VR LabbsKabK,A:BA VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabbsKabK,A:BA bsabKKBA:BABAabKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Labn1KnK1X,.,XVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabTAAATKTBBBTKBATAABKBTBABKAAN#ABN#BBATABKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBAAABKBABABKBABAABKBAA

26、BABKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBASA,:asbsKKabsabsAKLTBKLTAS, ,:abbsKaKabsTAAKLTBA, ,:abKaTAB1:VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabasbsababKKKsKsBATBATAS, ,:fromABATBATBAababbsabKKaKKs, ,:fromBBATABababKKa

27、,:VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabSAAasKSBBbsKSASasKSBSbsKBASabKBASBKBASAK)(#sTB)(#sTA)(#aTBVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBAAabKBABabKBABAabKBAABabKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabasbsababKKKsKsBATBATA,),( ,SAAasK),),( ,(bsababKKsKsBATBATSA)( ,(BATSAabKsVR030

28、4-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab)(#sTA),(BATSAabKsBASAabKBASAKBASAabKBAAabKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBABabKBAABabKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBAAabKBABabKBABAabKBAABabKBABAabKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法ABNc,A,B,Ka(Na,Nc,A,B)KDCM1M2M3M4M5Ka(Na,Nc,A,B)Kb(Nb,Nc,

29、A,B)Nc,Ka(Na,Kab),Kb(Nb,Kab)Ka(Na,Kab)KabVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabATKABAMNBAM,BTATKBKABAMNBAMNBAM,BTATKABBKABAKNKNM,ATKABAKNM,VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabATKABAMNBAM,ATKCANNB,BTATKBKABAMNBAMNBAM,),(BTATKCBKCANNNNT BTATKABBKABAKNKNM,),(BTABATABKCKBKCKANABANNBBANBA

30、TKABAKNM,ATABKCKANBBANA,VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabTAAATKTBBBTKTATATKBATAABKTBTBTKBATABKBATBABKXBTAXATBANA#BNB#CNA#VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBABAABKBAABABKBAAABKBABABKCNBACNABVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBANTBTBBBANBABBTBTABKBKKKB,)(#)(#,BABNBBANB

31、ABBTABKBKKBBATBBABBATBABABABKKK)(#,BABBATBBATBABABABKKK,VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBAAABKCNBACNAB| #()cBNVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabCNABBAAABKCNBABABABKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR L

32、abABKBN ANBA,ATBTKKABABAKAKBN, ,BTKABKA,ABKB1NVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabATBTABABABATBTKKKKKAKKABABABABABANAKAKBN),(#,BTABBTKKKABBABKA,BfromBANANABABABKKBKB,fromABANBNABABABKKBKB,1VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabTAAATKTBBBTKTATATKBATAABKTBTBTKBATABKBATBABK)(BATAABK#)(B

33、ATABK#ANA #BN#B )(BABABK#)(BATBABK#VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBAAABKBABABKBABAABKBAABABK)(#BAAABK)(#BABABKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 1 .),(#),( ,(),(#),( ,(,CBABABANTABABABANATAABTABABABATBTABABABATKKKKAKKKKKAKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab2 .)(),(

34、#),( ,(),(#CBATABABABANTANAABBTABABABKKKKKAAVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab4 .).(#3 .,)(#),(CBAACBAABATABATAABABABABKKKKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab5 .)()(),(CBATBTfromBABTBBABBTABBTKKKKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab6 .)()(),(#CBATBBATBBABABABABKKK)(BABA

35、BK#VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab7 .)(#),(),(CBABBATBBATBBATBABABABABKKKK)(BABABK)(BAAABKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab8 .)( ,()( ,(),(CBANBABfromBANABAAABABABABKBKKBKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab9 .)()( ,(),(#CBABABANBABAAABABABKKBK10.).(CBAABABKVR0304-

36、DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab3 .CBAAABK7 .CBABABK9 .CBABAABK10.CBAABABK4 .).(#CBAAABK)(#BABABKVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab)(#BNB VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabBAAABKBATBABKBAABKATABKKABA,N)(BABABK#VR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabVR0304-DOC0-學(xué)習(xí)討論：

37、形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR Lab 協(xié)議的理想化過于依賴分析時的直覺，協(xié)議的理想化使得在原始協(xié)議與理想化協(xié)議之間存在一個潛在的語義鴻溝。 Ban邏輯分析的正確性嚴(yán)重依賴于前幾步，但前三步在有效達(dá)成目標(biāo)上存在問題。即使對協(xié)議行為做出了準(zhǔn)確的解釋，也不能保證能夠正確理解協(xié)議設(shè)計者的真正意圖，因而雖然對主體行為的理解不存在任何歧義，但仍可能存在對同一協(xié)議有兩種理想化的結(jié)果。 BAN不夠完備，即BAN邏輯不能查出協(xié)議的所有問題，只能證偽。 BAN邏輯系統(tǒng)沒有為協(xié)議理想化過程提供標(biāo)準(zhǔn)的轉(zhuǎn)換格式，這就使得對同一個協(xié)議由于分析者的不同理解而得到不同的理想化版本。 不合理的假設(shè)認(rèn)為參與協(xié)

38、議運(yùn)行的主體都是誠實(shí)的。實(shí)際上許多合理協(xié)議并不滿足主體誠實(shí)性假設(shè)，且誠實(shí)概念也缺乏良好規(guī)范的定義初始狀態(tài)假設(shè)難以確定，而假設(shè)對分析結(jié)論的正確得出至關(guān)重要。沒有形式化規(guī)則來確定假設(shè)，從而無法確認(rèn)和自動驗(yàn)證假設(shè)的正確性和有效性。 BAN邏輯為認(rèn)證協(xié)議的設(shè)計提供了可參考的準(zhǔn)則。認(rèn)證主體用會話密鑰加密另一個認(rèn)證主體所知的明文信息，來表示已獲得了會話密鑰。協(xié)議中會話密鑰的使用必須以新鮮性為保證，以防密鑰重放。認(rèn)證協(xié)議中，在傳送包含關(guān)鍵的敏感信息的消息中，盡可能以顯式表現(xiàn)出參與協(xié)議的各個主體，使接收的主體能清晰地意識到其它主體的存在。在協(xié)議中可信服務(wù)器的信仰很重要，因此區(qū)分服務(wù)器作用的強(qiáng)弱是十分必要的。

39、1994年Syverson和Orschot提出了SVO邏輯，它的出現(xiàn)標(biāo)志著BAN及BAN類邏輯的成熟。1996年，他們又在SVO邏輯的公理，以及語義上有進(jìn)行了更準(zhǔn)確的定義。SVO邏輯吸收了BAN類邏輯系統(tǒng)的優(yōu)點(diǎn)，同時又具有十分簡潔的推理規(guī)則和公理。它為邏輯系統(tǒng)建立了用于推證合理性的理論模型。在形式化語義方面，它具有極好的擴(kuò)展能力。 定義T為初始術(shù)語集合，包括互不相交的常量符號集合：主體、共享密鑰、公鑰、私鑰以及序列號等?；诖?，n維函數(shù)表示有n個變量的函數(shù)，如加、解密函數(shù)等。SVO邏輯將語言劃分為集合T上的消息語言MT和公式語言FT。消息語言MT 是滿足下列性質(zhì)的最小語言集合：1.如果XT，則

40、X是消息。2.如果X1，Xn是消息，F(xiàn)是任意一個n維函數(shù)，則F(X1，Xn)是消息。3.如果是公式，則是消息。 公式語言FT是滿足下列性質(zhì)的最小公式集合：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是主體

41、P的公鑰，而K1指相應(yīng)的私鑰。PK(P，K)，PK(P，K) ，PK(P，K)分別表示用于加密，簽名和密鑰協(xié)商的公開密鑰。）SV(X, K, Y) 是公式，其中X，Y是消息，K是密鑰。（SV(X, K, Y)指簽名驗(yàn)證，即X為簽名后得到消息，K為簽名驗(yàn)證密鑰，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. In

42、itially available to P Received by P Freshly generated by P Constructible 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 ke

43、y functionality. PKy(P,K): K is a public ciphering key of P. Only P 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

44、 signed with key K. Notationally distinguish: Encrypted messages from 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

45、 to P. Used for messages that P doesnt know/recognize Example: XK where P does not know K P will recognize XK *p as the same thing if received again.SVO邏輯遵從兩條基本推理規(guī)則：Modus Ponens (MP)：( )Necessitation (Nec)： P believes SVO邏輯共有20條公理：對于任一主體P和公式，有：Ax1：P believes P believes ( ) P believes Ax2：P believes

46、P believes (P believes )公理Ax1表示主體相信由其已有的信任關(guān)系邏輯推導(dǎo)出的所有信仰結(jié)果。公理Ax2表示主體表明其信任的是什么。密鑰用于推斷消息發(fā)送者的身份。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中上標(biāo)Q暗示消息是Q產(chǎn)生并發(fā)送的，而不是P。 公理Ax4中PK(Q，K)表示K是主體Q的數(shù)字簽名驗(yàn)證密鑰。此公理表明如果主體R收到一個簽名消息，并且R知道簽名的驗(yàn)證公鑰是K，它就可以確認(rèn)消息發(fā)方的身份。會話密鑰是由密鑰

47、協(xié)商密鑰是良好的得到的。Ax5：(PK(P，Kp)PK(Q，Kq) shared(P，Kp,q，Q)Ax6： F0(K,K) / F0(K,K)公理Ax5中KpqF0(Kp，Kq1 )F0(Kp-1,Kq)，F(xiàn)0指密鑰協(xié)商函數(shù)，如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用于密鑰協(xié)商的公開密鑰，而KR-1是R保存的秘密密鑰。該公理表示兩個公式邏輯上是相等的

48、。也就是說，邏輯注意到密鑰協(xié)商的對稱性。主體對接收到的一個級聯(lián)的加密消息并用有效的密鑰解密。Ax 7：P received (X1，Xn) P received XiAx 8：P receivedXk P sees K1 P received XAx 9：P received Xk P received X其中Xk 表示標(biāo)準(zhǔn)的加密模式，Xk 表示被簽名的消息。AX9中，Principals are assumed to possess public keys (for convenience) 主體只要接收到一個消息就看到了這個消息，并且看到了這個消息的每一部分。主體還可以看到從已看到的消息計

49、算得到的消息。Ax10：P received X P sees XAx11：P sees (X1，Xn) P sees XiAx12：P sees X1 P sees Xn P sees (F (X1，Xn) 如果一個主體理解一個消息，并看到此消息的一個函數(shù)，那么它理解它所看到的。Ax13：P believes (P sees F(X) P believes (P sees X)F可視為加解密函數(shù)，K為參數(shù)。一個主體說過一個級聯(lián)消息，那么它一定說過且看到消息的每一部分。Ax14：P said (X1，Xn) P said Xi P sees XiAx15：P says (X1，Xn) P sa

50、id (X1，Xn) P says XiAx16：P controls P says 如果消息的一部分是新鮮，那么整個消息也是新鮮的。有關(guān)新鮮消息的任何一對一函數(shù)（如加密解密函數(shù)）也是新鮮的。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 隨機(jī)數(shù)-驗(yàn)證公理 (Nonc

51、e-Verification)新鮮性促使已經(jīng)被說的消息為當(dāng)前時間點(diǎn)所說的消息。Ax19：fresh (X)P said X P says X( Symmetric goodness of shared keys)如果K是P、Q之間的良好密鑰當(dāng)且僅當(dāng)K是Q、P之間的良好密鑰。Ax20：shared(P，K，Q)shared(Q，K，P) P has K P sees KVR0304-DOC0-學(xué)習(xí)討論：形式化分析方法 北京航空航天大學(xué)計算機(jī)學(xué)院 VR LabSVO邏輯的協(xié)議句法分析技術(shù)與BAN邏輯的分析技術(shù)同屬于推理結(jié)構(gòu)的分析方法。但SVO邏輯不需要BAN邏輯的協(xié)議理想化過程，而重點(diǎn)具體化了協(xié)議

52、前提的確定過程。SVO邏輯對協(xié)議的形式化分析分為以下三步： 給出協(xié)議所基于的前提。 形式化說明協(xié)議將達(dá)成的安全目標(biāo)。1. 運(yùn)用公理和推理規(guī)則及其前提，從協(xié)議的前提進(jìn)行推證直至驗(yàn)證協(xié)議是否滿足其最終運(yùn)行目標(biāo)。 第一類前提是初始假設(shè)，即在協(xié)議的初始狀態(tài)時就為真的假設(shè)。例如每個主體對其產(chǎn)生的隨機(jī)數(shù)的新鮮性的信任；主體對其與服務(wù)器共享的長期密鑰的良好性的信任；主體關(guān)于服務(wù)器對它發(fā)送的密鑰的質(zhì)量和新鮮性具有權(quán)威的信任等。 如：消息SA：Ts, B, Ka,bKa,s第一類前提有：A believe fresh(Ts)；A believe S controls share(A, Ka,b ,B) ；A b

53、elieve share(A, Ka,s, S) 第二類前提反映主體對在協(xié)議運(yùn)行期間發(fā)送的消息的接收，可以直接從協(xié)議描述得到。在證明過程中經(jīng)常不使用這類前提，但它們有助于形成后邊的前提。 如：上例為 A received Ts, B, Ka,bKa,s 第三類前提反映每個主體對其收到消息的理解。主體不可能完全理解其所收到的消息的每一部分。如由于分發(fā)（distributed）密鑰具有隨機(jī)性，故收到它的主體（而不是產(chǎn)生它的主體）必然不能理解它（unrecognizable）。通過考慮主體對其在第二類前提中的接收到子消息的理解，很容易得到這一類前提。如：上例為 A believes A receiv

54、ed Ts, B, *s Ka,s 第四類前提反映接收主體對收到消息加入的解釋。這是BAN邏輯中理想化步驟的主要替代部分（primary replacement）。這類前提還與具體協(xié)議的特征有關(guān)。如: 上例為 A believes （A received Ts, B, *s Ka,s A received Ts, B, share(A, Ka,b ,B),fresh(Ka,b) Ka,s） 不可否認(rèn)協(xié)議的實(shí)現(xiàn)包括證據(jù)的生成、證據(jù)的交換、證據(jù)的驗(yàn)證以及糾紛的解決，方法一般有兩種：一是雙方進(jìn)行同時（或接近同時）的秘密交換;另一種借鑒可信第三方（TTP）。經(jīng)常采用TTP方式。 兩個基本證據(jù)：NRO（

55、Non-repudiation of Origin)發(fā)方不可否認(rèn)。用于證明發(fā)方的確發(fā)送了消息，由發(fā)方提供。NRR（Non-repudiation of Receipt)收方不可否認(rèn)。用于證明收方的確收到了消息，由收方提供。 如有TTP介入，則還需要下面兩個證據(jù)：NRS（Non-repudiation of Submission)提交不可否認(rèn)。用于證明已提交給了TTP，由提交方提供。NRD（Non-repudiation of Delivery)傳遞不可否認(rèn)。證明TTP已交給了意定的接收者，由TTP提供。Zhou和Gollmann在文獻(xiàn)5提出了一個不可否認(rèn)協(xié)議（ZG協(xié)議），具體描述為：M1 AB

56、： fNRO,B,L,C,NROM2 BA: fNRR,A,L,C,NRRM3 ATTP: fNRS,B,L,K,NRS_KM4 BTTP: fNRD,A,B,L,K,NRD_KM5 ATTP: fNRD,A,B,L,K,NRD_KA:不可否認(rèn)協(xié)議交換的發(fā)起者。B：不可否認(rèn)協(xié)議交換的接收者。TTP：可提供網(wǎng)絡(luò)服務(wù)的在線可信第三方。M：A發(fā)送給B的消息。C：A發(fā)送給B的密文。K：A定義的消息密鑰。L：協(xié)議輪標(biāo)志SI：表示主體I的簽名私鑰。fNRO,fNRR,fNRS及fNRD:用于標(biāo)識生成特定消息的協(xié)議步驟的標(biāo)志，為方便起見記為f1,f2,f3,f4.: ftp操作符。NROSA(fNRO,B,

57、L,C)NRR=SB(fNRR,A,L,C)NRS_K=SA(fNRS,B,L,K)NRD_K=STTP(fNRO,A,B,L,K)消息M的傳輸分兩步：首先由A將消息的密文傳給B，在A收到B對此消息的回執(zhí)后通過可信第三方將K發(fā)給B。協(xié)議的運(yùn)行過程為：在M1中，A將CK（M）、輪標(biāo)志L、意定接收者的標(biāo)識以及NRO發(fā)送給B，B將之作為用于證明A在L輪協(xié)議發(fā)送C的證據(jù)。B返回一個簽名消息NRR用于證明在L輪中收到C。這為A提供了C已被B收到的證據(jù)。A將K以及一個提交不可否認(rèn)證據(jù)NRS_K發(fā)送給TTP1.在M4和M5中，A和B通過ftp操作從TTP處得到一個已先期存放的密鑰K以及由TTP簽發(fā)的傳遞不可

58、否認(rèn)證據(jù)NRD_K. 如果A希望證明消息已被對方接收，它可向仲裁出示證據(jù)：SB(f2,A,L,C)和STTP(f4,A,B,L,K)。前者證明B收到了C，后者證明K已在TTP中，因此意味著B能夠得到K并進(jìn)而得到M。如果B希望證明消息已被發(fā)送，它可向仲裁出示證據(jù)：SA（f1,B,L,C)和STTP（f4,A,B,L,K)。前者表明C已被A發(fā)送，后者證明K也已被發(fā)送給了TTP。L表明C和K是在同一輪協(xié)議中的。協(xié)議公平性：從協(xié)議執(zhí)行的開始到協(xié)議執(zhí)行結(jié)束的任何一個階段，通信的雙方要么能夠同時得到它們所期望的，要么任何一方都得不到有利于自己的信息，從而避免協(xié)議的任一方中斷執(zhí)行的協(xié)議，或否認(rèn)其已發(fā)生的行為

59、以達(dá)到利益不平等的可能。一個協(xié)議的不可否認(rèn)性成立，如果：協(xié)議任何一步執(zhí)行后的中止將不會破壞通信雙方主體的地位的公平性。1.在協(xié)議結(jié)束時提供主體參與協(xié)議行為的有效證據(jù)，即證據(jù)的有效性。證明ZG協(xié)議的不可否認(rèn)性。1.給出協(xié)議前提與假設(shè) A0基本假設(shè)：協(xié)議的運(yùn)行環(huán)境是不安全的。 A1:每個主體的公鑰是公開的。 A2:每個主體的私鑰僅為其所知。 A3:TTP believes SA A4: TTP believes SB A5: P believes STTP (P為參與協(xié)議運(yùn)行的主體） A6:TTP believes (B received C) TTP believes(A said C) A7:

60、 A said (A,B,L,Ek(M) A said(A,B,L,K) A said M A8: B received (A,B,L,Ek(M) B received(A,B,L,K) B received M A9:TTP believes (A said C B received C TTP received K) TTP says K A9表示TTP只有在確信A已說過C，并且B收到了C，以及TTP收到了K，才將K公布到其公開目錄中 A10: TTP says X P ftp X P sees XTTP將其認(rèn)為是有效的數(shù)據(jù)放入其公共目錄下，并可為任何主體通過ftp操作訪問。A11：P believes