基于符号模型自动化生成安全协议代码研究

摘要

在信息化高速发展的今天，人们越来越多的使用网络来获知信息，也越来越多的将个人信息提交到网络，社交聊天工具和一些网络应用的普及使得人们越来越多的关注信息安全。安全协议是信息安全的重要组成部分，由两个及以上的参与方在进行一系列消息交换后达到某种既定目的。目前对安全协议进行形式化分析，即用形式化建模方法分析验证安全协议的安全性，包括保密性和认证性等，人们做了大量工作。但是仅仅分析安全协议抽象规范的安全是不够的，因为在安全协议具体实施的过程中可能产生新的安全问题，因此安全协议实施安全成为安全协议研究的重要组成部分。
　　本文对安全协议实施安全进行研究，完成以下工作：
　　（1）根据应用PI演算与Java语言的操作语义关系，给出从应用PI演算到Java语言的语法结构的映射关系；
　　（2）提出从安全协议应用PI演算实施生成安全协议 Java实施的方法。首先对应用PI演算进行词法分析和语法分析，生成其语法树；接着根据转换映射，完成应用PI演算语法树到Java语法树的转换，最终将具有安全性的应用PI演算转成Java实施；
　　（3）开发转换工具PV2JAVA，可将安全协议应用PI演算实施转为安全协议Java实施；
　　（4）使用应用PI演算对SAML2.0、Oauth2.0、改进的Oauth2.0、SSHV2、TLS1.2五个安全协议进行形式化建模分析，应用ProVerif工具分析这些安全协议认证性，然后使用PV2JAVA对这些安全协议的应用PI演算实施转为Java实施，调整后放入eclipse运行，分析认证性，并与ProVerif得到的认证性结果进行对比，证明转换的正确性。

目录

声明

第一章 绪论

1.1研究背景和意义

1.2国内外研究现状

1.3本文的组织结构

第二章 安全协议形式化分析及实施安全

2.1 安全协议简介

2.2 安全协议分析方法

2.3 基于符号模型的安全协议形式化分析方法

2.4 实施安全

2.5 本章小结

第三章 应用PI演算和Java语法映射关系

3.1 应用PI演算

3.2 ProVerif

3.3 应用PI演算BNF范式

3.4 应用PI演算和Java语法映射关系

3.5 本章小结

第四章 从应用PI演算自动化生成安全协议Java实施方法

4.1 可视化语法分析器antlrworks

4.2使用ANTLRWorks对应用PI演算词法及语法分析

4.3 使用ANTLRWorks生成可视化语法树

4.4 抽象语法树转换

4.5 由Java抽象语法树生成Java语句

4.6 本章小结

第五章 开发安全协议代码转换工具PV2JAVA

5.1 软件结构设计

5.2 导入应用PI演算语句

5.3 生成应用PI演算语法树

5.4生成Java语法树

5.5生成Java代码

5.6 本章小结

第六章 验证安全协议Java代码认证性

6.1 协议应用PI演算表示

6.2 安全协议Java表示

6.3 安全协议Java代码认证性验证

6.4 本章小结

第七章 总结与展望

参考文献

致谢

附录A 攻读学位期间所发表的学术论文目录