安全协议实施安全性自动化分析与验证

第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 引言