《安全协议实施自动化生成与验证》包括五篇，共15章。系统地全面介绍了安全实施自动化生成与验证的基本理论和关键技术及新成果。主要内容包括安全协议规范与实施的形式化分析与验证的国内外发展现状、基于计算模型自动化抽取安全协议Blanchet演算实施模型、安全协议Blanchet演算实施自动化抽取工具JAVA2CV、基于计算模型自动化生成安全协议Java实施模型、安全协议Java实施自动化生成工具CV2JAVA、基于符号模型自动化生成安全协议Java实施模型、安全协议Java实施自动化生成工具PV2JAVA、典型安全协议Java实施生成与验证等。
　　《安全协议实施自动化生成与验证》可供从事安全协议、密码学、计算机、软件工程、通信、数学等专业的科技人员、硕士和博士研究生参考，也可供高等院校相关专业的师生参考。

第一篇 安全协议规范及实施形式化分析与验证
第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 Blanchet演算
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 0penIDConnect安全协议
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 握手协议
……
第三篇 基于计算模型自动化验证安全协议Java实施
第四篇 基于计算模型自动化生成安全协议Java实施
第五篇 基于符号模型自动化生成安全协议Java实施