前言
第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 習題
參考文獻
出版說明