【作者】 程娜；

【导师】 何大可；

【作者基本信息】 西南交通大学 ， 密码学， 2006， 硕士

【摘要】 随着网络的普及以及电子商务和电子政务的蓬勃兴起，网络安全问题日显突出。安全协议，作为解决安全问题最行之有效的方法，也就变得越来越重要。然而，在复杂的网络环境中，要确保安全协议的正确性却是件很难解决的问题，它已成为一项重要的研究课题。20年来，为了应对这一挑战，科学家们在安全协议分析这一领域投入了大量的精力。在已有的理论和方法中，形式化分析方法的成果较为突出。 在各种形式化分析方法中，被普遍认为最有前景的最新研究成果是由Fabrega，Herzog和Guttman三人提出的Strand Space模型。它充分吸收了前人的研究成果，使用一种节点间存在因果关系的有向图来表示协议中主体、入侵者的动作序列，利用证明的方法推导协议的正确性，可以防止状态空间爆炸。它是一种直观、简洁、严格、有效的形式化分析方法。 本文深入研究了Strand Space理论，并用该理论分析了若干协议： 1．Yahalom协议。建立了Yahalom协议的Strand Space模型，并进行了深入的讨论； 2．一种传输模型的认证协议。建立了该协议的Strand Space模型，通过分析，发现协议存在漏洞，并构造出了一种攻击方法，最后针对漏洞对协议进行了改进； 3．ISI支付协议。将Strand Space理论运用到电子商务协议公平性的分析中，得到了与其他分析方法一致的结果。 此外，本文在基础理论部分对代理多重签名进行了研究，提出了一种增强的代理多重签名方案。更多还原

【Abstract】 With the popularization of network and Internet applications, security issues are becoming more and more important. Accordingly, security protocol, the most effective way to solve security issues, is of the same importance. But it is not an easy work to ensure the validity of security protocol in the sophisticated network environment, which has become an important research subject. Great efforts have been made by scientists to meet this challenge during the past 20 years, which in a sense shows the difficulty of security protocols analysis. Among all existing theories and methods, formal analysis is an outstanding one.The updated research fruit--Strand Space Model (SSM) brought forward by Fabrega, Herzog and Guttman is of the best prospect among varieties of formal analysis methods at large. It fully absorbs former researching results and uses a kind of order graph between its nodes existing casual relationship to demonstrate the action sequence of main body and intruder of the protocol and deduce the validity of the protocol by means of certification. It can prevent the bursting of status space and is practical, intuitive and strict for formal analysis of security protocol.This paper does a further study on the SSM, and then analyses numbers of security protocols based on it as follows:1. Yahalom protocolEstablish the SSM of Yahalom protocol and conduct the further discussion;2. A kind of authentication protocol based on a transmission modelWith SSM, we find out its dropper and create a new attack on this protocol and make some improvement;3. ISI payment protocolWe apply the SSM to the analysis of fairness of E-business protocol. Additionally, we study on proxy multi-signature scheme in basic theory and present a strengthened proxy multi-signature scheme.更多还原