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

Formal analysis method suitable to security protocols with timestamp

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

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

出　　处：《计算机工程与应用》2012年第36期116-120,共5页Computer Engineering and Applications

基　　金：中国科学院研究生院院长基金(No.Y15102HN00)

摘　　要：提出了一种适用于带有时间戳的安全协议的有色Petr(iCPN)形式化分析方法,利用一个非自动时钟来描述协议中涉及的时间因素。对著名的WMF协议建模,利用CPN Tools,采用CPNML语言编写查询函数验证协议的新鲜性,从而发现协议的漏洞。应用分析结果表明该方法有效,且操作简单容易理解。This paper proposes a formal analysis method suitable to security protocols with timestamp. This method uses a non-auto clock to describe time factors involved in security protocols. Based on this method, it models for the famous WMF protocol. Under the CPN Tools, it programs query functions for verifying the freshness character in CPN so that flaws of the protocol can be found. Analysis results show that the method is efficient and easy to operate and understand.

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

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