计算机工程与应用 ›› 2012, Vol. 48 ›› Issue (36): 116-120.

• 网络、通信、安全 • 上一篇    下一篇

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

范玉涛1,苏桂平2   

  1. 1.华北科技学院 计算机系,北京 燕郊 101601
    2.中国科学院研究生院 信息科学与工程学院,北京 100049
  • 出版日期:2012-12-21 发布日期:2012-12-21

Formal analysis method suitable to security protocols with timestamp

FAN Yutao1, SU Guiping2   

  1. 1.Department of Computer Science, North China Institute of Science & Technology, Yanjiao, Beijing 101601, China
    2.School of Information Science and Engineering, Graduate University of the Chinese Academy of Sciences, Beijing 100049, China
  • Online:2012-12-21 Published:2012-12-21

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

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

Abstract: 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.

Key words: formal analysis, Colored Petri Net(CPN), timestamp, security protocols