密码协议是以密码学为基础以达到密钥分配与身份认证等目的的一种消息交换协议，是实现计算机网络系统安全的关键，在投入使用之前应该保证它是没有缺陷的。然而大量的事实表明，许多密码协议是存在漏洞的，甚至有些在使用多年后才被发现有漏洞。因此，协议的安全性验证是非常重要的。自Dolev和Yao在1981年首次提出了形式化方法分析密码协议以来，在该领域内涌现出了大量的形式化分析和验证方法。这些方法已经成功地发现了许多密码协议中的不安全因素，但这些方法本身仍然存着在很多问题。 密码协议的信息交换过程可以看作是一个进程，由一系列事件的集合和事件前集与后集的行为来确定。于是，密码协议可以被看成一个Petri网，用Petri网模型验证密码协议。自从该方法被提出，已经有很多文献使用此方法验证了密码协议。但是这种方法不可避免地遇到了状态空间“爆炸”问题。 本文在深入研究基于有色Petri网(CPN)模型的密码协议验证的形式化方法的基础上提出了一种更为简化的方法。这种方法首先把带入侵者的CPN模型中的一些变迁序列进行了合并，然后再进行验证。和传统方法相比，这种方法的优点主要体现在： (1)使模型在形式上变得简单了，但描述的信息量并没有减少； (2)简化了求解状态方程的过程； (3)屏蔽掉了一些具体的细节，有助于使协议的设计者从全局角度分析协议的薄弱环节。 本文最后采用这种方法对Woo-Lam协议和Denning-Sacco协议进行了验证，从而证明了这种方法的有效性。