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

Formal modeling and security analysis method of security protocol based on CPN

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

To solve the problem of modeling and analyzing with colored Petri net(CPN),which was determining vulnerabilities in hole location but couldn’t identify any attack path,and the problem of when the introduction of the attacker model,the number of possible message paths in the CPN formal model of security protocol surges the state space prone to explosion,which made it difficult to extract accurate attack paths,the formal modeling method of security protocol was improved base on CPN,the attack paths were verified and extracted,further the fine-grained protocol modeling and control were adopted.As well as in the aspect of state-space convergence,and a waiting-sync method for different processes of CPN model in each hierarchy model was proposed,which effectively controlled the state-space scale of the model.Through the security evaluation and analysis of TMN protocol,25 attack paths of the protocol are extracted successfully,the security of the protocol is evaluated,and the effectiveness of the proposed method is proved.