密码协议安全性分析是网络安全的一个难题,运用形式化方法对密码协议进行分析一直是该领域的研究热点.形式化分析由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,该文主要研究了基于时延Petri网的密码协议分析和评估方法.作者所取得的主要研究结果如下:(1)对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点.(2)首次提出用时延Petri网作为工具来分析和评估密码协议,并且给出了用它分析和评估密码协议的具体方法和步骤.该方法不但能够反映协议的结构特性和动态特性,而且能够对密码协议进行时间、空间上的性能评估.(3)给出了时延Petri网的引发规则、时间可达图定义和构造算法,并且介绍了时延Petri网的两个基本分析方法:时间可达图(或可覆盖图)和状态方程.(4)用时延Petri网对MSR协议、Aziz-Diffle协议和TMN协议进行了具体和详细的分析,给出了这三种协议的发生序列(执行剧情)和攻击者对这三种协议的详细攻击剧情,并且对Aziz-Diffle协议给出了一个改进方案.(5)该文对这三种密码协议的执行时间、结构特性以及实现分析的软件复杂度给出了客观的评估.最后,该文建立了实现自动化分析密码协议工具—时延Petri网分析器的结构框架.