Model checking electronic commerce security protocols based on CTL
Xiao De-qin, Huanguo Zhang · Wuhan University Journal of Natural Sciences · 2005
We present a model based on Computational Temporal Logic (CTL) methods for verifying security requirements of electronic commerce protocols. The model describes formally the authentication, confidentiality integrity, non-repudiation, denial of service and access control of the electronic commerce protocols. We illustrate as case study a variant of the Lu-Smolka protocol proposed by Lu-Smolka. Moreover, we have discovered two attacks that allow a dishonest user to purchase a good debiting the amount to another user. And also, we compared our work with relative research works and found that the formal way of this paper is more general to specify security protocols for E-Commerce.