《形式化验证安全协议Java代码的安全性》由会员分享，可在线阅读，更多相关《形式化验证安全协议Java代码的安全性（104页珍藏版）》请在金锄头文库上搜索。
1、形式化验证安全协议Java代码的安全性 学校代号 10524 学 号 12009499 分 类 号 密 级 硕士学位论文 形式化验证安全协议Java 代码的安全性 学位申请人姓名 汪 卫 培 养 单 位 计算机科学学院 导师姓名及职称 孟 博 副教授 学 科 专 业 计算机应用技术 研 究 方 向 信息安全 论文提交日期 2012 年5 月9 日 学校代号：10524 学 号：12009499 密 级： 中南民族大学硕士学位论文 形式化验证安全协议Java 代码的安全性 学位申请人姓名： 汪 卫 导师姓名及职称： 孟 博 副教授 培 养 单 位： 计算机科学学院 专 业 名 称： 计算机应用技
2、术 论文提交日期： 2012 年5 月9 日 论文答辩日期： 2012 年5 月19 日 答辩委员会主席： 李元香 教授 Formal verification of security protocols implementation by Java by WANG Wei B.E. South-Central University for Nationalities 2007 A thesis submitted in partial satisfaction of the Requirements for the degree of Master of Engineering in Com
3、puter Science and Technology in the Graduate School of South-Central University for Nationalities Supervisor Associate Professor Meng Bo May ，2012 中南民族大学 学位论文原创性声明 本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所取 得的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任何其 他个人或集体已经发表或撰写的成果作品。对本文的研究做出重要贡献的个 人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律后果 由本
4、人承担。 作者签名： 日期： 年 月 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学 校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查 阅和借阅。本人授权中南民族大学可以将本学位论文的全部或部分内容编入 有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本 学位论文。 本学位论文属于 1、保密，在_年解密后适用本授权书。 2 、不保密。 （请在以上相应方框内打“” ） 作者签名： 日期： 年 月 日 导师签名： 日期： 年 月 日 中南民族大学硕士学位论文 目 录 摘要. I Abstract .II 第1 章 绪论. 1 1.1 国内外研究现状. 1 1.2 本文组织结构. 2 第2 章 安全协议的形式化分析验证. 3 2.1 安全协议进行形式化分析的必要性. 3 2.2 形式化分析方法. 4 2.3 安全协议形式化验证. 7 2.4 本章小结. 9 第3 章 Java 语言的形式化描述. 10 3.1 程序形式化. 10 恒等式.11 静态绑定方法调用.11 创建对象. 12 使用对象. 12 申明子类. 13 3.2 Java 程序映射. 13
