随着计算机网络通信的迅猛发展，安全协议的重要性越来越得到重视。安全协议负责密钥分发和身份认证，一旦其自身出现漏洞，那么将会对通信的安全造成威胁。模型检验方法在对安全协议的验证中体现出了巨大的优越性。 本课题的研究目的是采用模型检验工具对安全协议进行验证。本文研究了验证安全协议的各种形式化方法，详细研究了符号化模型检验工具SMV的工作机制；确定了使用SMV作为工具对安全协议进行模型检验，验证了认证版Needham-Schroeder公钥协议和Woo and Lam Π对称钥协议。 通过使用SMV对Needham-Schroeder公钥协议进行建模和验证，理解了符号化模型检验和小系统模型的原理，并发现了一个协议漏洞，该漏洞与Gavin Lowe用FDR所发现的相一致。 为了突破小系统模型的局限性，我们使用SMV验证Woo and Lam Ⅱ对称钥协议时，建立了允许诚实的通信实体运行两次协议的模型，在这个模型上发现了一个已知的协议漏洞，攻击者利用诚实通信实体的两次运行，成功地进行了攻击。 在对SMV的大量使用中，我们发现了SMV的一个bug和其产品说明书中所忽略的一些值得注意的问题。 文章主要介绍了安全协议的概念、分类和性质，安全协议的形式化验证方法，以及小系统模型的原理；重点分析和研究了符号化模型检验工具SMV的原理和语法及其对安全协议进行模型检验时的工作机理，而且使用SMV对Needham-Schroeder公钥协议和Woo and Lam Π对称钥协议进行了形式化建模与模型检验，发现了它们的安全漏洞。