| 摘要 | 第1-8页 |
| Abstract | 第8-10页 |
| 第1章 绪论 | 第10-12页 |
| ·研究背景和意义 | 第10-11页 |
| ·国内外研究现状 | 第11页 |
| ·本文的组织结构 | 第11-12页 |
| 第2章 安全协议及代码的安全性分析技术 | 第12-16页 |
| ·如何验证安全协议的安全 | 第12-13页 |
| ·安全协议代码的形式化分析技术 | 第13-16页 |
| 第3章 安全协议转换原理 | 第16-25页 |
| ·Blanchet演算 | 第16-17页 |
| ·Java语言 | 第17-18页 |
| ·语言解析器 | 第18页 |
| ·安全协议代码的验证安全的可实施性 | 第18-20页 |
| ·Java与Blanchet演算语言映射 | 第20-25页 |
| ·语言转化 | 第21页 |
| ·类型转换 | 第21-22页 |
| ·函数转换 | 第22-23页 |
| ·秘密性声明 | 第23页 |
| ·通道声明 | 第23-24页 |
| ·安全属性 | 第24页 |
| ·发送进程和接收进程 | 第24页 |
| ·主进程 | 第24-25页 |
| 第4章 自动转换软件CV2JAVA开发过程 | 第25-38页 |
| ·Lexical analyzer词法分析器的开发 | 第27-28页 |
| ·Parser解析器的开发 | 第28-29页 |
| ·Simplifier语法树简化器 | 第29-31页 |
| ·Translator翻译器开发 | 第31-35页 |
| ·Code generator代码生成器的开发 | 第35-36页 |
| ·Template模板器的开发 | 第36-38页 |
| 第5章自动转换软件CV2JAVA结果验证 | 第38-45页 |
| 总结 | 第45-46页 |
| 参考文献 | 第46-49页 |
| 致谢 | 第49-50页 |
| 附录 攻读学位所发表的学术论文目录 | 第50页 |