網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證

前言

隨著以Internet為代表的信息化浪潮席卷全球，信息技術(shù)的應(yīng)用日益普及和廣泛，但I(xiàn)nternet所具有的開放性、國際性和自由性在增加應(yīng)用自由度的同時(shí)，對安全也提出了更高的要求，信息安全已成為關(guān)系到國家安全和經(jīng)濟(jì)發(fā)展的重大戰(zhàn)略問題。安全協(xié)議（也稱密碼協(xié)議）是一個(gè)分布式算法，它規(guī)定了兩個(gè)或多個(gè)通信主體在一次通信過程中必須執(zhí)行的一系列步驟。安全協(xié)議利用密碼技術(shù)實(shí)現(xiàn)開放網(wǎng)絡(luò)環(huán)境下的安全通信，達(dá)到信息安全的目的，廣泛地應(yīng)用于身份認(rèn)證、接入控制、密鑰分配、電子商務(wù)等領(lǐng)域。因此，安全協(xié)議作為實(shí)現(xiàn)信息安全的基礎(chǔ)，其自身的安全性間.題已成為安全研究的重要內(nèi)容。由于網(wǎng)絡(luò)安全協(xié)議的重要性，從1978年第一個(gè)安全協(xié)議（Needham-Schroeder協(xié)議）誕生以來，人們對它的分析和設(shè)計(jì)就一直沒有停止過，也做出了卓有成效的工作。.最初，人們基于經(jīng)驗(yàn)和單純的軟件測試，采用攻擊檢驗(yàn)方法來分析其安全性。由于安全協(xié)議往往運(yùn)行在復(fù)雜的、不安全的網(wǎng)絡(luò)環(huán)境中，同時(shí)，新的攻擊方法層出不窮，產(chǎn)生的錯(cuò)誤很難完全由人工識別。因此，很難保證對協(xié)議安全性分析的準(zhǔn)確性。人們一致認(rèn)為，必須采用形式化的方法和工具來分析密碼協(xié)議的安全性，即采用數(shù)學(xué)或邏輯模型，通過有效的程序來分析系統(tǒng)及其條件，以此確定一種在系統(tǒng)滿足條件情況下所得的證明是否正確的數(shù)學(xué)理論和方法。形式化方法在網(wǎng)絡(luò)安全協(xié)議分析中的作用主要體現(xiàn)在：①能使分析概念清晰；②能發(fā)現(xiàn)協(xié)議設(shè)計(jì)中的錯(cuò)誤；③能證明協(xié)議的正確性；④能作為安全協(xié)議自動(dòng)化分析、設(shè)計(jì)技術(shù)的理論指導(dǎo)。最先提出采用形式化方法分析密碼協(xié)議的是Needham和Schroeder。然而，在這一領(lǐng)域中第一項(xiàng)探索性的工作是由Dolev和Yao完成的，隨后由Dolev、Even和Karp在20世紀(jì)70年代后期和80年代初開發(fā)了一系列多項(xiàng)式時(shí)間算法來確定密碼協(xié)議的安全性。自1983年Dolev.Yao形式化模型提出以后，密碼協(xié)議形式化方法的研究有了長足的發(fā)展，到目前為止已形成了兩大流派，并且出現(xiàn)了理論融合的趨勢。一種流派稱為計(jì)算流派，它基于一個(gè)詳細(xì)的計(jì)算模型，安全性推理通常是通過構(gòu)造一個(gè)“歸約為矛盾”類型的證明得到的，這里的“矛盾”是指計(jì)算復(fù)雜性領(lǐng)域中一個(gè)困難問題的有效解。隨機(jī)預(yù)言機(jī)模型（ROM）、作為該流派的代表，對于分析密碼算法的安全性有著公認(rèn)的、廣泛的應(yīng)用。另一流派稱為邏輯符號流派，它基于簡單而有效的形式化語言方法，對公理的應(yīng)用可以基于邏輯證明、定理證明或狀態(tài)搜索技術(shù)。本書著重討論邏輯符號流派的主要S-作。目前，形式化理論在安全協(xié)議驗(yàn)證中的應(yīng)用主要集中在形式化分析、形式化設(shè)計(jì)及自動(dòng)化工具開發(fā)3個(gè)方面。同時(shí)，隨著密碼技術(shù)的不斷發(fā)展和安全應(yīng)用需求的不斷擴(kuò)大。安全協(xié)議的結(jié)構(gòu)也越來越復(fù)雜化，這些都對現(xiàn)有的形式化協(xié)議分析技術(shù)提出了很大的挑戰(zhàn)。

內(nèi)容概要

　　《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》概述了形式化技術(shù)在網(wǎng)絡(luò)安全協(xié)議分析、驗(yàn)證中的主要應(yīng)用原理及現(xiàn)狀；在此基礎(chǔ)上詳細(xì)地?cái)⑹隽司W(wǎng)絡(luò)安全協(xié)議的形式化分析技術(shù)、形式化設(shè)計(jì)技術(shù);最后重點(diǎn)介紹了目前的形式化分析技術(shù)對當(dāng)前典型應(yīng)用環(huán)境下復(fù)雜、實(shí)用網(wǎng)絡(luò)安全協(xié)議的分析成果，包括IPSec協(xié)議、SSL協(xié)議、電子商務(wù)協(xié)議、移動(dòng)通信安全協(xié)議及群組通信安全協(xié)議等。　　信息安全是關(guān)系到國家安全和經(jīng)濟(jì)發(fā)展的重大戰(zhàn)略問題，至關(guān)重要。安全協(xié)議作為實(shí)現(xiàn)信息安全的基礎(chǔ)，其自身的安全性問題已成為安全研究的重要內(nèi)容。目前，針對安全協(xié)議的安全性驗(yàn)證已形成了許多不同的流派、理論和方法?！毒W(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》理論與應(yīng)用并重，深入淺出地介紹了各類形式化分析技術(shù)的基本原理及其在大型復(fù)雜安全協(xié)議分析中的實(shí)際應(yīng)用。　　《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》可作為信息安全專業(yè)高年級本科生教材，也可作為高等學(xué)校電子信息類、計(jì)算機(jī)類等相關(guān)專業(yè)的參考書。

書籍目錄

前言第1章 緒論1.1 安全協(xié)議概述1.1.1 安全協(xié)議的基本概念1.1.2 安全協(xié)議的缺陷分析1.1.3 安全協(xié)議的攻擊手段1.1.4 安全協(xié)議形式化方法的必要性1.2 形式化技術(shù)基礎(chǔ)1.2.1 模態(tài)邏輯技術(shù)1.2.2 模型檢測技術(shù)1.2.3 定理證明技術(shù)1.3 形式化方法在安全協(xié)議驗(yàn)證中的應(yīng)用1.3.1 安全協(xié)議形式化理論發(fā)展現(xiàn)狀1.3.2 安全協(xié)議形式化方法發(fā)展趨勢1.4 本章 小結(jié)1.5 習(xí)題第2章 基于模態(tài)邏輯技術(shù)的安全協(xié)議分析方法2.1 BAN邏輯2.1.1 基本術(shù)語2.1.2 推理規(guī)則2.1.3 應(yīng)用實(shí)例2.2 類BAN邏輯2.2.1 GNY邏輯2.2.2 AT邏輯2.2.3 SVO邏輯2.2.4 Kailar邏輯2.3 Bieber邏輯2.3.1 歷史模型2.3.2 KT5邏輯2.3.3 CKT5通信邏輯2.3.4 消息的解釋2.3.5 認(rèn)證與保密2.4 非單調(diào)邏輯2.4.1 安全協(xié)議的Nonmonotomic邏輯描述2.4.2 安全協(xié)議的Nonmonotomic邏輯分析2.5 本章 小結(jié)2.6 習(xí)題第3章 基于模型檢測技術(shù)的安全協(xié)議分析方法3.1 Dolev Yao模型3.2 通信進(jìn)程方法3.2.1 CSP的基本概念3.2.2 CSP的網(wǎng)絡(luò)模型3.2.3 協(xié)議安全性質(zhì)的CSP描述3.2.4 CSP協(xié)議分析3.3 NRL協(xié)議分析器3.3.1 協(xié)議描述3.3.2 協(xié)議分析3.3.3 實(shí)例3.4 模型檢測工具M(jìn)ur3.4.1 Mur系統(tǒng)3.4.2 Mur協(xié)議分析過程3.4.3 Mur協(xié)議分析實(shí)例3.5 模型檢測工具ASTRAL3.6 協(xié)議分析工具BRUTUS3.6.1 BRUTUS協(xié)議描述模型3.6.2 BRUTUS協(xié)議屬性邏輯3.6.3 BRUTUS協(xié)議驗(yàn)證算法3.6.4.BRUTUS協(xié)議分析實(shí)例3.7 本章 小結(jié)3.8 習(xí)題第4章 基于定理證明的安全協(xié)議分析方法4.1 Paulson歸納法4.1.1 Paulson歸納法簡介4.1.2 Paulson歸納法的自動(dòng)化理論4.1.3 Paulson歸納法協(xié)議分析示例4.2 Schneider階函數(shù)4.2.1 階函數(shù)的定義4.2.2 階函數(shù)定理4.2.3 協(xié)議分析實(shí)例4.2.4 基于階函數(shù)的自動(dòng)化驗(yàn)證技術(shù)4.3 串空間4.3.1 基本概念4.3.2 協(xié)議入侵者描述4.3.3 安全屬性的表示4.3.4 協(xié)議分析舉例4.3.5 認(rèn)證測試方法4.4 重寫逼近法4.4.1 預(yù)備知識4.4.2 逼近技術(shù)4.4.3 對NS公鑰協(xié)議的描述與分析4.5 不變式產(chǎn)生技術(shù)4.5.1 基本概念4.5.2 描述攻擊者不可知項(xiàng)集合的不變式4.5.3 描述攻擊者可知項(xiàng)集合的不變式4.6 本章 小結(jié)4.7 習(xí)題第5章 安全協(xié)議的形式化設(shè)計(jì)方法5.1 合成協(xié)議模型及其安全性5.1.1 HT模型5.1.2 協(xié)議的組合5.2 Fail-Stop協(xié)議5.2.1 Fail-Stop協(xié)議及其分析5.2.2 復(fù)雜協(xié)議5.3 BSW簡單邏輯5.3.1 模型5.3.2 邏輯5.4 本章 小結(jié)5.5 習(xí)題第6章 Internet密鑰交換協(xié)議及其分析6.1 Internet密鑰交換協(xié)議概述6.1.1 階段1主模式交換6.1.2 階段1野蠻模式交換6.1.3 階段2快速模式交換6.2 IKE三協(xié)議的形式化分析6.2.1 采用NRL協(xié)議分析器進(jìn)行形式化分析6.2.2 利用擴(kuò)展BSW邏輯分析6.3 IKEV2協(xié)議概述6.3.1 IKEV2密鑰交換6.3.2 密鑰算法協(xié)商6.3.3 加密密鑰與認(rèn)證密鑰6.4 IKEV2協(xié)議的形式化分析6.4.1 擴(kuò)展串空間理論6.4.2 IKEV2協(xié)議分析6.5 本章 小結(jié)6.6 習(xí)題第7章 電子商務(wù)安全協(xié)議及其分析7.1 早期的電子商務(wù)安全協(xié)議7.1.1 Digicash協(xié)議7.1.2 First Virtual協(xié)議7.1.3 Netbill協(xié)議7.2 SSL協(xié)議及其分析7.2.1 SSL協(xié)議介紹7.2.2 SSL協(xié)議的形式化分析7.3 SET協(xié)議及其分析7.3.1 SET協(xié)議的流程7.3.2 雙重簽名技術(shù)7.3.3 數(shù)字信封v7.3.4 SEL協(xié)議的形式化分析7.4 本章 小結(jié)7.5 習(xí)題第8章 移動(dòng)通信安全協(xié)議及其分析8.1 移動(dòng)通信安全協(xié)議8.1.1 第1代移動(dòng)通信安全協(xié)議8.1.2 第2代移動(dòng)通信安全協(xié)議8.1.3 第3代移動(dòng)通信安全協(xié)議8.2 AUTLOG認(rèn)證邏輯對AKA協(xié)議的分析8.2.1 AUTLOG認(rèn)證邏輯8.2.2 協(xié)議的形式化描述8.2.3 假設(shè)前提8.2.4 協(xié)議目標(biāo)8.2.5 形式化證明8.3 利用認(rèn)證測試方法對3GPP-AKA，協(xié)議進(jìn)行安全性分析8.3.1 移動(dòng)用戶與移動(dòng)核心網(wǎng)之間的安全性驗(yàn)證8.3.2 服務(wù)網(wǎng)絡(luò)基站與移動(dòng)核心網(wǎng)之間的安全性驗(yàn)證8.3.3 服務(wù)網(wǎng)絡(luò)基站與移動(dòng)用戶之間的安全性驗(yàn)證8.4 本章 小結(jié)8.5 習(xí)題第9章 群組通信安全協(xié)議及其分析9.1 群組通信概述9.2 群組密鑰管理協(xié)議9.3 密鑰管理方案9.3.1 集中式密鑰管理方案9.3.2 分布式密鑰分發(fā)方案9.3.3 分擔(dān)式密鑰協(xié)商方案9.4 群組密鑰交換協(xié)議的形式化描述及安全性分析9.4.1 AT-GDH協(xié)議9.4.2 AT-GDH2協(xié)議9.4.3 AT-GDH3協(xié)議9.5 本章 小結(jié)9.6 習(xí)題參考文獻(xiàn)出版說明

章節(jié)摘錄

插圖：6.密碼系統(tǒng)缺陷密碼系統(tǒng)缺陷是指協(xié)議中使用的密碼算法不合適或?qū)γ艽a算法的實(shí)現(xiàn)不當(dāng)，而導(dǎo)致協(xié)議不能完全滿足所要求安全需求而產(chǎn)生的缺陷。應(yīng)該指出的是，隨著攻擊手段與技術(shù)的不斷翻新，以上缺陷并不能涵蓋網(wǎng)絡(luò)安全協(xié)議在實(shí)際應(yīng)用中的所有可能出現(xiàn)的漏洞。一個(gè)安全協(xié)議在運(yùn)行過程中，假如有攻擊者存在，并且沒有被系統(tǒng)或者誠實(shí)角色所察覺，同時(shí)攻擊者在參與協(xié)議運(yùn)行過程中并沒有利用任何密碼學(xué)上的漏洞，那么我們就說該協(xié)議存在設(shè)計(jì)上的漏洞。本書只討論由于協(xié)議設(shè)計(jì)漏洞所產(chǎn)生的協(xié)議缺陷。1.1.3 安全協(xié)議的攻擊手段針對信息系統(tǒng)的攻擊主要有兩種形式，即被動(dòng)竊聽和主動(dòng)分析。前者是通過非法搭線竊聽，截取通信信息后進(jìn)行分析以獲得機(jī)密內(nèi)容或敏感信息：后者指對通信信息進(jìn)行非法修改，包括插入非法信息、重放陳舊信息、刪除通信消息和修改通信消息等。一個(gè)被動(dòng)攻擊者可以在線竊聽敏感信息，而一個(gè)主動(dòng)攻擊者則可截獲數(shù)據(jù)包并對其進(jìn)行任意的修改，甚至可以偽裝成通信主體，欺騙誠實(shí)主體與其進(jìn)行非法的通信。實(shí)現(xiàn)這些攻擊的方法很多，比如可以對系統(tǒng)采用的密碼系統(tǒng)進(jìn)行數(shù)學(xué)分析、旁路攻擊以破解機(jī)密信息并對系統(tǒng)進(jìn)行即時(shí)監(jiān)聽等；另外，還有一類很重要的攻擊方式，那就是利用協(xié)議本身的漏洞攻擊信息系統(tǒng)，采用這種攻擊方式不需要很大的計(jì)算量，往往成為黑客的主要攻擊手段。下面簡要介紹一些由于協(xié)議設(shè)計(jì)漏洞而產(chǎn)生的針對安全協(xié)議的攻擊方式。1.中間人攻擊在中間人攻擊中，攻擊者將自己偽裝于兩個(gè)通信主體之間進(jìn)行通信，甚至可以冒充任一主體的身份向?qū)Ψ桨l(fā)送消息。考慮以下協(xié)議：在用戶Alice、Bob不知道對方私鑰的情況下，用戶Alice希望采用公鑰密碼技術(shù)向Bob發(fā)送一條秘密消息，協(xié)議使用：RSA公鑰加密算法。

編輯推薦

《網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證》：安全協(xié)議及其形式化技術(shù)的基本概念、原理和方法,安全協(xié)議的形式化分析方法,安全協(xié)議的形式化設(shè)計(jì)技術(shù),形式化技術(shù)在復(fù)雜安全協(xié)議分析中的典型應(yīng)用。

圖書封面

評論、評分、閱讀與下載

---

    網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗(yàn)證 PDF格式下載

---