一种含时间因素的安全协议形式化分析方法

摘要

In this paper, we propose a colour Petri net (CPN) formal analysis method specifically for security protocols including time factors. This method uses a general auto-clock mark embedded in the CPN Tools, and the attributes related to time can be verified through emulation and state diagrams generation. Based on this method, we model the famous NS protocol (simplified) and verify the security attributes related to time. Then using CPN Tools, we program query functions for verifying the AUT character in CPN ML so that the flaws of the protocol can be found. Analysis results show that the method is effective and easy to operate and understand.%提出一种针对包含时间因素的安全协议的有色Petri (CPN)形式化分析方法,利用CPN Tools中的内置全局自动时钟标记,时间相关性质可通过仿真和生成状态图进行分析验证.基于这一方法,对著名的NS协议(简化版)建模,来分析验证与时间相关的安全属性.然后利用CPN Tools,采用CPN ML语言编写查询函数验证协议的AUT性质,从而发现协议的漏洞.应用分析结果表明方法有效,且操作简单容易理解.