本书包括五篇，共15章。系统地全面介绍了安全实施自动化生成与验证的基本理论和关键技术及最新成果。主要内容包括安全协议规范与实施的形式化分析与验证的国内外发展现状、基于计算模型自动化抽取安全协议Blanchet演算实施模型、安全协议Blanchet演算实施自动化抽取工具JAVA2CV、基于计算模型自动化生成安全协议Java实施模型、安全协议Java实施自动化生成工具CV2JAVA、基于符号模型自动化生成安全协议Java实施模型、安全协议Java实施自动化生成工具PV2JAVA、典型安全协议Java实施生成与验证等。
样章试读
目录
- 目录
第一篇安全协议规范及实施形式化分析与验证
第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
第二篇安全协议规范形式化分析与验证
第3章AppliedPI演算与其BNF范式41
3.1引言41
3.2AppliedPI演算41
3.3AppliedPI演算BNF范式45
3.4本章小结48
参考文献48
第4章一阶定理证明器ProVerif及应用49
4.1引言49
4.2一阶定理证明器ProVerif49
4.3ProVerif的输入和输出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.2Blanchet演算73
5.3Blanchet演算BNF范式80
5.4本章小结83
参考文献84
第6章自动化安全协议证明器CryptoVerif及应用85
6.1引言85
6.2自动化安全协议证明器CryptoVerif85
6.2.1结构85
6.2.2证明目标90
6.2.3语法92
6.3自动化分析OpenIDConnect安全协议认证性94
6.3.1OpenIDConnect安全协议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.1TLS1.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.1OAuth2.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实施
第7章基于计算模型自动化抽取安全协议Blanchet演算实施模型161
7.1引言161
7.2Java语言子集SubJava的确定162
7.3Java语言到Blanchet演算映射模型164
7.4SubJava语言到Blanchet演算语句映射关系166
7.5SubJava语言类型到Blanchet演算类型映射关系169
7.6本章小结170
参考文献170
第8章安全协议抽象规范模型生成工具JAVA2CV171
8.1引言171
8.2JAVA2CV架构172
8.3JAVA2CV词法分析器174
8.4JAVA2CV语法解析器177
8.5JAVA2CV语法树化简器181
8.6JAVA2CV翻译器185
8.7JAVA2CV代码生成器186
8.8JAVA2CV模板器188
8.9JAVA2CV使用手册188
8.10本章小结191
参考文献192
第9章Needham-Schroeder安全协议Java实施生成与验证193
9.1引言193
9.2Needham-Schroeder安全协议194
9.3Needham-Schroeder安全协议Java实施195
9.4生成Needham-Schroeder安全协议Blanchet演算实施197
9.5Needham-Schroeder安全协议Blanchet演算实施认证性验证201
9.6本章小结206
参考文献206
第四篇基于计算模型自动化生成安全协议Java实施
第10章基于计算模型自动化生成安全协议Java实施模型209
10.1引言209
10.2Blanchet演算到Java语言映射模型209
10.3Blanchet演算到Java语言语句映射关系211
10.4Blanchet演算类型到Java语言类型映射关系214
10.5本章小结215
参考文献216
第11章安全协议Java实施自动化生成工具CV2JAVA217
11.1引言217
11.2CV2JAVA架构218
11.3CV2JAVA词法分析器221
11.4CV2JAVA语法解析器221
11.5CV2JAVA语法树化简器222
11.6CV2JAVA翻译器225
11.7CV2JAVA代码生成器229
11.8CV2JAVA模板器230
11.9CV2JAVA使用手册231
11.10本章小结235
参考文献236
第12章SSH安全协议Java实施生成与验证237
12.1引言237
12.2SSH安全协议237
12.2.1SSHv2协议结构238
12.2.2SSHv2消息流程239
12.2.3SSHv2的用户认证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实施
第13章基于符号模型自动化生成安全协议Java实施模型263
13.1引言263
13.2AppliedPI演算到Java语言映射模型263
13.3AppliedPI演算到Java语言语句映射关系265
13.4AppliedPI演算类型到Java语言类型映射关系271
13.5本章小结272
参考文献272
第14章安全协议Java实施自动化生成工具PV2JAVA273
14.1引言273
14.2PV2JAVA架构274
14.3PV2JAVA词法分析器276
14.4PV2JAVA语法解析器279
14.5PV2JAVA化简器289
14.6PV2JAVA翻译器294
14.7PV2JAVA代码生成器295
14.8PV2JAVA模板器299
14.9PV2JAVA使用手册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
京公网安备 11010102004214号