密码学作为信息保护的手段,最早应用在军事和外交领域,随科技的发展逐渐进入人们的生活中。传统的对密码协议的建模和分析主要包括:代数模型,逻辑模型,逻辑和代数模型,代数和状态转换模型,Petri网模型等。四十多年来Petri网已经被成功的应用于一类并发,并行和异步系统的建模和分析。对具有并发,并行,异步性质的协议来说,Petri网是一个合适的模型。论文是在仔细的阅读了上面提到的Petri网分析方法的基础上提出来的。要用形式化的方法建模一个协议,我们需要建立协议主体的元素与形式化方法元素之间的关系。论文首先介绍一种利用时延Petri网对密码协议建模的方法,然后介绍一种对协议进行正确性验证和性能评估的Petri网方法。协议的正确性验证试图在协议具体实现前最大限度地检测和纠正错误和缺陷,包括死锁、活锁、错误的动作序列,接收或发送缓冲区的溢出,遗漏或重复接收报文等等。协议的性能评估主要是对协议的吞吐量和效率等指标的评价,复杂度值可以用来评估维护协议的时间和费用。论文提出一种密码协议的攻击检测方法,并用实例说明了利用该方法检测密码协议的过程。如何找到密码协议中的薄弱环节,确定不安全状态则成为该分析方法的关键。论文首先对简单的谓词/变迁系统的密码协议模型做了进一步的说明,然后分析了协议中攻击者能够获得的信息,最后通过一个简单的协议的例子对整个分析过程作了详细说明。对密码协议的攻击行为的检测是对密码协议安全性分析的一条有效途径。这样论文便对密码协议的正确性,性能评估,安全性应用Petri网方法做了分析。