一种适于带时间戳安全协议的形式化分析方法

摘要：

提出了一种适用于带有时间戳的安全协议的有色Petri (CPN)形式化分析方法,利用一个非自动时钟来描述协议中涉及的时间因素.对著名的WMF协议建模,利用CPN Tools,采用CPN ML语言编写查询函数验证协议的新鲜性,从而发现协议的漏洞.应用分析结果表明该方法有效,且操作简单容易理解.

关键词：形式化分析、有色Petri网(CPN)、时间戳、安全协议

所属期刊栏目：48

分类号：TP393(计算技术、计算机技术)

资助基金：中国科学院研究生院院长基金Y15102HN00

在线出版日期：2013-01-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：116-120