第一篇 安全协议规范及实施形式化分析与验证

第1章 安全协议规范形式化分析与验证发展现状

1.1 引言

1.2 符号模型

1.3 计算模型

1.4 本章小结

参考文献

第2章 安全协议实施生成与验证发展现状

2.1 引言

2.2 模型抽取：验证安全协议实施

2.2.1 程序验证

2.2.2 模型抽取

2.3 代码生成：生成安全协议实施

2.4 安全协议实施生成与验证模型

2.4.1 安全协议实施模型抽取

2.4.2 安全协议实施生成

2.5 本章小结

参考文献

第二篇 安全协议规范形式化分析与验证

第3章 AppliedPI演算与其BNF范式

3.1 引言

3.2 AppliedPI演算

3.3 AppliedPI演算BNF范式

3.4 本章小结

参考文献

第4章 一阶定理证明器ProVerif及应用

4.1 引言

4.2 一阶定理证明器ProVerif

4.3 ProVerif的输入和输出

4.4 自动化分析基于SAML2.0的联合身份认证协议安全性

4.4.1 基于SAML2.0的联合身份认证协议

4.4.2 应用AppliedPI演算对基于SAML2.0的联合身份认证协议形式化建模

4.4.3 利用ProVerif验证基于SAML2.0的联合身份认证协议的秘密性和认证性

4.4.4 分析结果

4.5 本章小结

参考文献

第5章 概率进程演算Blanchet演算与其BNF范式

5.1 引言

5.2 B1anchet演算

5.3 Blanchet演算BNF范式

5.4 本章小结

参考文献

第6章 自动化安全协议证明器CryptoVerif及应用

6.1 引言

6.2 自动化安全协议证明器CryptoVerif

6.2.1 结构

6.2.2 证明目标

6.2.3 语法

6.3 自动化分析OpenIDConnect安全协议认证性

6.3.1 OpenIDConnect安全协议

6.3.2 应用Blanchet演算对OpenIDConnect安全协议形式化建模

6.3.3 利用CryptoVerif验证OpenIDConnect安全协议的认证性

6.3.4 分析结果

6.4 自动化分析改进的OAuth2.0安全协议认证性

6.4.1 改进的OAuth2.0安全协议

6.4.2 应用Blanchet演算对改进的OAuth2.0安全协议形式化建模

6.4.3 利用CryptoVerif验证改进的OAuth2.0安全协议的认证性

6.4.4 分析结果

6.5 自动化分析TLS1.2握手协议安全性

6.5.1 TLS1.2握手协议

6.5.2 应用Blanchet演算对TLS1.2握手协议形式化建模

6.5.3 利用CryptoVerif验证TLS1.2握手协议的秘密性和认证性

6.5.4 分析结果

6.6 自动化分析OAuth2.0安全协议认证性

6.6.1 OAuth2.0安全协议

6.6.2 应用Blanchet演算对OAuth2.0安全协议形式化建模

6.6.3 利用CryptoVerif验证OAuth2.0安全协议的认证性

6.6.4 分析结果

6.7 本章小结

参考文献

第三篇 基于计算模型自动化验证安全协议Java实施

第7章 基于计算模型自动化抽取安全协议Blanchet演算实施模型

7.1 引言

7.2 Java语言子集SubJava的确定

7.3 Java语言到Blanchet演算映射模型

7.4 SubJava语言到Blanchet演算语句映射关系

7.5 SubJava语言类型到Blanchet演算类型映射关系

7.6 本章小结

参考文献

第8章 安全协议抽象规范模型生成工具JAVA2CV

8.1 引言

8.2 JAVA2CV架构

8.3 JAVA2CV词法分析器

8.4 JAVA2CV语法解析器

8.5 JAVA2CV语法树化简器

8.6 JAVA2CV翻译器

8.7 JAVA2CV代码生成器

8.8 JAVA2CV模板器

8.9 JAVA2CV使用手册

8.10 本章小结

参考文献

第9章 Needham-Schroeder安全协议Java实施生成与验证

9.1 引言

9.2 Needham-Schroeder安全协议

9.3 Needham-Schroeder安全协议Java实施

9.4 生成Needham-Schroeder安全协议Blanchet演算实施

9.5 Needham-Schroeder安全协议Blanchet演算实施认证性验证

9.6 本章小结

参考文献

第四篇 基于计算模型自动化生成安全协议Java实施

第10章 基于计算模型自动化生成安全协议Java实施模型

10.1 引言

10.2 Blanchet演算到Java语言映射模型

10.3 Blanchet演算到Java语言语句映射关系

10.4 Blanchet演算类型到Java语言类型映射关系

10.5 本章小结

参考文献

第11章 安全协议Java实施自动化生成工具CV2JAVA

11.1 引言

11.2 CV2JAVA架构

11.3 CV2JAVA词法分析器

11.4 CV2JAVA语法解析器

11.5 CV2JAVA语法树化简器

11.6 CV2JAVA翻译器

11.7 CV2JAVA代码生成器

11.8 CV2JAVA模板器

11.9 CV2JAVA使用手册

11.10 本章小结

参考文献

第12章 SSH安全协议Java实施生成与验证

12.1 引言

12.2 SSH安全协议

12.2.1 SSHv2协议结构

12.2.2 SSHv2消息流程

12.2.3 SSHv2的用户认证

12.3 应用Blanchet演算对SSHv2安全协议形式化建模

12.3.1 建立Blanchet演算模型

12.3.2 协议事件声明

12.3.3 验证结果

12.4 生成SSH安全协议Java实施

12.5 分析生成的SSH安全协议Java实施的安全性

12.6 本章小结

参考文献

第五篇 基于符号模型自动化生成安全协议Java实施

第13章 基于符号模型自动化生成安全协议Java实施模型

13.1 引言

13.2 AppliedPI演算到Java语言映射模型

13.3 AppliedPI演算到Java语言语句映射关系

13.4 AppliedPI演算类型到Java语言类型映射关系

13.5 本章小结

参考文献

第14章 安全协议Java实施自动化生成工具PV2JAVA

14.1 引言

14.2 PV2JAVA架构

14.3 PV2JAVA词法分析器

14.4 PV2JAVA语法解析器

14.5 PV2JAVA化简器

14.6 PV2JAVA翻译器

14.7 PV2JAVA代码生成器

14.8 PV2JAVA模板器

14.9 PV2JAVA使用手册

14.10 本章小结

参考文献

第15章 典型安全协议Java实施生成与验证

15.1 引言

15.2 安全协议AppliedPI演算实施

15.3 安全协议AppliedPI演算实施分析结果

15.4 安全协议Java实施

15.5 验证安全协议Java实施认证性

15.6 本章小结

参考文献