基于模型检测技术对协议形式化分析的设计.pdf

《基于模型检测技术对协议形式化分析的设计.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、西安邮电大学毕业设计（论文）题目：基于模型检测技术对协议形式化分析的设计院（系）：通信与信息工程学院专业：信息安全班级：安全0804学生姓名：余伟东导师姓名：胡明娣职称：副教授起止时间：2012年1月2日至2012年6月15日毕业设计（论文）诚信声明书本人声明：本人所提交的毕业论文《基于模型检测技术对协议形式化分析的设计》是本人在指导教师指导下独立研究、写作的成果，论文中所引用他人的文献、数据、图件、资料均已明确标注；对本文的研究做出重要贡献的个人与集体，均已在文中以明确方式注明并表示感谢。本人完全意识到本声明

2、的法律后果由本人承担。论文作者：（签字）时间：2012年6月15日指导教师已阅：（签字）时间：2012年6月15日西安邮电大学毕业设计(论文)任务书学生姓名余伟东指导教师胡明娣职称副教授院(系)通信与信息工程学院专业信息安全题目基于模型检测技术对协议形式化分析的设计任务与要求1.学习模型检测与安全协议的基础知识。2.调研一些重要的安全协议的设计与分析方案。3.了解安全协议的有代表性的形式化分析方法,其中包括基于知识与信念推理的模态逻辑方法、基于定理证明的分析方法、Spi演算方法等，比较他们的设计方案。4.基于模

3、型检测技术对协议形式化分析设计方案。5.讨论该设计的合理性与优势。开始日期2012年1月2日完成日期2012年6月15日院长(签字)2012年1月6日西安邮电大学毕业设计(论文)工作计划2012年1月2日学生姓名__余伟东__指导教师___胡明娣___职称___副教授___院（系）__通信与信息工程学院___专业___信息安全________题目基于模型检测技术对协议形式化分析的设计________________________________________________________工作进程起止时间工

4、作内容1月2日至1月15日学习模型检测与安全协议的基础知识。1月16日至3月12日讨论基于模型检测技术对协议形式化分析方法。3月20日至4月25日设计方案。4月28日至5月12日进行实例分析。5月15日至5月20日撰写论文，完成论文初稿。5月21日至6月1日完善并修改毕业论文。6月2日至6月15日准备答辩。主要参考书目(资料)：[1]安靖.基于扩展CSP模型的安全协议分析技术研究[D].解放军信息工程大学,2006年.[2]苏开乐,吕关锋,陈清亮;基于知识结构的认证协议验证[J];中国科学E辑;2005年04期

5、[3]DoronPeled,PatrizioPelliccione,PaolaSpoletini,ModelChecking[J].WileyEncyclopediaofComputerScienceandEngineering,2009.主要仪器设备及材料：1.计算机一台。2.文献查询平台。3.VisualC++论文(设计)过程中教师的指导安排：每周指导一次，主要解答学生问题，指导研究进度，并检查阅读资料笔记与研究讨论的结论。对计划的说明：本计划为开题之初所定，后续会根据具体情况随时调整，最终一定按毕业设计规

6、定结束日期完成。西安邮电大学毕业设计(论文)开题报告通信与信息工程学院院（系）信息安全专业08级04班课题名称：基于模型检测技术对协议形式化分析的设计学生姓名：余伟东学号：06083121指导教师：胡明娣报告日期：2012年2月27日1．本课题所涉及的问题及应用现状综述涉及的问题：1.对安全协议的安全性与可靠性的重要性的分析。2.对安全协议的形式化分析进行分析。3.提出一个使用模型检测的方法来检测安全协议的可靠性的实现方案。4.对该方案的可实现性以及可用性进行分析。应用现状综述：随着网络应用的广泛覆盖，网络安全

7、越来越被关注。模型检测是一种面向有穷并发系统的自动分析验证技术，而且适用范围广速度快、充分自动化。模型检测过程只需要计算机有良好的处理能力与充足时间，就可以执行并得出结果。目前，模型检测在形式化验证领域受到广泛重视。安全协议是通讯与网络安全体系、分布式系统与电子商务的关键组成部分，是安全系统的主要保障手段与工具。由于安全协议运行在复杂的分布式网络环境中，设计出的安全协议难免会存在安全漏洞，许多安全协议在使用多年后都被发现存在很严重的安全漏洞，例如著名的Needham-Schroeder公开密钥协议在公开17年后

8、，它存在的入侵者攻击漏洞才被Lowe发现。在安全协议的设计中，任何的细微的差错都有可能导致严重的后果，并且带来不可预测的、无法挽回的、严重的损失，则对安全协议的安全性与可靠性的验证也成为了一个重要的问题。但是安全协议的设计是十分困难的，而且容易出现漏洞，这是因为对安全协议进行人工测试无法保证测试的完备性。如果使用存在漏洞的安全协议，势必会形成严重的安全威胁。则，网络安全协议的研究具有很