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

Formal analysis method suitable to security protocols with timestamp

提出了一种适用于带有时间戳的安全协议的有色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.