网络安全协议形式化分析技术研究.pdf

硕士学位论文蚤簧它手抖较戈誊⋯⋯§熙趣．：删峨．蛆№魍怼题小⒂⑽睦圜终塞全协这形式纯分析攮本研究一王堇玲⋯⋯指导教师姓名、职务⋯杨潼．熬援⋯～一萋萋学⋯一学科、专业⋯⋯⋯蜜碣学⋯⋯⋯⋯一⋯⋯⋯⋯三零零六年隆⋯作者姓名学科门类提交论文日期⋯⋯⋯⋯．§蝦．玪琛．￡鱼№旦ゝ⋯⋯⋯⋯⋯⋯⋯代号分类号学号⋯鲫密级⋯～金开摘要安全协议的安全性是网络安全的重要基础运用形式化方法分析安全协议已成为目前研究的主要热点。本文主要研究运用形式化方法分析安全协议的理论与技术对基于模型检测技术的运行模式分析法进行深入的研究并把其扩展到公平交换协议的分析与设计中去。主要的研究成果如下：樯馨踩榈谋尘凹盎靖拍睢⒀芯拷购头⒄骨魇疲攀隽税踩议的分类和安全协议的形式化分析方法的三种思路；樯芰椒胶腿桨踩榈脑诵心Ｊ椒治龇ǎ杓撇⑻岢隽肆椒嚼止酃平交换协议运行模式分析法；褂迷诵心Ｊ椒治龇ǔ晒Ψ治隽思父龅缱由涛裥椋鐂协议、的电子合同协议、缱佑始椋玫搅私虾玫慕崧郏莨浇换恍榈奶氐悖岢隽斯浇换恍榈纳杓圃颍⑸杓屏一个安全的电子合同签署协议；关键词：安全协议模型检测形式化分析方法运行模式分析法公平交换协议詎猰蛅謉鄋．’猰．．订琫也猵仃『。瓺：鞘．艘城尘堇硷日期丝生塑田日期逊廖宀萤垒显殓日期麴荒紹堕关于论文使用授权的说明独创性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知除了文中特别加以标注和致谢中所罗列的内容以外议文中不包含其他人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若不实之处本人承担一切相关责任。本人签名：本人完全了解硬安电子科技大学有关保留和使用学位论文的规定即：研究生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕业离校后发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。学校有权保留送交论文的复印件允许查阅和借阅论文；学校可以公布论文中的全部或部分内容可以允许采用影印、缩印或其它复制手段保存论文。Ｃ艿穆畚在解密后遵守此规定导师签名：第一章绪论从年玻甋协议的诞生算起安全协议的发展已经历经余安全协议的背景及其基本概念本章简要地介绍了安全协议的背景及其基本概念讨论了安全协议的安全性概述了安全协议形式化分析方法的研究成果重点介绍了模型检测技术的研究成果及发展趋势最后给出了本文的内容安排并列举了本文的主要研究工作。在一个分布式的互连网网络环境中人们通过安全协议来具体实现安全共享网络资源的需求。在理解安全协议这～概念之前首先要了解什么是协议。所谓协议緇褪橇礁龌蛄礁鲆陨系牟斡胝呶M瓿赡诚钐囟ǖ娜挝穸扇的一系列步骤。这个定义包含三层含义：第～协议自始至终是有序的过程每一步骤都必须一次执行。在前一步没有执行完之前后面的步骤不可能执行。第二协议至少需要两个参与者。一个人可以通过执行一系列的步骤来完成某项任务但它不构成协议。第三通过执行协议必须完成某项任务。即使某些东西看似协议但没有完成任何任务也不能成为协议只不过是浪费时间的空操作。由上可见协议与算法的概念是不尽相同的。算法应用于协议中消息处理的环节。对消息不同的处理方式则要求不同的算法而对算法的具体化则可定义出不同的协议类型。因此可以简单地说安全协议就是在消息处理环节采用了若干密码算法的协议。由此可见密码算法和安全协议处于网络安全体系的不同层次是网络数据安全的两个主要内容。应用于计算机网络的安全协议始于年甅．蚆．⒈的甋现ば椤简称认证协议Ｐ矶喙惴菏褂玫娜现ば槎是以猻槲@侗径杓频摹榭煞治6猿泼苈胩逯坪头嵌称密码体制下的两种版本分别简称为协议和协议。这些早期的经典安全协议是安全协议分析的“试验床”．亦即每当出现一个新的形式化分析方法都要先分析这几个安全协议验证新方法的有效性。同时学者们也经常以它们为例说明安全协议的设计原则和各种不同分析方法的特点。年了。在网络通信中最常用的、最基本的安全协议按照其目的可以分成以下四类【：茉拷换恍这类协议用于完成会话