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

• 作者: 苏桂平 范玉涛
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 形式化分析 CPN 时间因素 安全协议
• 年，卷（期）: 2013,（1）
• 所属期刊栏目: 安全技术
• 页码范围: 315-318
• 页数: 4页
• 分类号: TP393
• 字数: 3461字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2013.01.081

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏桂平	中国科学院研究生院信息科学与工程学院	24	238	8.0	15.0
2	范玉涛	华北科技学院计算机学院	8	34	3.0	5.0