龚翔，冯涛，杜谨泽

（兰州理工大学计算机与通信学院，甘肃 兰州 730050）

1 引言

安全协议已成为现代计算机网络正常运转的基础，但由于其设计阶段的规范缺失和不可避免的逻辑缺陷，常会带来潜在的安全隐患，使各种协议的开发和安全性验证成为一项艰巨的任务[1]。

安全协议的形式化分析一直是网络安全领域的研究热点[2-6]。丹麦奥尔胡斯大学开发的有色Petri网（CPN,colored Petri net）工具软件CPN-Tools，不仅实现了计算机上的CPN 可视化建模，还提供了全部状态空间的自动计算以及生成状态空间报告的功能，集成的SML（standard meta language）可以辅助完成各种安全协议的功能评价和状态路径搜索。

按照安全协议分析的目的，现有的CPN 协议分析目标可分为三类。第一类是对协议本身进行建模，按照状态空间报告所提供的各种属性（活性、公平性等）来判断协议的设计是否正确，验证协议的正确性[7-8]。第二类是在协议建模的基础上引入攻击者模型，构建恰当合理的安全评估模型以快速找到协议中存在的潜在威胁[9-10]。第三类在第二类的基础上更进一步，提出协议改进方案并且利用安全评估模型验证，分析改进结果[11-13]。本文着重研究通过CPN 对安全协议进行分析验证的方法，并通过实例说明该方法的有效性。

然而，由于没有统一标准，利用CPN 针对协议安全分析的方法是多种多样的[14]。近年来，有较多文献提供了不同解决方案，存在的主要问题如下。

1) 部分文献中采用了正确性验证方法验证安全协议漏洞，在引入攻击者模型后，通过建立模型的关联矩阵，用线性代数的方法判定方程是否存在解，如果有解则认为某序列可达[15-16]；……