A General Model Checking Method of Electronic Transaction Protocols Using Colored Petri Nets

As a special kind of security protocol, ecommerce 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 ecommerce protocols--non-repudiation, 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 ecommerce protocols.