《通信網(wǎng)安全理論與技術(shù)》課程《安全協(xié)議形式化分析與設(shè)計(jì)》

1、通信網(wǎng)安全理論與技術(shù)課程安全協(xié)議形式化分析與設(shè)計(jì)實(shí)踐性通信安全保障協(xié)議安全設(shè)計(jì)理論和技術(shù)基礎(chǔ)前導(dǎo)性8. 課程體系及主要內(nèi)容講解內(nèi)容通信網(wǎng)安全現(xiàn)狀、趨勢(shì)與策略第1講通信網(wǎng)技術(shù)基礎(chǔ)與安全體系第2講通信網(wǎng)安全基礎(chǔ)理論與技術(shù)(密碼學(xué)、攻擊與防御技術(shù))第3講網(wǎng)絡(luò)安全協(xié)議理論設(shè)計(jì)與分析認(rèn)證協(xié)議以及密鑰建立協(xié)議第4講數(shù)字簽名與閾下信道設(shè)計(jì)第5講零知識(shí)證明及其安全協(xié)議構(gòu)造第6講安全協(xié)議形式化分析與設(shè)計(jì)第7講典型的網(wǎng)絡(luò)安全協(xié)議(IPSec協(xié)議、Kerberos協(xié)議、 Radius/AAA協(xié)議) 第810講通信網(wǎng)安全保障技術(shù)第11講無(wú)線網(wǎng)絡(luò)安全性增強(qiáng)技術(shù)(WLAN為主)第12講網(wǎng)絡(luò)防火墻與入侵防御技術(shù)第13講網(wǎng)絡(luò)

2、安全實(shí)現(xiàn)方案設(shè)計(jì)與分析第14講內(nèi)容提要安全協(xié)議存在安全缺陷安全協(xié)議形式化分析類BAN邏輯形式化分析例子：對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析安全協(xié)議存在安全缺陷原因目前安全協(xié)議因如下原因，都存在一些安全缺陷：對(duì)于其目的、需求和概念沒(méi)有明確認(rèn)識(shí)和準(zhǔn)確描述運(yùn)行環(huán)境復(fù)雜，攻擊者無(wú)處不在，其攻擊能力強(qiáng)、手段多協(xié)議設(shè)計(jì)者誤解或者采用了不恰當(dāng)?shù)募夹g(shù)很多安全缺陷并不顯而易見(jiàn)，必須采用一定的分析手段才能發(fā)現(xiàn)和彌補(bǔ)安全協(xié)議存在安全缺陷常見(jiàn)缺陷根據(jù)其產(chǎn)生的原因和相應(yīng)的攻擊方法，安全缺陷主要有：基本協(xié)議缺陷：指在設(shè)計(jì)中沒(méi)有或者很少防范攻擊者的攻擊而引發(fā)的協(xié)議缺陷例如：使用公鑰密碼系統(tǒng)加密交換消息時(shí)，不能預(yù)防中間人攻擊

3、口令/密鑰猜測(cè)缺陷：指用戶選擇一些常用詞作為其口令，而導(dǎo)致攻擊者能進(jìn)行口令猜測(cè)攻擊；或者選取了不安全的偽隨機(jī)數(shù)生成算法構(gòu)造密鑰，使攻擊者能夠恢復(fù)該密鑰安全協(xié)議存在安全缺陷常見(jiàn)缺陷陳舊消息缺陷：指設(shè)計(jì)中對(duì)消息的新鮮性沒(méi)有充分考慮，從而使攻擊者能夠進(jìn)行消息重放攻擊，包括消息源的攻擊、消息目的的攻擊等 并行會(huì)話缺陷：指協(xié)議對(duì)并行會(huì)話攻擊缺乏防范，從而導(dǎo)致攻擊者通過(guò)交換適當(dāng)?shù)膮f(xié)議消息能夠獲得所需要的信息。包括并行會(huì)話單角色缺陷、并行會(huì)話多角色缺陷等內(nèi)部協(xié)議缺陷：指協(xié)議的可達(dá)性存在問(wèn)題，協(xié)議的參與者中至少有一方不能夠完成所有必需的動(dòng)作而導(dǎo)致的缺陷密碼系統(tǒng)缺陷：指協(xié)議中使用的密碼算法和安全協(xié)議導(dǎo)致協(xié)議不能

4、完全滿足所要求的機(jī)密性、完整性等需求而產(chǎn)生的缺陷 內(nèi)容提要安全協(xié)議存在安全缺陷安全協(xié)議形式化分析類BAN邏輯形式化分析例子：對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析安全協(xié)議形式化分析需求從前面的認(rèn)證協(xié)議、密鑰建立協(xié)議來(lái)看，幾乎所有協(xié)議都有安全漏洞迫切需要一套協(xié)議的安全分析方法，以指導(dǎo)協(xié)議設(shè)計(jì)安全協(xié)議形式化分析就是一種正規(guī)的、標(biāo)準(zhǔn)的方法，可有效檢查協(xié)議是否滿足其安全目標(biāo)形式化分析被視作分析協(xié)議安全的有效工具 安全協(xié)議形式化分析主要技術(shù)現(xiàn)有的安全協(xié)議形式化分析技術(shù)主要有四種：邏輯方法：采用基于信仰和知識(shí)邏輯的形式分析方法，比如以BAN邏輯為代表的類BAN邏輯通用形式化分析方法：采用一些通用的形式分析方法

5、來(lái)分析安全協(xié)議，例如應(yīng)用Petri網(wǎng)等模型檢測(cè)方法：基于代數(shù)方法構(gòu)造一個(gè)運(yùn)行協(xié)議的有限狀態(tài)系統(tǒng)模型，再利用狀態(tài)檢測(cè)工具來(lái)分析安全協(xié)議定理證明方法：將密碼協(xié)議的安全行作為定理來(lái)證明，這是一個(gè)新的研究熱點(diǎn) 內(nèi)容提要安全協(xié)議存在安全缺陷安全協(xié)議形式化分析類BAN邏輯形式化分析例子：對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析類BAN邏輯形式化分析BAN邏輯形式化在眾多協(xié)議形式化分析方法中，其中最具有影響的是1989年由Burrows、Abadi和Needham提出的BAN邏輯成功地對(duì)NS協(xié)議，Kerberos等幾個(gè)著名的協(xié)議進(jìn)行了分析，找到了其中已知的和未知的漏洞由此，激發(fā)了密碼研究者對(duì)密碼協(xié)議形式分析的興趣

6、并導(dǎo)致許多密碼協(xié)議形式分析方法的產(chǎn)生 BAN邏輯只在抽象層次上討論認(rèn)證協(xié)議的安全行，而不考慮其具體實(shí)現(xiàn)的安全缺陷和因加密體制而引發(fā)的協(xié)議缺陷類BAN邏輯形式化分析BAN邏輯形式化它是一種基于主體信念以及用于從已知信念推出新的信念的推理規(guī)則的邏輯基本原理：它可形式化定義協(xié)議的目標(biāo)，并確定協(xié)議初始時(shí)刻各參與者的知識(shí)和信任，通過(guò)協(xié)議里消息的發(fā)送和接收步驟產(chǎn)生新知識(shí)，運(yùn)用推導(dǎo)規(guī)則來(lái)得到目標(biāo)信任和知識(shí)如果得到最終的關(guān)于知識(shí)和信任的語(yǔ)句集里不包含所要得到的信任和知識(shí)的語(yǔ)句時(shí)，就表明協(xié)議存在安全缺陷即：通過(guò)相互發(fā)送和接收消息，協(xié)議雙方能否從最初的信念逐漸發(fā)展到協(xié)議運(yùn)行最終要達(dá)到的目的類BAN邏輯形式化分析對(duì)

7、BAN邏輯修改或擴(kuò)充人們發(fā)現(xiàn)BAN邏輯在分析某些協(xié)議和協(xié)議攻擊時(shí)，功能還不夠完善，對(duì)協(xié)議中某些性能的推理能力有限，因此各國(guó)學(xué)者又提出了許多修改和擴(kuò)充意見(jiàn)，其中較為著名的有：GNY邏輯AT邏輯VO邏輯和SVO邏輯它們統(tǒng)稱為BAN類邏輯類BAN邏輯形式化分析對(duì)BAN邏輯修改或擴(kuò)充GNY邏輯對(duì)BAN邏輯作了如下重要改進(jìn)與推進(jìn)：通過(guò)新增加的邏輯構(gòu)件與規(guī)則，推廣了BAN邏輯的應(yīng)用范圍增加了“擁有密鑰”的表達(dá)式，增加了GNY邏輯本身的表達(dá)能力在GNY邏輯中，區(qū)分一個(gè)主體收到的消息和一個(gè)主體可用的消息在GNY邏輯中，進(jìn)一步區(qū)分一個(gè)主體自己生成的消息和其它消息在GNY邏輯的分析中，在理想化協(xié)議中保留明文；而在

8、BAN邏輯分析中，明文在認(rèn)證過(guò)程中不起作用類BAN邏輯形式化分析對(duì)BAN邏輯修改或擴(kuò)充AT邏輯AT邏輯比BAN邏輯更接近的模態(tài)邏輯：對(duì)BAN邏輯中的定義和推理規(guī)則進(jìn)行整理，拋棄其中語(yǔ)義和實(shí)現(xiàn)細(xì)節(jié)的混合部分：對(duì)某些邏輯構(gòu)件引入更直接的定義，免除對(duì)誠(chéng)實(shí)性進(jìn)行隱含假設(shè)簡(jiǎn)化了推理規(guī)則，所有的概念都獨(dú)立定義，不與其它概念相混淆整個(gè)邏輯只有兩條基本推理規(guī)則：MP 規(guī)則(modus pones)Nec規(guī)則(necessitation) 在AT邏輯中有一條比BAN邏輯更加直接的管轄公理A15類BAN邏輯形式化分析對(duì)BAN邏輯修改或擴(kuò)充VO邏輯其貢獻(xiàn)在于：拓展了BAN邏輯的應(yīng)用范圍。VO邏輯的設(shè)計(jì)目標(biāo)就是增加分

9、析Diffie-Hellman協(xié)議的能力，進(jìn)而可以分析IETF標(biāo)準(zhǔn)Internet密鑰交換協(xié)議IKE和SSL協(xié)議等它細(xì)化了認(rèn)證協(xié)議的認(rèn)證目標(biāo)類BAN邏輯形式化分析對(duì)BAN邏輯修改或擴(kuò)充雖形式化分析已獲得了較大發(fā)展，但它還需在以下幾方面提高：擴(kuò)展現(xiàn)有的形式化分析工具的能力，使之不僅能分析證明一個(gè)安全協(xié)議的不安全性，還能證明協(xié)議的安全性以及分析和評(píng)測(cè)系統(tǒng)的安全性為現(xiàn)有形式語(yǔ)言構(gòu)造完善的數(shù)學(xué)描述，并進(jìn)行嚴(yán)謹(jǐn)?shù)睦碚撟C明；為各種協(xié)議形式化分析方法形成統(tǒng)一的形式語(yǔ)言表述，以描述可利用的必要信息，并使之能夠應(yīng)用于一些新的應(yīng)用協(xié)議的分析中將形式化方法應(yīng)用于協(xié)議說(shuō)明和協(xié)議涉及階段，使之不僅僅用于分析具體的某個(gè)安

10、全協(xié)議的安全性，從而可以極小的代價(jià)盡可能早地發(fā)現(xiàn)錯(cuò)誤 類BAN邏輯形式化分析BAN邏輯形式化形式化分析的步驟：首先需要進(jìn)行“理想化”，即將協(xié)議的消息轉(zhuǎn)換為BAN邏輯中的公式再根據(jù)具體情況進(jìn)行合理的假設(shè)再由邏輯的推理規(guī)則，根據(jù)理想化協(xié)議和假設(shè)進(jìn)行推理，推斷協(xié)議能否完成預(yù)期的目標(biāo) 類BAN邏輯形式化分析BAN邏輯形式化BAN邏輯系統(tǒng)的假設(shè)如下：密文塊不能被篡改，也不能用幾個(gè)小的密文塊來(lái)拼湊成一個(gè)新的大的密文塊一個(gè)消息中的兩個(gè)密文塊被看作是分兩次分別到達(dá)的加密系統(tǒng)是完善的，只有知道密鑰的主體才能解讀密文消息，任何不知道密鑰的主體都不能解讀密文消息，也沒(méi)有辦法根據(jù)密文推導(dǎo)密鑰密文含有足夠的冗余消息，解

11、密者可以根據(jù)解密的結(jié)果來(lái)判斷他是否已經(jīng)正確解密消息中有足夠的冗余消息，使得主體可以判斷該消息是否來(lái)源于自身BAN邏輯還假設(shè)協(xié)議的參與主體是誠(chéng)實(shí)的 類BAN邏輯形式化分析BAN邏輯形式化BAN邏輯主要包含下面三種處理對(duì)象：主體密鑰公式，也被稱為語(yǔ)句或命題依照BAN邏輯的慣例，P，Q，R等表示主體變量，K表示密鑰變量，X，Y表示公式變量。A，B表示主體，S表示服務(wù)器協(xié)議的每個(gè)消息表達(dá)為該邏輯的一個(gè)公式Na、Nb、Nc代表具體的觀點(diǎn)(如隨機(jī)數(shù))X、Y代表一般意義上的消息推導(dǎo)規(guī)則“邏輯公式X1, X2, ., Xn成立則Y成立”記為類BAN邏輯形式化分析BAN邏輯形式化基本公式語(yǔ)義P、Q主體變量，泛指

12、參與協(xié)議的各方X公式變量，泛指協(xié)議中消息的含義P |= XP相信X；P相信X為真P XP看見(jiàn)X；P曾經(jīng)收到過(guò)包含X的消息并且讀到XP | XP曾經(jīng)說(shuō)過(guò)X；P曾經(jīng)發(fā)送過(guò)包含X的消息P |= XP可以裁定X；相信P對(duì)于X的真值的判定#(X)X是新鮮的；X在當(dāng)前協(xié)議運(yùn)行前沒(méi)有被發(fā)現(xiàn)過(guò)P和Q共享一個(gè)好的密鑰k：“好”代表k依舊具有保密性P具有密鑰公鑰k(私鑰是k-1)，這個(gè)私鑰只有P以及他信任的人知道P和Q分享秘密X：這個(gè)秘密只有P、Q以及他們信任的人知道XK用k加密X后的消息YX與消息Y結(jié)合BAN邏輯：推理規(guī)則消息含義規(guī)則使主體推知其他主體發(fā)送過(guò)的消息說(shuō)明消息的出處共享秘鑰情況公鑰情況共享秘鑰情況B

13、AN邏輯：推理規(guī)則臨時(shí)值驗(yàn)證規(guī)則使主體推知其他主體的信仰BAN邏輯：推理規(guī)則管轄規(guī)則拓展了主體的推知能力使主體可以在基于其他主體已有的信仰之上推知新的信仰BAN邏輯：推理規(guī)則接收消息規(guī)則定義了主體在協(xié)議運(yùn)行中對(duì)消息的獲取規(guī)則1規(guī)則2BAN邏輯：推理規(guī)則接收消息規(guī)則定義了主體在協(xié)議運(yùn)行中對(duì)消息的獲取規(guī)則3規(guī)則4BAN邏輯：推理規(guī)則接收消息規(guī)則定義了主體在協(xié)議運(yùn)行中對(duì)消息的獲取規(guī)則5BAN邏輯：推理規(guī)則信仰規(guī)則反映了信念在消息的級(jí)聯(lián)與分割的不同操作中的一致性規(guī)則1規(guī)則2BAN邏輯：推理規(guī)則信仰規(guī)則反映了信念在消息的級(jí)聯(lián)與分割的不同操作中的一致性規(guī)則3規(guī)則4BAN邏輯：推理規(guī)則新鮮性規(guī)則如果一個(gè)公式

14、的一部分是新鮮的，則該公式的全部是新鮮的BAN邏輯：推理規(guī)則密鑰與秘密共享規(guī)則共享密鑰和共享秘密具有對(duì)稱性規(guī)則1規(guī)則2BAN邏輯：推理規(guī)則密鑰與秘密共享規(guī)則共享密鑰和共享秘密具有對(duì)稱性規(guī)則3規(guī)則4內(nèi)容提要安全協(xié)議存在安全缺陷安全協(xié)議形式化分析類BAN邏輯形式化分析例子：對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析分析步驟BAN邏輯的分析步驟對(duì)協(xié)議的進(jìn)行理想化將協(xié)議的實(shí)際消息轉(zhuǎn)換成BAN邏輯的公式給出協(xié)議初始狀態(tài)及其所基于的假設(shè)對(duì)協(xié)議進(jìn)行解釋注釋將形如PQ: X的協(xié)議步驟轉(zhuǎn)換成形如QX的邏輯語(yǔ)言形式化說(shuō)明協(xié)議將達(dá)成的安全目標(biāo)應(yīng)用公理和推理規(guī)則以及協(xié)議會(huì)話事實(shí)和假設(shè)，從協(xié)議

15、的開(kāi)始進(jìn)行推證直至驗(yàn)證協(xié)議是否滿足其最終運(yùn)行目標(biāo)對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析理想化協(xié)議協(xié)議的理想化目的非形式化的符號(hào)表達(dá)非常模糊示例一理想化之前：A-B:A, kABkBS告訴B(它知道kBS) kAB是它和A的通信秘鑰理想化之后：對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析理想化協(xié)議協(xié)議的理想化理想化的一些簡(jiǎn)單的指導(dǎo)方針如果任何時(shí)候接收者得到一個(gè)真實(shí)消息m后能推導(dǎo)出發(fā)送者必須相信X，那么m能被解釋成一個(gè)公式X現(xiàn)實(shí)中的隨機(jī)數(shù)被轉(zhuǎn)化為任意的新公式假定在整個(gè)過(guò)程中發(fā)送者都相信這些公式：Y把Y作為一個(gè)秘密使用，僅當(dāng)該秘密用作身份證明時(shí)有效出于實(shí)用性目的，每個(gè)主體總是相信它作為消息產(chǎn)生的公式對(duì)NSSK認(rèn)證

16、協(xié)議的BAN邏輯分析理想化協(xié)議協(xié)議的注釋在協(xié)議執(zhí)行過(guò)程中，一系列關(guān)于各個(gè)主體的信條和所看到的內(nèi)容的說(shuō)明發(fā)送第一條消息以前的公式表示各主體在協(xié)議開(kāi)始時(shí)的信條初始假設(shè)各主體之間共享了哪些密鑰那些主體能產(chǎn)生新鮮的隨機(jī)數(shù)哪些主體在哪方面被信任合法注釋的主要規(guī)則如果在P-Q: Y 之前X成立，則之后X和QY都成立如果根據(jù)推理規(guī)則，能從已知的X推到出Y，則X成立時(shí)Y必然成立如果能從X得到Y(jié) ，則X成立時(shí)Y也成立對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析分析NS協(xié)議Needham-Schroeder(NS)協(xié)議A-S: A, B , NaS-A: Na, B, kab, AkbskasA-B: kab, AkbsB-A: NbkabA-B: Nb - 1kab對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析分析NS協(xié)議理想化協(xié)議對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析分析NS協(xié)議初始假設(shè)對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析分析NS協(xié)議注釋NS協(xié)議對(duì)NSSK認(rèn)證協(xié)議的BAN邏輯分析分析NS協(xié)