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

前言
第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ī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)ur
3.4.1 Mur系統(tǒng)
3.4.2 Mur協(xié)議分析過程
3.4.3 Mur協(xié)議分析實(shí)例
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é)議分析實(shí)例
3.7 本章 小結(jié)
3.8 習(xí)題
第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é)議分析實(shí)例
4.2.4 基于階函數(shù)的自動化驗證技術(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 描述攻擊者不可知項集合的不變式
4.5.3 描述攻擊者可知項集合的不變式
4.6 本章 小結(jié)
4.7 習(xí)題
第5章 安全協(xié)議的形式化設(shè)計方法
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ù)字信封v
7.3.4 SEL協(xié)議的形式化分析
7.4 本章 小結(jié)
7.5 習(xí)題
第8章 移動通信安全協(xié)議及其分析
8.1 移動通信安全協(xié)議
8.1.1 第1代移動通信安全協(xié)議
8.1.2 第2代移動通信安全協(xié)議
8.1.3 第3代移動通信安全協(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 移動用戶與移動核心網(wǎng)之間的安全性驗證
8.3.2 服務(wù)網(wǎng)絡(luò)基站與移動核心網(wǎng)之間的安全性驗證
8.3.3 服務(wù)網(wǎng)絡(luò)基站與移動用戶之間的安全性驗證
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)
出版說明