Formal analysis method suitable to security protocols with timestamp

Computer Engineering and Applications ›› 2012, Vol. 48 ›› Issue (36): 116-120.

Previous Articles Next Articles

Formal analysis method suitable to security protocols with timestamp

FAN Yutao1, SU Guiping2

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

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

范玉涛1，苏桂平2

1.华北科技学院计算机系，北京燕郊 101601
2.中国科学院研究生院信息科学与工程学院，北京 100049

Abstract

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

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

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

FAN Yutao1, SU Guiping2. Formal analysis method suitable to security protocols with timestamp[J]. Computer Engineering and Applications, 2012, 48(36): 116-120.

范玉涛1，苏桂平2. 一种适于带时间戳安全协议的形式化分析方法[J]. 计算机工程与应用, 2012, 48(36): 116-120.

[1]	LI Qian1, WANG Zheng1, MA Jianfen1, LI Na2. Lightweight mobile payment protocol fairness analysis [J]. Computer Engineering and Applications, 2018, 54(19): 82-87.
[2]	MA Yuanjia1, LIU Daowei2. Improved mutual authentication with backward security for RFID protocols [J]. Computer Engineering and Applications, 2017, 53(9): 136-140.
[3]	QIN Manman, WANG Zheng, WANG Li. Formal analysis and improvement of remote attestation protocol based on the SPIN [J]. Computer Engineering and Applications, 2017, 53(1): 34-38.
[4]	YU Lei1, WEI Shimin1, ZHUO Zepeng2. Research on consistence of strand parameters for protocol principals in authentication test theory [J]. Computer Engineering and Applications, 2015, 51(13): 86-91.
[5]	YU Lei, WEI Shimin. Analysis on properties for principals’ keys on construction of test components [J]. Computer Engineering and Applications, 2013, 49(6): 114-117.
[6]	LUO Jun, WANG Hong, LI Wensheng. Research on eventual consistency of NoSQL database based on vector clocks model [J]. Computer Engineering and Applications, 2013, 49(23): 100-102.
[7]	LIU Yonglei1，2, JIN Zhigang3. Security analysis of WPS in WLAN [J]. Computer Engineering and Applications, 2013, 49(21): 87-89.
[8]	ZHANG Xiaoliang，JIN Cong，GUO Jinglei. Copyright protection scheme for determining scope of tamper person [J]. Computer Engineering and Applications, 2011, 47(5): 111-113.
[9]	QI Xin，ZHANG Chun-ming. Research of replica consistency model based on timestamp for data grids [J]. Computer Engineering and Applications, 2010, 46(4): 104-106.
[10]	LI Ting-yuan1，2，QIN Zhi-guang1，LIU Xiao-dong2，ZHANG Xuan-fang2. Formal analysis of Needham-Schroeder protocol with authentication test methods [J]. Computer Engineering and Applications, 2010, 46(19): 100-102.
[11]	ZHOU Jia-jun¹，MA Rui-xing²，WANG Feng³，LI Xiao-jian^3，4. Formal analysis and algorithmic application on weighted strategy for smart-proliferation of worm [J]. Computer Engineering and Applications, 2010, 46(13): 90-94.
[12]	PAN Xin-chun，JIN Wen-guang，ZHOU Dong-xin. On-virtual timestamp synchronization protocal for wireless sensor network [J]. Computer Engineering and Applications, 2009, 45(29): 87-90.
[13]	ZHANG Chao,HAN Ji-hong,WANG Ya-di,ZHU Yu-na. Improved first-order logic model for security protocols [J]. Computer Engineering and Applications, 2008, 44(26): 95-98.
[14]	FANG Xian-wen^1,2，XU Zhi-cai³，YIN Zhi-xiang¹. The study on data distribution management based on the Colored Petri Net and Lookahead [J]. Computer Engineering and Applications, 2007, 43(24): 97-99.
[15]	ZHAO You-jun¹，ZENG Zi-wei¹，ZANG Dian-hong². Virtual timestamp and father-burden-chain clock synchronization algorithms for WSN [J]. Computer Engineering and Applications, 2007, 43(19): 167-170.

Formal analysis method suitable to security protocols with timestamp

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics