基本介紹
內容簡介,圖書目錄,
內容簡介
《網路安全協定的形式化分析與驗證》概述了形式化技術在網路安全協定分析、驗證中的主要套用原理及現狀；在此基礎上詳細地敘述了網路安全協定的形式化分析技術、形式化設計技術;最後重點介紹了目前的形式化分析技術對當前典型套用環境下複雜、實用網路安全協定的分析成果，包括IPSec協定、SSL協定、電子商務協定、移動通信安全協定及群組通信安全協定等。
信息安全是關係到國家安全和經濟發展的重大戰略問題，至關重要。安全協定作為實現信息安全的基礎，其自身的安全性問題已成為安全研究的重要內容。目前，針對安全協定的安全性驗證已形成了許多不同的流派、理論和方法。《網路安全協定的形式化分析與驗證》理論與套用並重，深入淺出地介紹了各類形式化分析技術的基本原理及其在大型複雜安全協定分析中的實際套用。
《網路安全協定的形式化分析與驗證》可作為信息安全專業高年級本科生教材，也可作為高等學校電子信息類、計算機類等相關專業的參考書。
圖書目錄
前言
第1章 緒論
1.1 安全協定概述
1.1.1 安全協定的基本概念
1.1.2 安全協定的缺陷分析
1.1.3 安全協定的攻擊手段
1.1.4 安全協定形式化方法的必要性
1.2 形式化技術基礎
1.2.1 模態邏輯技術
1.2.2 模型檢測技術
1.2.3 定理證明技術
1.3 形式化方法在安全協定驗證中的套用
1.3.1 安全協定形式化理論發展現狀
1.3.2 安全協定形式化方法發展趨勢
1.4 本章 小結
1.5 習題
第2章 基於模態邏輯技術的安全協定分析方法
2.1 BAN邏輯
2.1.1 基本術語
2.1.2 推理規則
2.1.3 套用實例
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 認證與保密
2.4 非單調邏輯
2.4.1 安全協定的Nonmonotomic邏輯描述
2.4.2 安全協定的Nonmonotomic邏輯分析
2.5 本章 小結
2.6 習題
第3章 基於模型檢測技術的安全協定分析方法
3.1 Dolev Yao模型
3.2 通信進程方法
3.2.1 CSP的基本概念
3.2.2 CSP的網路模型
3.2.3 協定安全性質的CSP描述
3.2.4 CSP協定分析
3.3 NRL協定分析器
3.3.1 協定描述
3.3.2 協定分析
3.3.3 實例
3.4 模型檢測工具Mur
3.4.1 Mur系統
3.4.2 Mur協定分析過程
3.4.3 Mur協定分析實例
3.5 模型檢測工具ASTRAL
3.6 協定分析工具BRUTUS
3.6.1 BRUTUS協定描述模型
3.6.2 BRUTUS協定屬性邏輯
3.6.3 BRUTUS協定驗證算法
3.6.4.BRUTUS協定分析實例
3.7 本章 小結
3.8 習題
第4章 基於定理證明的安全協定分析方法
4.1 Paulson歸納法
4.1.1 Paulson歸納法簡介
4.1.2 Paulson歸納法的自動化理論
4.1.3 Paulson歸納法協定分析示例
4.2 Schneider階函式
4.2.1 階函式的定義
4.2.2 階函式定理
4.2.3 協定分析實例
4.2.4 基於階函式的自動化驗證技術
4.3 串空間
4.3.1 基本概念
4.3.2 協定入侵者描述
4.3.3 安全屬性的表示
4.3.4 協定分析舉例
4.3.5 認證測試方法
4.4 重寫逼近法
4.4.1 預備知識
4.4.2 逼近技術
4.4.3 對NS公鑰協定的描述與分析
4.5 不變式產生技術
4.5.1 基本概念
4.5.2 描述攻擊者不可知項集合的不變式
4.5.3 描述攻擊者可知項集合的不變式
4.6 本章 小結
4.7 習題
第5章 安全協定的形式化設計方法
5.1 合成協定模型及其安全性
5.1.1 HT模型
5.1.2 協定的組合
5.2 Fail-Stop協定
5.2.1 Fail-Stop協定及其分析
5.2.2 複雜協定
5.3 BSW簡單邏輯
5.3.1 模型
5.3.2 邏輯
5.4 本章 小結
5.5 習題
第6章 Internet密鑰交換協定及其分析
6.1 Internet密鑰交換協定概述
6.1.1 階段1主模式交換
6.1.2 階段1野蠻模式交換
6.1.3 階段2快速模式交換
6.2 IKE三協定的形式化分析
6.2.1 採用NRL協定分析器進行形式化分析
6.2.2 利用擴展BSW邏輯分析
6.3 IKEV2協定概述
6.3.1 IKEV2密鑰交換
6.3.2 密鑰算法協商
6.3.3 加密密鑰與認證密鑰
6.4 IKEV2協定的形式化分析
6.4.1 擴展串空間理論
6.4.2 IKEV2協定分析
6.5 本章 小結
6.6 習題
第7章 電子商務安全協定及其分析
7.1 早期的電子商務安全協定
7.1.1 Digicash協定
7.1.2 First Virtual協定
7.1.3 Netbill協定
7.2 SSL協定及其分析
7.2.1 SSL協定介紹
7.2.2 SSL協定的形式化分析
7.3 SET協定及其分析
7.3.1 SET協定的流程
7.3.2 雙重簽名技術
7.3.3 數字信封v
7.3.4 SEL協定的形式化分析
7.4 本章 小結
7.5 習題
第8章 移動通信安全協定及其分析
8.1 移動通信安全協定
8.1.1 第1代移動通信安全協定
8.1.2 第2代移動通信安全協定
8.1.3 第3代移動通信安全協定
8.2 AUTLOG認證邏輯對AKA協定的分析
8.2.1 AUTLOG認證邏輯
8.2.2 協定的形式化描述
8.2.3 假設前提
8.2.4 協定目標
8.2.5 形式化證明
8.3 利用認證測試方法對3GPP-AKA，協定進行安全性分析
8.3.1 移動用戶與移動核心網之間的安全性驗證
8.3.2 服務網路基站與移動核心網之間的安全性驗證
8.3.3 服務網路基站與移動用戶之間的安全性驗證
8.4 本章 小結
8.5 習題
第9章 群組通信安全協定及其分析
9.1 群組通信概述
9.2 群組密鑰管理協定
9.3 密鑰管理方案
9.3.1 集中式密鑰管理方案
9.3.2 分散式密鑰分發方案
9.3.3 分擔式密鑰協商方案
9.4 群組密鑰交換協定的形式化描述及安全性分析
9.4.1 AT-GDH協定
9.4.2 AT-GDH2協定
9.4.3 AT-GDH3協定
9.5 本章 小結
9.6 習題
參考文獻
出版說明
