A General Model Checking Method of Electronic Transaction Protocols Using Colored Petri Nets
As a special kind of security protocol, E-Commerce protocols have been analyzed with many formal methods in recent years. However, there is no general specification and verification model checking method to be applied effectively to the four special properties in E-Commerce protocols--nonrepudiation, accountability, fairness, and timeliness. Based on our previous work on the suitability of Colored Petri Nets(CPNs) to the formal analysis of timeliness, this paper concentrates on the formal modeling and analysis of the other three properties using CPNs. Combined with Petri net reduction methods and random numbers as time factors and keys, we describe and analyze both online Trusted Third Party (TTP) and offline TTP protocols, discover their flaws which could not be found by many other formal methods, proving that our methods are more general and suitable for nearly all the E-Commerce protocols.
model checking Colored Petri Nets E-Commerce
Meng Xu Guiping Su Jin Wei
School of Information Science and Engineering Graduate University of Chinese Academy of Sciences Beijing, China
国际会议
2009 Ninth International Conference on Hybrid Intelligent Systems(第九届混合智能系统国际会议 HIS 2009)
沈阳
英文
1-6
2009-08-12（万方平台首次上网日期，不代表论文的发表时间）