Model checking electronic commerce security protocols based on CTL
- 55 Downloads
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.
Key wordsE-commerce security protocols formal methods computational temporal logic
CLC numberTP 309
Unable to display preview. Download preview PDF.
- Lu S, Smolka S. Model Checking the Secure Electronic Transaction (SET) Protocol.http://citeseer.ist.psu.edu/332906.html. Oct 1999.Google Scholar
- Xiao De-qin.Security Technology and Application on E-Commerce. Guangzhou: Publishing House of South China Technology University, 2003, 5–6 (Ch).Google Scholar
- Emerson A.Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics. Amsterdam and Cambridge: Elsevier and MIT Press, 1990, 45–58.Google Scholar
- Xiao De-qin, Lin Pi-yuan Zhang Huan-guo,et al. Analysis Key Distribution Protocols Using Temporal Logic.Micro-Mini Computer System, 2002,23(11): 1340–1343 (Ch).Google Scholar
- Van H E. Non-Repudiation in SET: Open Issues.Proceedings of 4th Conference on Financial Cryptography 2000 (LNCS 1962), Berlin: Springer, 2000, 140–156.Google Scholar
- Kessler V, Neumann H. A Sound Logic for Analyzing Electronic Commerce Protocols.Computer Security-ESORICS' 98 5th European Symposium on Research in Computer Security (LNCS 1485). New York: Springer, 1998, 345–360.Google Scholar
- Bella G, Massacci F, Paulson L,et al. Formal Verification of Cardholder Registration in SET.Proceedings of the 6th European Symposium on Research in Computer Security (ESORICS). Toulouse: Springer, 2000, 159–174.Google Scholar