第1章 密码协议概述 1
1.1 信息安全与加密 1
1.2 密码协议的分类 3
1.2.1 身份认证协议 3
1.2.2 密钥建立协议 3
1.2.3 电子商务协议 4
1.2.4 安全多方协议 4
1.3 密码协议的安全 4
1.4 本书的动机 9
参考文献 10
第2章 密码协议背景知识 13
2.1 预备知识 13
2.1.1 函数 13
2.1.2 术语 14
2.2 密码学基础 15
2.2.1 密码概念 15
2.2.2 对称密钥加密 17
2.2.3 公钥加密 17
2.2.4 数字签名 17
2.2.5 哈希函数 18
2.2.6 消息认证 19
2.3 密码协议 22
2.3.1 安全信道 22
2.3.2 主体 23
2.3.3 时变参数 24
2.3.4 挑战和响应 25
2.3.5 密码协议的其它分类 26
2.4 密码协议的安全性 26
2.4.1 针对基础密码算法的攻击 26
2.4.2 针对协议的攻击 28
2.4.3 协议的安全性 29
2.4.4 协议安全的分析方法 31
2.5 通信威胁模型 32
2.5.1 Dolev-Yao威胁模型 32
2.5.2 协议环境的假设 33
2.5.3 密码协议表达方式 35
参考文献 35
第3章 密码协议安全设计的工程原则 36
3.1 工程原则介绍 36
3.1.1 谨慎工程原则 37
3.1.2 密码协议工程原则 38
3.2 协议工程需求分析原则 39
3.2.1 安全需求分析原则 39
3.2.2 明文需求分析原则 41
3.2.3 应用环境分析原则 42
3.2.4 攻击者模型及攻击者能力分析原则 42
3.2.5 密码服务需求分析原则 43
3.3 密码协议工程的详细协议设计原则 44
3.3.1 主体通信的真实性原则 44
3.3.2 新鲜性标识符的新鲜性和生成者认证原则 57
3.3.3 消息的数据完整性保护原则 62
3.3.4 逐步细化的设计原则 64
3.4 密码协议工程的安全性证明原则 69
参考文献 71
第4章 密码协议的非形式化分析方法 75
4.1 密码协议安全性 75
4.1.1 在计算模型下的认证性和保密性 76
4.1.2 安全性定义 77
4.2 基于可信任新鲜性的安全机制 78
4.2.1 概念 78
4.2.2 新鲜性原则 84
4.2.3 认证协议的安全性 85
4.2.4 基于可信任新鲜性的分析方法 87
4.2.5 基于可信任新鲜性的安全性分析应用 88
4.3 一些经典攻击的分析 90
4.3.1 中间人攻击 91
4.3.2 源替换攻击 93
4.3.3 消息重放攻击 97
4.3.4 平行会话攻击 101
4.3.5 反射攻击 106
4.3.6 交错攻击 107
4.3.7 类型缺陷攻击 112
4.3.8 身份标识省略导致的攻击 115
4.3.9 由于密码服务误用导致的攻击 118
4.3.1 0其它协议的安全分析 120
参考文献 138
第5章 实际使用的网络协议安全分析 142
5.1 SSL协议和TLS协议 143
5.1.1 SSL和TLS概述 143
5.1.2 SSL握手协议 144
5.1.3 基于可信任新鲜性分析SSL协议的安全性 150
5.2 互联网协议安全 161
5.2.1 IPSec概览 161
5.2.2 互联网密钥交换（IKE）协议 164
5.2.3 基于可信任新鲜性分析IKE的安全性 172
5.3 Kerberos网络认证协议 181
5.3.1 Kerberos概览 182
5.3.2 基本的Kerberos网络认证服务 186
5.3.3 基于可信任新鲜性分析Kerberos的安全性 188
5.3.4 公钥Kerberos 192
参考文献 200
第6章 密码协议安全性的保证 202
6.1 认证性的安全定义 202
6.1.1 协议的形式化模型 203
6.1.2 通信的形式化模型 204
6.1.3 实体认证的形式化模型 205
6.2 SK－安全的安全性定义 207
6.2.1 CK模型中的协议和攻击者模型 208
6.2.2 CK模型中的SK－安全 210
6.3 基于可信任新鲜性的认证 211
6.3.1 可信任新鲜性 211
6.3.2 主体活现性 215
6.3.3 新鲜性标识符的保密性 216
6.3.4 新鲜性标识符的新鲜性 217
6.3.5 新鲜性标识符的关联性 217
6.3.6 基于可信任新鲜性的安全性分析 218
6.3.7 安全性定义 220
6.3.8 基于可信任新鲜性的不可否认性 226
参考文献 229
第7章 协议安全的形式化分析 230
7.1 BAN逻辑 231
7.1.1 基本符号 231
7.1.2 逻辑假设 232
7.1.3 基于BAN逻辑的安全分析步骤 233
7.1.4 BAN类逻辑 234
7.2 模型检验 235
7.3 定理证明 236
7.4 基于可信任新鲜性的信任多集 237
7.4.1 信任逻辑语言 237
7.4.2 逻辑假设 241
7.5 信任多集方法的应用 253
7.5.1 Needham-Schroeder公钥认证协议的分析 254
7.5.2 分布式传感器网中Kerberos对密钥协议分析 260
7.5.3 IEEE 802.1 1i中认证协议的分析 264
7.6 比较 274
参考文献 276
第8章 基于可信任新鲜性的密码协议设计 279
8.1 协议设计方法 279
8.1.1 认证协议设计的简单逻辑 280
8.1.2 失败停止协议设计 280
8.1.3 认证测试 281
8.1.4 Canetti-Krawczyk模型 281
8.1.5 安全协议设计模型及其复合框架 282
8.2 协议设计的安全属性目标 283
8.2.1 保密性 284
8.2.2 数据完整性 284
8.2.3 数据源认证 284
8.2.4 实体认证 288
8.2.5 源实体认证 291
8.2.6 不可抵赖性 292
8.2.7 访问控制 293
8.2.8 密钥建立 294
8.2.9 公平性 295
8.3 基于可信任新鲜性的协议设计 295
8.3.1 符号和描述 297
8.3.2 密码协议的设计 301
8.3.3 SK－安全协议的下界 303
8.4 可信任新鲜性在协议设计中的应用 309
参考文献 313
第9章 基于可信任新鲜性的密码协议自动化分析 315
9.1 已有的自动化分析方法 315
9.1.1 基于逻辑的自动化分析工具 315
9.1.2 基于模型检验的自动化分析工具 316
9.1.3 基于定理证明的自动化分析工具 318
9.1.4 CAPSL规范语言 319
9.2 基于可信任新鲜性的自动化密码协议分析 320
9.2.1 基于信任多集形式化方法的分析工具框架 320
9.2.2 BMF分析工具的两种初步实现的比较 321
9.2.3 信任多集形式化方法的实现 324
参考文献 337
索引 340