第一篇 安全协议规范及实施形式化分析与验证 3
第1章 安全协议规范形式化分析与验证发展现状 3
1.1 引言 3
1.2 符号模型 4
1.3 计算模型 8
1.4 本章小结 14
参考文献 14
第2章 安全协议实施生成与验证发展现状 28
2.1 引言 28
2.2 模型抽取：验证安全协议实施 29
2.2.1 程序验证 29
2.2.2 模型抽取 29
2.3 代码生成：生成安全协议实施 31
2.4 安全协议实施生成与验证模型 32
2.4.1 安全协议实施模型抽取 32
2.4.2 安全协议实施生成 34
2.5 本章小结 35
参考文献 36
第二篇 安全协议规范形式化分析与验证 41
第3章 AppliedPI演算与其BNF范式 41
3.1 引言 41
3.2 AppliedPI演算 41
3.3 AppliedPI演算BNF范式 45
3.4 本章小结 48
参考文献 48
第4章 一阶定理证明器ProVerif及应用 49
4.1 引言 49
4.2 一阶定理证明器ProVerif 49
4.3 ProVerif的输入和输出 53
4.4 自动化分析基于SAML2.0的联合身份认证协议安全性 54
4.4.1 基于SAML2.0的联合身份认证协议 54
4.4.2 应用AppliedPI演算对基于SAML2.0的联合身份认证协议形式化建模 58
4.4.3 利用ProVerif验证基于SAML2.0的联合身份认证协议的秘密性和认证性 64
4.4.4 分析结果 68
4.5 本章小结 71
参考文献 71
第5章 概率进程演算Blanchet演算与其BNF范式 73
5.1 引言 73
5.2 B1anchet演算 73
5.3 Blanchet演算BNF范式 80
5.4 本章小结 83
参考文献 84
第6章 自动化安全协议证明器CryptoVerif及应用 85
6.1 引言 85
6.2 自动化安全协议证明器CryptoVerif 85
6.2.1 结构 85
6.2.2 证明目标 90
6.2.3 语法 92
6.3 自动化分析OpenIDConnect安全协议认证性 94
6.3.1 OpenIDConnect安全协议 94
6.3.2 应用Blanchet演算对OpenIDConnect安全协议形式化建模 97
6.3.3 利用CryptoVerif验证OpenIDConnect安全协议的认证性 102
6.3.4 分析结果 109
6.4 自动化分析改进的OAuth2.0安全协议认证性 111
6.4.1 改进的OAuth2.0安全协议 111
6.4.2 应用Blanchet演算对改进的OAuth2.0安全协议形式化建模 113
6.4.3 利用CryptoVerif验证改进的OAuth2.0安全协议的认证性 118
6.4.4 分析结果 125
6.5 自动化分析TLS1.2握手协议安全性 126
6.5.1 TLS1.2握手协议 126
6.5.2 应用Blanchet演算对TLS1.2握手协议形式化建模 128
6.5.3 利用CryptoVerif验证TLS1.2握手协议的秘密性和认证性 134
6.5.4 分析结果 139
6.6 自动化分析OAuth2.0安全协议认证性 141
6.6.1 OAuth2.0安全协议 141
6.6.2 应用Blanchet演算对OAuth2.0安全协议形式化建模 143
6.6.3 利用CryptoVerif验证OAuth2.0安全协议的认证性 150
6.6.4 分析结果 155
6.7 本章小结 156
参考文献 156
第三篇 基于计算模型自动化验证安全协议Java实施 161
第7章 基于计算模型自动化抽取安全协议Blanchet演算实施模型 161
7.1 引言 161
7.2 Java语言子集SubJava的确定 162
7.3 Java语言到Blanchet演算映射模型 164
7.4 SubJava语言到Blanchet演算语句映射关系 166
7.5 SubJava语言类型到Blanchet演算类型映射关系 169
7.6 本章小结 170
参考文献 170
第8章 安全协议抽象规范模型生成工具JAVA2CV 171
8.1 引言 171
8.2 JAVA2CV架构 172
8.3 JAVA2CV词法分析器 174
8.4 JAVA2CV语法解析器 177
8.5 JAVA2CV语法树化简器 181
8.6 JAVA2CV翻译器 185
8.7 JAVA2CV代码生成器 186
8.8 JAVA2CV模板器 188
8.9 JAVA2CV使用手册 188
8.10 本章小结 191
参考文献 192
第9章 Needham-Schroeder安全协议Java实施生成与验证 193
9.1 引言 193
9.2 Needham-Schroeder安全协议 194
9.3 Needham-Schroeder安全协议Java实施 195
9.4 生成Needham-Schroeder安全协议Blanchet演算实施 197
9.5 Needham-Schroeder安全协议Blanchet演算实施认证性验证 201
9.6 本章小结 206
参考文献 206
第四篇 基于计算模型自动化生成安全协议Java实施 209
第10章 基于计算模型自动化生成安全协议Java实施模型 209
10.1 引言 209
10.2 Blanchet演算到Java语言映射模型 209
10.3 Blanchet演算到Java语言语句映射关系 211
10.4 Blanchet演算类型到Java语言类型映射关系 214
10.5 本章小结 215
参考文献 216
第11章 安全协议Java实施自动化生成工具CV2JAVA 217
11.1 引言 217
11.2 CV2JAVA架构 218
11.3 CV2JAVA词法分析器 221
11.4 CV2JAVA语法解析器 221
11.5 CV2JAVA语法树化简器 222
11.6 CV2JAVA翻译器 225
11.7 CV2JAVA代码生成器 229
11.8 CV2JAVA模板器 230
11.9 CV2JAVA使用手册 231
11.10 本章小结 235
参考文献 236
第12章 SSH安全协议Java实施生成与验证 237
12.1 引言 237
12.2 SSH安全协议 237
12.2.1 SSHv2协议结构 238
12.2.2 SSHv2消息流程 239
12.2.3 SSHv2的用户认证 243
12.3 应用Blanchet演算对SSHv2安全协议形式化建模 244
12.3.1 建立Blanchet演算模型 244
12.3.2 协议事件声明 251
12.3.3 验证结果 251
12.4 生成SSH安全协议Java实施 255
12.5 分析生成的SSH安全协议Java实施的安全性 259
12.6 本章小结 259
参考文献 260
第五篇 基于符号模型自动化生成安全协议Java实施 263
第13章 基于符号模型自动化生成安全协议Java实施模型 263
13.1 引言 263
13.2 AppliedPI演算到Java语言映射模型 263
13.3 AppliedPI演算到Java语言语句映射关系 265
13.4 AppliedPI演算类型到Java语言类型映射关系 271
13.5 本章小结 272
参考文献 272
第14章 安全协议Java实施自动化生成工具PV2JAVA 273
14.1 引言 273
14.2 PV2JAVA架构 274
14.3 PV2JAVA词法分析器 276
14.4 PV2JAVA语法解析器 279
14.5 PV2JAVA化简器 289
14.6 PV2JAVA翻译器 294
14.7 PV2JAVA代码生成器 295
14.8 PV2JAVA模板器 299
14.9 PV2JAVA使用手册 299
14.10 本章小结 303
参考文献 304
第15章 典型安全协议Java实施生成与验证 305
15.1 引言 305
15.2 安全协议AppliedPI演算实施 305
15.3 安全协议AppliedPI演算实施分析结果 310
15.4 安全协议Java实施 312
15.5 验证安全协议Java实施认证性 314
15.6 本章小结 317
参考文献 317