基于CPN的安全协议形式化建模及安全分析方法

摘要

为了解决有色Petri网(CPN)对安全协议进行形式化建模分析时,仅能判断协议是否存在漏洞而无法找出漏洞具体位置和攻击路径的问题,以及CPN建模时随着攻击者模型引入,安全协议的形式化模型可能的消息路径数量激增,状态空间容易发生爆炸导致难以提取准确攻击路径的问题,改进了基于CPN的安全协议形式化建模方法,验证并提取攻击路径的同时,采用更细粒度的协议建模及控制.在状态空间收敛方面提出了CPN模型不同进程在各分层模型中等待?同步的方法控制状态空间规模.通过针对TMN协议的安全评估分析,成功提取出该协议25条攻击路径,评估了该协议安全性的同时证明了所述方法的有效性.