密码协议的安全性分析对于保障计算机网络的安全通信具有重要意义。运用形式化方法对密码协议进行分析一直是该领域的研究热点。目前密码协议的形式分析方法包括:逻辑方法、模型检测方法、定理证明方法和Petri网方法等,这些方法各自有它们的优点和缺点。本文主要针对Petri网方法在密码协议分析中存在的一些不足,研究将Petri网方法和模型检测方法的一些理论成果结合起来对密码协议进行分析,取得了如下结果: 1.提出将运行模式法和Petri网建模结合起来分析密码协议的思想,给出了协议运行模式的基础Petri网模型和攻击Petri网模型的概念,并阐述了两者与密码协议分析之间的关系。 2.给出协议运行模式的基础Petri网模型和攻击Petri网模型的构造方法,在此基础上给出密码协议分析的具体步骤。 3.具体对Needham—Schroeder公钥协议,Helsinki协议以及TMN协议进行了分析,并对密码协议的一类攻击的特点做出了概括。 本文工作的特点是: 1.利用协议的运行模式来指导Petri网建模,这使得我们的方法与一般Petri网方法分析密码协议的思路有所不同。 2.以一个协议的两个实例并行运行时可能存在的攻击为例,探讨了多个实例并行运行情况下的协议安全问题。