随着计算机网络的广泛应用，计算机网络的安全问题也日益引起人们的重视。在网络安全中，各种安全服务都是基于安全协议的，这使得安全协议的安全性变得尤为重要。在过去的二十多年中，为了满足各种各样的网络应用，提出了大量安全协议，但是后来的研究证明这些安全协议大多数都含有这样或者那样的安全漏洞，如何设计一个比较安全的安全协议以及如何验证一个已设计出来的安全协议是否安全成为安全协议研究领域中最重要的两方面。安全协议是一种通信协议，它的主要目的是利用密码技术实现网络通信中的密钥分发和身份认证。然而，大量事实表明，有许多安全协议经过安全专家认真仔细地分析、设计和实现后仍然存在着漏洞。本文首先介绍了以往的各种安全协议，在此基础上总结出了五种典型的安全协议漏洞。形式化方法能有效检验安全协议的安全性，BAN逻辑的发展极大地促进了这一领域的研究。本文重点阐述了形式化方法及其在安全协议验证中的应用。同时，针对串空间模型这一新兴的形式化方法进行了深入地分析和研究，在此基础上，应用串空间模型对Andrew RPC安全协议进行了形式化分析和验证，指出了该协议的安全缺陷。论文还比较了BAN逻辑和串空间模型这两种形式化方法各自的优缺点。然后，对串空间模型提出了扩展，使得它能更好地分析公平的不可否认协议，并且以ZG协议为例，用扩展理论成功地对它进行了安全性分析和验证。