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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社