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