作者：孟博，王德军
页数：249页
出版社：科学出版社
出版日期：2019
ISBN：9787030625069
电子书格式：pdf/epub/txt
内容简介
本书共分五篇14章。系统地全面介绍了安全协议实施安全性自动化分析与验证的基本理论和关键技术及最新成果。主要内容包括安全协议实施安全性分析与验证关键技术及国内外发展现状、应用PI演算、一阶定理证明器ProVerif及应用、概率进程演算Blanchet演算、自动化安全协议证明器CryptoVerif及应用、基于能够获取安全协议客户端实施和安全协议服务器端实施自动化分析其安全性、基于仅能够获取安全协议客户端实施自动化分析其安全性, 基于不能获取安全协议客户端实施和安全协议服务器端实施自动化分析其安全性等。
本书特色
本书共分五篇14章。系统地全面介绍了安全协议实施安全性自动化分析与验证的基本理论和关键技术及最成果。主要内容包括安全协议实施安全性分析与验证关键技术及国内外发展现状、应用PI演算、一阶定理证明器ProVerif及应用、概率进程演算Blanchet演算、自动化安全协议证明器CryptoVerif及应用、基于能够获取安全协议客户端实施和安全协议服务器端实施自动化分析其安全性、基于仅能够获取安全协议客户端实施自动化分析其安全性，基于不能获取安全协议客户端实施和安全协议服务器端实施自动化分析其安全性等。
目录
第1章 安全协议实施安全性分析与验证现状
1.1 引言
1.2 能够获取安全协议客户端实施和安全协议服务器端实施
1.2.1 程序验证
1.2.2 模型抽取
1.3 仅能够获取安全协议客户端实施
1.3.1 网络轨迹
1.3.2 模型抽取
1.4 不能获取安全协议客户端实施和安全协议服务器端实施
1.4.1 指令序列
1.4.2 网络轨迹
1.4.3 流量识别
参考文献
第2章 Applied PI演算与其BNF范式
2.1 引言
2.2 Applied PI演算语法及语义
2.3 Applied PI演算BNF范式
参考文献
第3章 一阶定理证明器ProVerif及应用
3.1 引言
3.2 一阶定理证明器ProVerif
3.3 ProVerif的输入和输出
3.4 自动化分析OpenID Connect安全协议安全性
3.4.1 OpenID Connect安全协议
3.4.2 应用Applied PI演算对OpenID Connect安全协议形式化建模
3.4.3 利用Proverif验证OpenID Connect安全协议秘密性和认证性
3.4.4 分析结果
3.5 自动化分析PPMUAS身份认证协议安全性
3.5.1 PPMUAS身份认证协议
3.5.2 应用Applied PI演算对PPMUAS身份认证协议形式化建模
3.5.3 利用Proverif验证PPMUAS身份认证协议秘密性和认证性
3.5.4 分析结果
3.6 自动化分析改进的OpenID Connect安全协议认证性
3.6.1 改进的OpenID Connect安全协议
3.6.2 应用Applied PI演算对改进的0penID Connect安全协议形式化建模
3.6.3 利用ProVerif验证改进的OpenID Connect安全协议认证性
3.6.4 分析结果
3.7 自动化分析Mynah安全协议认证性
3.7.1 Mynah安全协议
3.7.2 应用Applied PI演算对Mynah安全协议形式化建模
3.7.3 利用ProVerif验证Mynah安全协议认证性
3.7.4 分析结果
参考文献
第4章 概率进程演算Blanchet演算与其BNF范式
4.1 引言
4.2 Blanchet演算语法及语义
4.3 Blanchet演算BNF范式
参考文献
第5章 自动化安全协议证明器CryptoVerif及应用
5.1 引言
1.1 引言
1.2 能够获取安全协议客户端实施和安全协议服务器端实施
1.2.1 程序验证
1.2.2 模型抽取
1.3 仅能够获取安全协议客户端实施
1.3.1 网络轨迹
1.3.2 模型抽取
1.4 不能获取安全协议客户端实施和安全协议服务器端实施
1.4.1 指令序列
1.4.2 网络轨迹
1.4.3 流量识别
参考文献
第2章 Applied PI演算与其BNF范式
2.1 引言
2.2 Applied PI演算语法及语义
2.3 Applied PI演算BNF范式
参考文献
第3章 一阶定理证明器ProVerif及应用
3.1 引言
3.2 一阶定理证明器ProVerif
3.3 ProVerif的输入和输出
3.4 自动化分析OpenID Connect安全协议安全性
3.4.1 OpenID Connect安全协议
3.4.2 应用Applied PI演算对OpenID Connect安全协议形式化建模
3.4.3 利用Proverif验证OpenID Connect安全协议秘密性和认证性
3.4.4 分析结果
3.5 自动化分析PPMUAS身份认证协议安全性
3.5.1 PPMUAS身份认证协议
3.5.2 应用Applied PI演算对PPMUAS身份认证协议形式化建模
3.5.3 利用Proverif验证PPMUAS身份认证协议秘密性和认证性
3.5.4 分析结果
3.6 自动化分析改进的OpenID Connect安全协议认证性
3.6.1 改进的OpenID Connect安全协议
3.6.2 应用Applied PI演算对改进的0penID Connect安全协议形式化建模
3.6.3 利用ProVerif验证改进的OpenID Connect安全协议认证性
3.6.4 分析结果
3.7 自动化分析Mynah安全协议认证性
3.7.1 Mynah安全协议
3.7.2 应用Applied PI演算对Mynah安全协议形式化建模
3.7.3 利用ProVerif验证Mynah安全协议认证性
3.7.4 分析结果
参考文献
第4章 概率进程演算Blanchet演算与其BNF范式
4.1 引言
4.2 Blanchet演算语法及语义
4.3 Blanchet演算BNF范式
参考文献
第5章 自动化安全协议证明器CryptoVerif及应用
5.1 引言
