第1章 绪论 1
1.1 安全协议概述 1
1.1.1 安全协议的基本概念 1
1.1.2 安全协议的缺陷分析 4
1.1.3 安全协议的攻击手段 6
1.1.4 安全协议形式化方法的必要性 11
1.2 形式化技术基础 12
1.2.1 模态逻辑技术 12
1.2.2 模型检测技术 13
1.2.3 定理证明技术 14
1.3 形式化方法在安全协议验证中的应用 14
1.3.1 安全协议形式化理论发展现状 14
1.3.2 安全协议形式化方法发展趋势 16
1.4 本章小结 17
1.5 习题 18
第2章 基于模态逻辑技术的安全协议分析方法 19
2.1 BAN逻辑 19
2.1.1 基本术语 19
2.1.2 推理规则 20
2.1.3 应用实例 22
2.2 类BAN逻辑 25
2.2.1 GNY逻辑 27
2.2.2 AT逻辑 33
2.2.3 SVO逻辑 37
2.2.4 Kailar逻辑 40
2.3 Bieber逻辑 42
2.3.1 历史模型 43
2.3.2 KT5逻辑 44
2.3.3 CKT5通信逻辑 44
2.3.4 消息的解释 45
2.3.5 认证与保密 46
2.4 非单调逻辑 49
2.4.1 安全协议的Nonmonotomic逻辑描述 49
2.4.2 安全协议的Nonmonotomic逻辑分析 53
2.5 本章小结 56
2.6 习题 57
第3章 基于模型检测技术的安全协议分析方法 58
3.1 Dolev-Yao模型 58
3.2 通信进程方法 59
3.2.1 CSP的基本概念 59
3.2.2 CSP的网络模型 61
3.2.3 协议安全性质的CSP描述 65
3.2.4 CSP协议分析 72
3.3 NRL协议分析器 73
3.3.1 协议描述 73
3.3.2 协议分析 75
3.3.3 实例 76
3.4 模型检测工具Mur？ 80
3.4.1 Mur？系统 80
3.4.2 Mur？协议分析过程 81
3.4.3 Mur？协议分析实例 81
3.5 模型检测工具ASTRAL 83
3.6 协议分析工具BRUTUS 85
3.6.1 BRUTUS协议描述模型 85
3.6.2 BRUTUS协议属性逻辑 87
3.6.3 BRUTUS协议验证算法 88
3.6.4 BRUTUS协议分析实例 88
3.7 本章小结 91
3.8 习题 92
第4章 基于定理证明的安全协议分析方法 93
4.1 Paulson归纳法 93
4.1.1 Paulson归纳法简介 93
4.1.2 Paulson归纳法的自动化理论 96
4.1.3 Paulson归纳法协议分析示例 99
4.2 Schneider阶函数 101
4.2.1 阶函数的定义 102
4.2.2 阶函数定理 102
4.2.3 协议分析实例 104
4.2.4 基于阶函数的自动化验证技术 110
4.3 串空间 110
4.3.1 基本概念 110
4.3.2 协议入侵者描述 113
4.3.3 安全属性的表示 114
4.3.4 协议分析举例 115
4.3.5 认证测试方法 117
4.4 重写逼近法 119
4.4.1 预备知识 119
4.4.2 逼近技术 120
4.4.3 对NS公钥协议的描述与分析 120
4.5 不变式产生技术 123
4.5.1 基本概念 124
4.5.2 描述攻击者不可知项集合的不变式 125
4.5.3 描述攻击者可知项集合的不变式 126
4.6 本章小结 127
4.7 习题 128
第5章 安全协议的形式化设计方法 129
5.1 合成协议模型及其安全性 129
5.1.1 HT模型 129
5.1.2 协议的组合 132
5.2 Fail-Stop协议 133
5.2.1 Fail-Stop协议及其分析 133
5.2.2 复杂协议 134
5.3 BSW简单逻辑 135
5.3.1 模型 135
5.3.2 逻辑 136
5.4 本章小结 137
5.5 习题 137
第6章 Internet密钥交换协议及其分析 138
6.1 Internet密钥交换协议概述 138
6.1.1 阶段1主模式交换 138
6.1.2 阶段1野蛮模式交换 142
6.1.3 阶段2快速模式交换 143
6.2 IKE协议的形式化分析 144
6.2.1 采用NRL协议分析器进行形式化分析 144
6.2.2 利用扩展BSW逻辑分析 146
6.3 IKE v2协议概述 150
6.3.1 IKE v2密钥交换 150
6.3.2 密钥算法协商 151
6.3.3 加密密钥与认证密钥 152
6.4 IKE v2协议的形式化分析 153
6.4.1 扩展串空间理论 153
6.4.2 IKE v2协议分析 154
6.5 本章小结 156
6.6 习题 156
第7章 电子商务安全协议及其分析 158
7.1 早期的电子商务安全协议 158
7.1.1 Digicash协议 158
7.1.2 FirstVirtual协议 159
7.1.3 Netbill协议 159
7.2 SSL协议及其分析 160
7.2.1 SSL协议介绍 160
7.2.2 SSL协议的形式化分析 162
7.3 SET协议及其分析 163
7.3.1 SET协议的流程 163
7.3.2 双重签名技术 164
7.3.3 数字信封 165
7.3.4 SET协议的形式化分析 165
7.4 本章小结 170
7.5 习题 170
第8章 移动通信安全协议及其分析 171
8.1 移动通信安全协议 171
8.1.1 第1代移动通信安全协议 171
8.1.2 第2代移动通信安全协议 172
8.1.3 第3代移动通信安全协议 173
8.2 AUTLOG认证逻辑对AKA协议的分析 177
8.2.1 AUTLOG认证逻辑 177
8.2.2 协议的形式化描述 178
8.2.3 假设前提 178
8.2.4 协议目标 179
8.2.5 形式化证明 179
8.3 利用认证测试方法对3GPP-AKA协议进行安全性分析 180
8.3.1 移动用户与移动核心网之间的安全性验证 181
8.3.2 服务网络基站与移动核心网之间的安全性验证 182
8.3.3 服务网络基站与移动用户之间的安全性验证 183
8.4 本章小结 183
8.5 习题 183
第9章 群组通信安全协议及其分析 184
9.1 群组通信概述 184
9.2 群组密钥管理协议 185
9.3 密钥管理方案 185
9.3.1 集中式密钥管理方案 185
9.3.2 分布式密钥分发方案 189
9.3.3 分担式密钥协商方案 189
9.4 群组密钥交换协议的形式化描述及安全性分析 190
9.4.1 AT-GDH协议 190
9.4.2 AT-GDH2协议 191
9.4.3 AT-GDH3协议 193
9.5 本章小结 206
9.6 习题 207
参考文献 208