安全协议实施自动化生成与验证【2025|PDF|Epub|mobi|kindle电子书版本百度云盘下载】

安全协议实施自动化生成与验证PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

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

第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

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

第3章 AppliedPI演算与其BNF范式41

3.1 引言41

3.2 AppliedPI演算41

3.3 AppliedPI演算BNF范式45

3.4 本章小结48

参考文献48

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

4.1 引言49

4.2 一阶定理证明器ProVerif49

4.3 ProVerif的输入和输出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.2 B1anchet演算73

5.3 Blanchet演算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.1 OpenIDConnect安全协议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.1 TLS1.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.1 OAuth2.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实施161

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

7.1 引言161

7.2 Java语言子集SubJava的确定162

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

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

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

7.6 本章小结170

参考文献170

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

8.1 引言171

8.2 JAVA2CV架构172

8.3 JAVA2CV词法分析器174

8.4 JAVA2CV语法解析器177

8.5 JAVA2CV语法树化简器181

8.6 JAVA2CV翻译器185

8.7 JAVA2CV代码生成器186

8.8 JAVA2CV模板器188

8.9 JAVA2CV使用手册188

8.10 本章小结191

参考文献192

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

9.1 引言193

9.2 Needham-Schroeder安全协议194

9.3 Needham-Schroeder安全协议Java实施195

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

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

9.6 本章小结206

参考文献206

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

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

10.1 引言209

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

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

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

10.5 本章小结215

参考文献216

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

11.1 引言217

11.2 CV2JAVA架构218

11.3 CV2JAVA词法分析器221

11.4 CV2JAVA语法解析器221

11.5 CV2JAVA语法树化简器222

11.6 CV2JAVA翻译器225

11.7 CV2JAVA代码生成器229

11.8 CV2JAVA模板器230

11.9 CV2JAVA使用手册231

11.10 本章小结235

参考文献236

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

12.1 引言237

12.2 SSH安全协议237

12.2.1 SSHv2协议结构238

12.2.2 SSHv2消息流程239

12.2.3 SSHv2的用户认证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实施263

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

13.1 引言263

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

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

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

13.5 本章小结272

参考文献272

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

14.1 引言273

14.2 PV2JAVA架构274

14.3 PV2JAVA词法分析器276

14.4 PV2JAVA语法解析器279

14.5 PV2JAVA化简器289

14.6 PV2JAVA翻译器294

14.7 PV2JAVA代码生成器295

14.8 PV2JAVA模板器299

14.9 PV2JAVA使用手册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