计算机应用与软件2013，Vol.30Issue(1)：315-318,4.DOI:10.3969/j.issn.1000-386x.2013.01.081
一种含时间因素的安全协议形式化分析方法
A FORMAL ANALYSIS METHOD FOR SECURITY PROTOCOLS INCLUDING TIME FACTORS
摘要
Abstract
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/时间因素/安全协议Key words
Formal analysis/Coloured Petri net/Time factors/Security protocols分类
信息技术与安全科学引用本文复制引用
范玉涛,苏桂平..一种含时间因素的安全协议形式化分析方法[J].计算机应用与软件,2013,30(1):315-318,4.基金项目
中国科学院研究生院院长基金项目(Y15102HN00) （Y15102HN00）
