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

前言
第1章 緒論
1.1 安全協(xié)議概述
1.1.1 安全協(xié)議的基本概念
1.1.2 安全協(xié)議的缺陷分析
1.1.3 安全協(xié)議的攻擊手段
1.1.4 安全協(xié)議形式化方法的必要性
1.2 形式化技術基礎
1.2.1 模態(tài)邏輯技術
1.2.2 模型檢測技術
1.2.3 定理證明技術
1.3 形式化方法在安全協(xié)議驗證中的應用
1.3.1 安全協(xié)議形式化理論發(fā)展現(xiàn)狀
1.3.2 安全協(xié)議形式化方法發(fā)展趨勢
1.4 本章 小結
1.5 習題
第2章 基于模態(tài)邏輯技術的安全協(xié)議分析方法
2.1 BAN邏輯
2.1.1 基本術語
2.1.2 推理規(guī)則
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 安全協(xié)議的Nonmonotomic邏輯描述
2.4.2 安全協(xié)議的Nonmonotomic邏輯分析
2.5 本章 小結
2.6 習題
第3章 基于模型檢測技術的安全協(xié)議分析方法
3.1 Dolev Yao模型
3.2 通信進程方法
3.2.1 CSP的基本概念
3.2.2 CSP的網(wǎng)絡模型
3.2.3 協(xié)議安全性質的CSP描述
3.2.4 CSP協(xié)議分析
3.3 NRL協(xié)議分析器
3.3.1 協(xié)議描述
3.3.2 協(xié)議分析
3.3.3 實例
3.4 模型檢測工具Mur
3.4.1 Mur系統(tǒng)
3.4.2 Mur協(xié)議分析過程
3.4.3 Mur協(xié)議分析實例
3.5 模型檢測工具ASTRAL
3.6 協(xié)議分析工具BRUTUS
3.6.1 BRUTUS協(xié)議描述模型
3.6.2 BRUTUS協(xié)議屬性邏輯
3.6.3 BRUTUS協(xié)議驗證算法
3.6.4.BRUTUS協(xié)議分析實例
3.7 本章 小結
3.8 習題
第4章 基于定理證明的安全協(xié)議分析方法
4.1 Paulson歸納法
4.1.1 Paulson歸納法簡介
4.1.2 Paulson歸納法的自動化理論
4.1.3 Paulson歸納法協(xié)議分析示例
4.2 Schneider階函數(shù)
4.2.1 階函數(shù)的定義
4.2.2 階函數(shù)定理
4.2.3 協(xié)議分析實例
4.2.4 基于階函數(shù)的自動化驗證技術
4.3 串空間
4.3.1 基本概念
4.3.2 協(xié)議入侵者描述
4.3.3 安全屬性的表示
4.3.4 協(xié)議分析舉例
4.3.5 認證測試方法
4.4 重寫逼近法
4.4.1 預備知識
4.4.2 逼近技術
4.4.3 對NS公鑰協(xié)議的描述與分析
4.5 不變式產(chǎn)生技術
4.5.1 基本概念
4.5.2 描述攻擊者不可知項集合的不變式
4.5.3 描述攻擊者可知項集合的不變式
4.6 本章 小結
4.7 習題
第5章 安全協(xié)議的形式化設計方法
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 復雜協(xié)議
5.3 BSW簡單邏輯
5.3.1 模型
5.3.2 邏輯
5.4 本章 小結
5.5 習題
第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é)議分析器進行形式化分析
6.2.2 利用擴展BSW邏輯分析
6.3 IKEV2協(xié)議概述
6.3.1 IKEV2密鑰交換
6.3.2 密鑰算法協(xié)商
6.3.3 加密密鑰與認證密鑰
6.4 IKEV2協(xié)議的形式化分析
6.4.1 擴展串空間理論
6.4.2 IKEV2協(xié)議分析
6.5 本章 小結
6.6 習題
第7章 電子商務安全協(xié)議及其分析
7.1 早期的電子商務安全協(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 雙重簽名技術
7.3.3 數(shù)字信封v
7.3.4 SEL協(xié)議的形式化分析
7.4 本章 小結
7.5 習題
第8章 移動通信安全協(xié)議及其分析
8.1 移動通信安全協(xié)議
8.1.1 第1代移動通信安全協(xié)議
8.1.2 第2代移動通信安全協(xié)議
8.1.3 第3代移動通信安全協(xié)議
8.2 AUTLOG認證邏輯對AKA協(xié)議的分析
8.2.1 AUTLOG認證邏輯
8.2.2 協(xié)議的形式化描述
8.2.3 假設前提
8.2.4 協(xié)議目標
8.2.5 形式化證明
8.3 利用認證測試方法對3GPP-AKA，協(xié)議進行安全性分析
8.3.1 移動用戶與移動核心網(wǎng)之間的安全性驗證
8.3.2 服務網(wǎng)絡基站與移動核心網(wǎng)之間的安全性驗證
8.3.3 服務網(wǎng)絡基站與移動用戶之間的安全性驗證
8.4 本章 小結
8.5 習題
第9章 群組通信安全協(xié)議及其分析
9.1 群組通信概述
9.2 群組密鑰管理協(xié)議
9.3 密鑰管理方案
9.3.1 集中式密鑰管理方案
9.3.2 分布式密鑰分發(fā)方案
9.3.3 分擔式密鑰協(xié)商方案
9.4 群組密鑰交換協(xié)議的形式化描述及安全性分析
9.4.1 AT-GDH協(xié)議
9.4.2 AT-GDH2協(xié)議
9.4.3 AT-GDH3協(xié)議
9.5 本章 小結
9.6 習題
參考文獻
出版說明