安全协议实施自动化生成与验证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 一阶定理证明器ProVerif 49

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 自动化安全协议证明器CryptoVerif 85

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章 安全协议抽象规范模型生成工具JAVA2CV 171

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实施自动化生成工具CV2JAVA 217

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实施自动化生成工具PV2JAVA 273

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