第1章 导论 1
Needham-Schroeder协议 1
更多的例子 4
其他身份鉴别协议的例子 4
加密的运用 6
时效 7
类型攻击 9
代数攻击 10
更复杂的协议和攻击 10
一些符号约定 11
第2章 消息认证与数字签名方案 13
消息认证方案及其抗伪造性质 13
强/弱抗伪造性质及其蕴涵关系 14
特例：基于拟随机函数的MAC方案 17
数字签名方案及其抗伪造性质 17
抗简单伪造性质及弱分支引理 18
抗选择消息伪造及强分支引理 21
数字签名方案与身份鉴别协议：Fiat-Shamir变换 24
正则身份鉴别协议及Fiat-Shamir变换 24
协议的抗身份欺诈性质与签名方案的抗伪造性质的等价性 27
时变方案、Fiat-Shamir变换及前向安全性质 30
第3章 对称加密方案 37
各种保密性质及其相互关系 37
各种保密性质的定义 37
各种保密性之间的关系 39
一些典型对称加密方案的保密性质 45
加密-认证方案：明文完整性与密文完整性 47
加密-认证方案的几个一般性构造 49
加密及认证式构造 49
先认证再加密式构造 50
先加密再认证式构造 52
时变对称加密方案及其前向保密性质 54
第4章 公钥加密方案（Ⅰ）：保密性质和PA性质 58
各种保密性质及其相互关系 58
保密性 59
密文非可塑性 61
随机oracle-范型的PA性质 65
非随机oracle-范型的PA性质 72
概念：PA0、PA1及PA2 72
PA性质与保密性质的关系 76
一些否定性结果 79
基于身份的公钥加密方案 81
一个随机oracle-范型的加密方案不可实现性的例子 85
方案构造及安全性证明 86
不可实现的实例 92
第5章 公钥加密方案（Ⅱ）：一些通用构造及其保密性条件 97
混合构造：Fuj isaki-Okamoto变换 97
方案构造及基本概念 98
IND CCA保密性条件 99
混合构造：REACT变换 105
方案构造及IND CCA保密性条件 106
其他混合构造 110
基于IBE构造公钥加密方案 110
Canetti-Halevi-Katz变换及其保密性条件 111
Boneh-Katz变换及其保密性条件 113
具有前向安全性质的时变公钥加密方案 116
基本概念 116
基于2-叉树加密方案的一般性构造 117
前向保密性条件 119
一个2-叉树加密方案的实例 121
第6章 公钥加密方案（Ⅲ）：匿名性质 123
各种匿名性质及其相互关系 123
匿名性、相对匿名性及其与保密性的关系 123
相对保密性及其与匿名性的关系 128
IBE方案的匿名性质及应用：PEKS方案 130
基本概念与BDOP变换 130
匿名与非匿名IBE方案的例子 135
Fujisaki-Okamoto变换的匿名性条件 137
ANO CPA匿名性的一个充要条件 138
ANO CCA匿名性的一个充分条件 143
REACT变换的匿名性条件 147
基于IBE的公钥加密方案的匿名性条件 151
Canetti-Halevi-Katz变换的匿名性条件 151
Boneh-Katz变换的匿名性条件 156
时变公钥加密方案的前向匿名条件 159
第7章 身份鉴别协议 163
Fiat-Shamir型身份鉴别协议与基于ID的身份鉴别协议 163
基本概念 164
cSS-2-IBI变换 169
再论Fiat-Shamir变换：基于ID的数字签名方案 170
一般性结果 172
实例 175
抗状态重置攻击的身份鉴别协议 179
基本概念 180
一般性构造：抗第一类状态重置攻击的协议IDP-I 184
一般性构造：抗第二类状态重置攻击的协议IDP-II 187
第8章 密码协议的UC-理论及应用 193
概念 193
协议的UC-运行模型及理想UC-模型 194
协议的UC-相似概念及基本性质 196
UC-稳定性定理 198
JUC-稳定性定理 200
一个弱UC-相似概念及弱UC-稳定性定理 200
典型密码协议的理想UC-模型与实现（Ⅰ）：消息的认证式传输 202
典型密码协议的理想UC-模型与实现（Ⅱ）：密钥交换 204
密钥交换协议的强UC-安全模型 205
密钥交换协议的UC-安全模型 206
典型密码协议的理想UC-模型与实现（Ⅲ）：安全信道 209
密码协议的结构化分析与设计理论概要 212
第9章Dolev-Yao理论（Ⅰ）：自由消息代数strand-图模型 214
密码协议的strand-图模型 214
消息代数与strand-图 214
攻击者-strand 217
消息代数的理想 218
strand-图理论的几个普遍结论 219
协议的安全性质 221
协议分析的例子 221
Needham-Schroeder-Lowe协议 221
Otway-Rees协议 224
第10章Dolev-Yao理论（Ⅱ）：自动分析技术 228
Athena：逻辑求解技术 228
基本概念和符号 228
形式演绎系统的语法及语义 229
算法 231
算法的优化 233
Millen-Shamtikov约束求解技术：自由消息代数情形 234
消息代数与攻击者模型 235
协议的安全性质 236
格局、变元与约束 236
约束求解算法 238
约束求解的例子：再论Needham-Schroeder-Lowe协议 239
算法的相容性和完备性 241
算法的改进和优化 241
第11章Dolev-Yao理论（Ⅲ）：带交换群算术的非自由消息代数 243
具代数能力的扩展Dolev-Yao攻击者模型 243
带交换群算术的非自由消息代数及扩展的Dolev-Yao攻击模型 244
形式演绎及其性质 246
约束的正则解及存在性 250
非自由消息代数的Millen-Shamtikov约束求解 252
猜测解的集合 252
猜测可导出的子项及其导出顺序 253
从演绎树中消去非M-和I-规则的分支 254
以新变元替换目标项 255
约化到线性Diophantine方程 255
第12章 密码协议形式模型的计算语义（Ⅰ）：被动攻击情形 258
自由消息代数的计算密码学语义 258
消息表达式的模式及共模关系 258
一些共模表达式的例子 259
几个重要性质 260
几个重要的加密类型及其精确的计算语义 261
消息表达式的计算语义 263
Abadi-Rogaway定理 264
计算语义的完备性 266
计算语义的一般性构造 269
形式模型 269
计算语义 270
语义类型 271
关于计算语义的几个普遍结果 272
应用：推广的Abadi-Rogaway定理 274
第13章 密码协议形式模型的计算语义（Ⅱ）：主动攻击情形 276
理论分析框架 277
一些辅助性结果 279
协议的形式模型的计算语义与算法模型的语法骨架 283
密码协议的Dolev-Yao刚性和Dolev-Yao相似性 285
关于Dolev-Yao刚性的主要结论及证明 286
Dolev-Yao刚性的复合-稳定性定理 286
Dolev-Yao刚性的相似-遗传定理 290
语法-语义相似性的对偶关系 291
总结与推广 293
附录A一些必要的数学事实 295
Euclid定理及等价形式 295
交换群的概念、性质和密码学中常见的例子 295
中国剩余定理 296
二次剩余及二次同余式x2=a mod p在特殊情况下的解 297
因子分解与求平方根难度等价 297
已知N的素因子分解，解多项式方程f（x）=0modN 298
参考文献 298
附录B进程代数模型：spi-演算 299
π-演算 299
概念 299
例子 300
spi-演算 302
概念 302
例子 302
形式演算 303
双向模拟 304
进程代数的计算语义：Abadi-Jurgens定理 306
参考文献 306
参考文献 307