基于StrandSpace模型的安全协议形式化分析研究.pdf

西南交通大学硕士学位论文基于StrandSpace模型的安全协议形式化分析研究姓名：程娜申请学位级别：硕士专业：密码学指导教师：何大可20060501摘要随着网络的普及以及电子商务和电子政务的蓬勃兴起网络安全问题曰显突出。安全协议作为解决安全问题最行之有效的方法也就变得越来越重要。然而在复杂的网络环境中要确保安全协议的正确睦却是件很难解决的问题它已成为一项重要的研究课题。年来为了应对这一挑战科学家们在安全协议分析这一领域投入了大量的精力。在已有的理论和方法中本文深入研究了譨砺郏⒂酶美砺鄯治隽巳舾尚椋甀支付协议。将辒砺墼擞玫降缱由涛裥楣叫缘姆治Ｐ停还叫裕淮矶嘀厍┟西南交通大学硕士研究生学位论文第形式化分析方法的成果较为突出。在各种形式化分析方法中被普遍认为最有前景的晶新研究成果是由琀虶氯颂岢龅腟汀Ｐ汀Ｋ浞治樟饲人的研究成果使用一种节点问存在因果关系的有向图来表示协议中主体、入侵者的动作序列利用证明的方法推导协议的正确性可以防止状态空间爆炸。它是一种直观、简洁、严格、有效的形式化分析方法。甕协议。建立了榈膕Ｐ停⒔辛深入的讨论；恢执淠Ｐ偷娜现ば椤＝⒘烁眯榈腟Ｐ停ü分析发现协议存在漏洞并构造出了一种攻击方法最后针对漏洞对协议进行了改进；中得到了与其他分析方法一致的结果。此外本文在基础理论部分对代理多重签名进行了研究提出了一种增强的代理多重签名方案。关键词：安全协议；形式化分析；脚秂琭皿肌西南交通大学硕士研究生学位论文第页研。止肌籲蜘肌锄譫甕她％鑤；印蛆叨唱甀盯出”瑆騡’．癷瑆。瑆猄琀．琲打打；瓵妯鰀甀騛瑆猻騪西南交通大学硕士研究生学位论文第籉：；第滦髀研究背景各种现实世界里的组织与系统正在走进网络这个虚拟的世界使网络世界变得更加精彩；与此同时安全问题也变得日益突出、复杂解决安全问题对许多网络应用来说已是头等大事。从目前解决安全问题的方式来看安全协议是最有效的手段之一。它可以有效地解决以下一些重要的安全问题：源认证和目标认证、消息的完整性、匿名通信、抗拒绝服务、抗抵赖、授权等。另一方面．随着网络技术的飞速发展多播技术已不断走向成熟由多播应用带动的安全问题也变得更加复杂为解决这些问题也是通过一种称为群协议的安全协议来完成的。目前研究熟点之一的多主体系统中的安全主体问题在很大程度上也是依靠有效的安全协议的设计来完成的。可见安全协议是在一个分布式的互联网网络环境中人们通过安全协议来具体实现安全共享网络资源的需求。然而安全协议的设计极易出错而且十分困难即使我们只讨论安全协议中最基本的认证协议其中参加协议的主体只有两三个变换的消息只有条设计一个正确的、符合认证目标的、没有冗余的认证协议也十分困难。正如实际应用中已有的安全协议往往被证实并不如它们设计者期望的那样安全复杂而恶意的网络环境使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击从而达到破坏网络的目的。即使一个安全协议被很小心仔细地设计了并被使用了很多年仍然包含一些微妙的漏洞没有被发现。设计一个符合安全目标的协议仅仅知道系统的安全需求远远不够我们需要确保所设计的协议在系统参与的各方之间能够运行良好。因此安全协议的安全性成为网络安全的关键。考量和分析一个安全协议的安全性我们称之为安全协议的分析。二十多年来为了应对这一挑战科学家们投入了大量的精力设计开发了不同种类的研究理论与方法比如形式化方法、可证明安全理论、零知识证明理论等。西南交通大学硕士研究生学位论文第计算机网络正以惊人的速度向各个领域渗透成为各领域发展的新源泉一个十分重要的研究课题。煳论文的研究意义究成果：尽薄鵅Ｗ远橹すぞ叩挠攀形式化分析就是将安全协议及其所处的环境视为一个系统运用各种正规的、模型化的、标准的、