基于计算模型生成密码学安全的安全协议代码

发布时间：2017-09-19 01:45

  本文关键词：基于计算模型生成密码学安全的安全协议代码

  更多相关文章： 安全性 协议实现代码 形式化分析 抽象模型 认证性

【摘要】：目前安全协议的安全性仍是学术界关注的重点,但是安全协议的安全性分析仅仅停留在对安全协议抽象分析和验证方面,很难应用于日常研究中,而且在安全协议的代码实现中难免会出现一些人为漏洞,这可能会给安全协议引入更大的漏洞。安全协议代码的一般安全性(如数组下标越界、内存泄露、类型安全等),国内外学者已经做了很多有效的工作,但是关于安全协议实现代码的研究人们做的工作很少,故本文重点关注安全协议代码的密码学安全性。安全协议的最主要的安全性分析方法有两种,一种是构造攻击下的安全性分析,另外一种是模型形式化分析。本文基于安全协议的模型形式化分析方法,由代码级出发,进而研究安全协议的安全性,也就是对安全协议代码的安全性进行研究,以得到具有更强实用性的安全协议代码。针对这些问题,本文首先对概率标号迁移系统进行研究,探索提出安全协议代码的密码学安全性模型;其次探索应用概率进程演算:Blanchet演算建模安全协议抽象规范的方法,给出安全协议抽象规范建模的模版;以Blanchet演算建立的安全协议抽象规范模型为基础,研究代码转换的可行性,并建立与Java代码之间的映射关系。本文探索从安全协议抽象规范模型生成安全协议Java代码SP[Java]的方法。从进程、角色、目标多方面来建立Blanchet演算语言的映射模型,介绍转换软件的词法分析器、语法分析器、简化器、模板器的工作原理来阐述软件的开发过程。最后开发生成安全协议Java代码的自动化转换软件工具CV2JAVA。本文最后基于计算方法的自动化证明工具Crypto Verif证明SSHV2协议的抽象模型具有认证性,同时使用自动转换软件CV2JAVA对SSHV2建立的Blanchet演算模型语言进行转换,生成SSHV2的规范流程Java核心代码。SSHV2协议生成的核心代码嵌入Java环境进行验证分析,结果表明生成的安全协议代码具有SSHV2协议定义的身份认证性。
【关键词】：安全性 协议实现代码 形式化分析 抽象模型 认证性
【学位授予单位】：中南民族大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP393.08
【目录】：

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

【相似文献】

中国期刊全文数据库 前10条

1 赵军;;基于模板的代码生成器的研究与实现[J];长春师范学院学报;2011年12期

2 张仕仁;基于可重用代码生成器设计与实现[J];山西大学学报(自然科学版);1993年03期

3 尤澜涛;;基于数据表的代码生成器的设计与实现[J];福建电脑;2013年10期

4 辛伯宇;;在RAD中实现代码自动生成[J];电脑开发与应用;2008年12期

5 朱敏;苏博;;利用VS中的宏实现VB.NET字段重构[J];武汉船舶职业技术学院学报;2006年02期

6 李榕;;基于多态变形的恶意代码技术与检测方法[J];中小企业管理与科技(下旬刊);2009年10期

7 万军民;基于Java的代码生成器的设计与实现[J];计算机工程;2004年S1期

8 王忠杰;战德臣;徐晓飞;杨美荣;程臻;;基于对象关联模型的企业应用软件代码生成器[J];计算机集成制造系统;2007年05期

9 任佳丽;曹海燕;;嵌入式软件自动代码生成和代码整合方法研究[J];太原理工大学学报;2013年04期

10 王毅;DSP/BIOS实现实时数据调试和交换[J];电子质量;2001年05期

中国重要会议论文全文数据库 前1条

1 柳桐;;基于代码再生成的Web系统架构设计[A];中国电子学会第十七届信息论学术年会论文集[C];2010年

中国重要报纸全文数据库 前1条

1 吉林 飘零雪;妙手空空制炸弹[N];电脑报;2002年

中国硕士学位论文全文数据库 前10条

1 陈君;基于Sax的XML解析工具的设计与实现[D];中国科学院大学(工程管理与信息技术学院);2015年

2 楚龙辉;基于MDL的可视化代码自动生成框架的研究与应用[D];电子科技大学;2015年

3 马杰;多核数字电路高层次综合的研究与实现[D];电子科技大学;2014年

4 李磊;C编译器中间代码生成及其后端的设计与实现[D];电子科技大学;2016年

5 牛乐园;基于计算模型生成密码学安全的安全协议代码[D];中南民族大学;2015年

6 柳桐;数据访问代码生成器的设计与实现[D];北京邮电大学;2011年

7 彭仁夔;基于关系模型的代码生成器的设计与实现[D];南昌大学;2014年

8 温衍博;基于模型驱动的电子商务系统代码生成器的研究与实现[D];国防科学技术大学;2005年

9 段雷;可选运行框架的J2EE Web应用自动生成[D];山东大学;2005年

10 张震;基于Cactus的JSP页面测试及代码自动生成器[D];北京邮电大学;2008年

，

本文编号：878762