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

A FORMAL ANALYSIS METHOD FOR SECURITY PROTOCOLS INCLUDING TIME FACTORS

作　　者：范玉涛[1] 苏桂平[2] 

机构地区：[1]华北科技学院计算机学院,北京101601 [2]中国科学院研究生院信息科学与工程学院,北京100049

出　　处：《计算机应用与软件》2013年第1期315-318,共4页Computer Applications and Software

基　　金：中国科学院研究生院院长基金项目(Y15102HN00)

摘　　要：提出一种针对包含时间因素的安全协议的有色Petri(CPN)形式化分析方法,利用CPN Tools中的内置全局自动时钟标记,时间相关性质可通过仿真和生成状态图进行分析验证。基于这一方法,对著名的NS协议(简化版)建模,来分析验证与时间相关的安全属性。然后利用CPN Tools,采用CPN ML语言编写查询函数验证协议的AUT性质,从而发现协议的漏洞。应用分析结果表明方法有效,且操作简单容易理解。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.

关 键 词：形式化分析CPN 时间因素 安全协议 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]