Title
A General Model Checking Method of Electronic Transaction Protocols Using Colored Petri Nets
Abstract
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.
Year
DOI
Venue
2009
10.1109/HIS.2009.172
HIS (2)
Keywords
Field
DocType
colored petri nets,general model checking method,protocols,trusted third party protocol,e-commerce protocol,security protocol,special property,petri nets,model checking,e-commerce,electronic transaction,special kind,formal modeling,offline ttp protocol,formal analysis,third party,general specification,ecommerce protocol,electronic transaction protocol,electronic commerce,formal method,security of data,trusted third party,data mining,probability density function,petri net,e commerce,niobium,cryptography
Trusted third party,Model checking,Petri net,Cryptographic protocol,Computer science,Cryptography,Theoretical computer science,Formal methods,Database transaction,E-commerce,Distributed computing
Conference
Volume
ISBN
Citations 
2
978-0-7695-3745-0
1
PageRank 
References 
Authors
0.35
9
3
Name
Order
Citations
PageRank
Meng Xu120.73
Guiping Su2132.36
Wei Jin38325.25