第一部分 理论基础 3
第1章 数理逻辑基础 3
1.1 基本概念 3
1.2 命题逻辑 5
1.2.1 命题逻辑语法 5
1.2.2 命题逻辑语义 6
1.2.3 命题逻辑推演系统 7
1.2.4 命题逻辑的可靠性 8
1.3 谓词逻辑 9
1.3.1 谓词逻辑语法 9
1.3.2 谓词逻辑的语义 11
1.3.3 谓词逻辑推演系统 13
1.3.4 谓词逻辑的可靠性 13
1.4 模态逻辑 13
1.4.1 命题模态逻辑 14
1.4.2 谓词模态逻辑 17
1.4.3 知识逻辑与信念逻辑 19
1.5 Hoare逻辑 20
1.6 本章小结 21
参考文献 21
第2章 现代密码学基础 23
2.1 概述 23
2.1.1 加密方案 23
2.1.2 对加密方案的攻击 24
2.1.3 信息论安全 24
2.1.4 现代密码学 25
2.2 计算复杂性 26
2.2.1 图灵机 26
2.2.2 时间复杂性 27
2.2.3 P与NP 28
2.2.4 多项式时间归约 28
2.2.5 概率图灵机与BPP 29
2.3 计算安全 30
2.3.1 计算安全的概念 30
2.3.2 安全假设 31
2.3.3 几个安全相关概念 32
2.4 私钥加密 33
2.4.1 私钥加密方案 33
2.4.2 私钥加密方案的CPA安全 34
2.4.3 私钥加密方案的CCA安全 35
2.5 公钥加密 35
2.5.1 公钥加密方案 36
2.5.2 公钥加密方案的CPA安全 36
2.5.3 公钥加密方案的CCA安全 37
2.6 数字签名 37
2.6.1 数字签名方案 38
2.6.2 数字签名方案的安全性 38
2.7 安全性证明 39
2.7.1 概率多项式时间归约 39
2.7.2 混合论证 40
2.7.3 标准模型与随机应答器模型 40
2.8 本章小结 41
参考文献 42
第二部分 密码协议分析概述 45
第3章 密码协议 45
3.1 密码协议的概念与意义 45
3.2 密码协议的属性与分类 46
3.3 对密码协议的攻击 47
3.4 密码协议的表示法 50
3.5 密码协议实例 51
3.6 本章小结 59
参考文献 60
第4章 密码协议分析 61
4.1 形式化方法 61
4.1.1 形式化方法概览 61
4.1.2 DY模型 64
4.1.3 Woo-Lam模型及其扩展 66
4.2 计算方法 67
4.2.1 计算方法概览 67
4.2.2 BR模型 68
4.2.3 其他模型 71
4.3 密码协议形式化分析的计算可靠性 71
4.3.1 基于映射的方法 72
4.3.2 基于模拟的方法 73
4.3.3 已有形式化方法的计算可靠性 73
4.3.4 计算方法的直接形式化 74
4.4 可复合密码协议分析 75
4.5 密码协议逻辑 76
4.6 本章小结 77
参考文献 77
第三部分 密码协议逻辑 87
第5章 BAN逻辑 87
5.1 BAN逻辑的语法 87
5.2 推理规则 88
5.3 协议及其目标的描述 92
5.3.1 协议理想化 92
5.3.2 协议注解 93
5.3.3 认证目标的形式化 94
5.4 协议分析实例 95
5.4.1 NSSK协议及其形式化分析 95
5.4.2 Kerberos协议及其形式化分析 98
5.5 对BAN逻辑语义的简单讨论 101
5.6 对BAN逻辑的不同意见 103
5.6.1 Nessett的评论 103
5.6.2 Snekkenes的评论 105
5.7 本章小结 107
参考文献 107
第6章 BAN逻辑的扩展 108
6.1 GNY逻辑 108
6.1.1 模型 108
6.1.2 GNY逻辑的语法 109
6.1.3 推理规则 111
6.1.4 协议形式化 117
6.1.5 协议分析实例 118
6.2 VO逻辑 123
6.2.1 语法扩展 123
6.2.2 公理与规则扩展 125
6.2.3 通用的形式化目标 125
6.2.4 通用的形式化假设 127
6.2.5 STS协议分析 127
6.3 MB逻辑 130
6.3.1 公式 131
6.3.2 推理规则 132
6.3.3 协议消息理想化 134
6.3.4 协议分析 135
6.4 本章小结 136
参考文献 137
第7章 类BAN逻辑的语义 138
7.1 AT逻辑 138
7.1.1 AT逻辑对BAN逻辑的改进 138
7.1.2 语法 141
7.1.3 公理系统 142
7.1.4 模型 143
7.1.5 AT逻辑的语义 145
7.2 SVO逻辑 148
7.2.1 SVO逻辑语言 148
7.2.2 公理系统 149
7.2.3 模型 152
7.2.4 SVO逻辑的语义 154
7.2.5 SVO逻辑的可靠性 158
7.2.6 基于SVO逻辑的协议分析 159
7.3 本章小结 162
参考文献 163
第8章 BAN逻辑的进一步扩展 164
8.1 Kailar逻辑 164
8.1.1 可追责性 164
8.1.2 分析框架 165
8.1.3 分析假设 166
8.1.4 逻辑规则 167
8.1.5 协议目标 169
8.1.6 分析实例 169
8.2 BSW逻辑 171
8.2.1 模型 172
8.2.2 BSW逻辑语言 173
8.2.3 推理规则 174
8.2.4 定理 175
8.2.5 合成规则 175
8.2.6 协议分析与设计的实例 177
8.3 本章小结 181
参考文献 181
第9章 非单调逻辑 182
9.1 引言 182
9.2 Moser逻辑 182
9.2.1 知道与相信公理 183
9.2.2 unless谓词 184
9.2.3 关于unless的例子 185
9.3 Rubin逻辑 186
9.3.1 khat协议 186
9.3.2 协议描述与分析概述 187
9.3.3 全局集 188
9.3.4 本地集 189
9.3.5 信任矩阵 190
9.3.6 行为描述 191
9.3.7 更新函数 193
9.3.8 推理规则 194
9.3.9 对khat协议的描述与分析 195
9.4 本章小结 199
参考文献 200
第10章 引入时间的协议逻辑 201
10.1 CKT5逻辑 201
10.1.1 CKT5逻辑术语 202
10.1.2 安全性定理 205
10.2 CS逻辑 208
10.2.1 语法 208
10.2.2 公理与推理规则 209
10.2.3 实例分析 211
10.3 GS逻辑 213
10.3.1 扩展术语及规则 214
10.3.2 协议分析实例 215
10.4 本章小结 218
参考文献 218
第11章 时间相关密码协议逻辑及其形式化语义 220
11.1 TCPL的引入 220
11.2 TCPL的语法 222
11.3 公理与规则 225
11.4 TCPL的语义 228
11.4.1 模型 228
11.4.2 语义 232
11.5 TCPL的可靠性 233
11.6 基于TCPL的密码协议形式化建模方案 238
11.6.1 密码协议建模 238
11.6.2 安全属性建模 241
11.7 基于TCPL的密码协议分析 243
11.7.1 定时发布协议 243
11.7.2 NSPK协议 249
11.8 进步讨论 250
11.9 本章小结 252
参考文献 252
第12章 协议复合逻辑 255
12.1 协议编程语言 255
12.1.1 PPL的语法 255
12.1.2 PPL的语义 258
12.2协议及其属性 259
12.2.1 协议执行模型 259
12.2.2 协议属性 260
12.3 PCL的语法与语义 261
12.3.1 PCL的语法 261
12.3.2 PCL的语义 262
12.4 证明系统 264
12.5 PCL的可靠性 267
12.6 协议分析实例 270
12.6.1 弱认证 270
12.6.2 强认证性 271
12.7 协议复合 272
12.7.1 并行复合 272
12.7.2 顺序复合 273
12.7.3 协议复合实例 274
12.8 PCL协议存在的问题 275
12.9 本章小结 276
参考文献 276
第四部分 计算可靠的密码协议逻辑 281
第13章 AR逻辑 281
13.1 形式化加密与消息等价 281
13.1.1 形式化消息 281
13.1.2 消息等价 282
13.2 加密方案与不可区分性 284
13.2.1 加密方案的安全性 284
13.2.2 加密方案安全性的定义 285
13.3 形式等价的计算可靠性 286
13.3.1 总体关联 287
13.3.2 等价性蕴涵不可区分性 287
13.4 不完备性 293
13.5 完备性定理 295
13.5.1 无混淆加密与认证加密 296
13.5.2 完备性定理 297
13.6 本章小结 305
参考文献 306
第14章 对AR逻辑的扩展 307
14.1 形式化模型 308
14.1.1 消息 308
14.1.2 模式 310
14.1.3 等价 313
14.2 计算模型 315
14.3 计算可靠性 317
14.4 本章小结 324
参考文献 325
第15章 计算可靠的PCL 327
15.1 协议语法 327
15.2 逻辑语法 328
15.3 证明系统 329
15.4 证明实例 330
15.5 协议的执行 331
15.6 计算语义 333
15.7 本章小结 336
参考文献 336
第16章 IK逻辑 337
16.1 T系统 338
16.1.1 语法 340
16.1.2 T系统的公理 341
16.1.3 T系统的可靠性 345
16.2 基于T系统的实例证明 345
16.3 计算不可区分系统 348
16.3.1 语法 348
16.3.2 证明规则 349
16.4 基于IK逻辑的证明实例 350
16.5 IK逻辑的可靠性 351
16.6 本章小结 352
参考文献 353
第17章 计算不可区分逻辑 354
17.1 应答器系统 354
17.1.1 应答器系统与敌手 354
17.1.2 语义 357
17.1.3 事件 358
17.2 CIL的语句与基本规则 359
17.2.1 语句 359
17.2.2 基本规则 359
17.3 上下文 360
17.4 互模拟 362
17.5 确定性 364
17.6 CIL的规则与可靠性 364
17.6.1 上下文与应答器规则 364
17.6.2 派生规则与外部前提 365
17.7 概率签名方案 366
17.7.1 随机应答器 367
17.7.2 形式化证明 368
17.8 本章小结 372
参考文献 373
结束语 374
索引 377