基于着色Petri网仿真模型的安全协议分析

采取形式化方法验证协议的安全性，Petri网是有效的方法之一，但传统Petri网分析过程中经常会出现状态空间爆炸问题。该文采用了基于着色Petri网建立安全协议及入侵者攻击的仿真模型方法，从而获得仿真数据。该方法利用逆向状态分析和Petri网可达性分析，能有效地发现协议中的安全漏洞。并且，如果能恰当地控制好状态空间，则能有效地克服Petri网分析过程中的状态空间爆炸问题。该文给出的利用着色Petri网建立安全协议仿真模型分析的一般方法，实例说明该方法具有普适性，并且方便利用Petri网自动化分析工具实现自动化分析。

The Analysis of Secure Protocols Based on Coloured Petri Nets Simulation Model

Using the formalized method to validate the safety of the protocol, Petri nets is one of these valid methods. But in the process of conventional petri nets analysis, the problem of state space explosion of ten occurs. This paper proposed a modeling and simulation approach for secure protocol and attacked protocol by intruders based on colored petri nets to get simulation data. The methodology is based on the idea of backward state analysis and the reachability analysis for Petri nets. By using this method, the insecure problems can be found effectively. And if state space is rightly controlled , the problem of state space explosion in the process of Petri nets analysis can be a-voided. This paper gives a normal method to validate secure protocol using colored Petri nets simulation model. The example in the paper shows that the method is applicable universally. And the method will easily realize automatic a-nalysis by using Petri nets tools for analysis.