Wuhan University Journal of Natural Sciences

, Volume 10, Issue 1, pp 333–337 | Cite as

Model checking electronic commerce security protocols based on CTL

  • Xiao De-qin
  • Zhang Huan-guo
Information Security Techology and Application


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 words

E-commerce security protocols formal methods computational temporal logic 

CLC number

TP 309 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Lu S, Smolka S. Model Checking the Secure Electronic Transaction (SET) Protocol. Oct 1999.Google Scholar
  2. [2]
    Xiao De-qin.Security Technology and Application on E-Commerce. Guangzhou: Publishing House of South China Technology University, 2003, 5–6 (Ch).Google Scholar
  3. [3]
    Meadows C, Syverson P. A Formal Specification of Requirements for Payment Transactions in the SET Protocol.Proceedings of the 2nd Financial Cryptography. Anguilla: Springer, 1998, 122–140.CrossRefGoogle Scholar
  4. [4]
    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
  5. [5]
    Xiao De-qin, Zhou Quan, Zhang Huan-guo,et al. Analyzing Encryption Protocols Based on Temporal Logic.Chinese Journal of Computers, 2002,25(10): 1083–1089 (Ch).MathSciNetGoogle Scholar
  6. [6]
    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
  7. [7]
    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
  8. [8]
    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
  9. [9]
    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
  10. [10]
    Bolignano D. Towards the Formal Verification of Electronic Commerce Protocols.Proceedings of 10 th Computer Security Foundations Workshop. New York: IEEE Computer Society Press, 1997, 133–146.CrossRefGoogle Scholar

Copyright information

© Springer 2005

Authors and Affiliations

  • Xiao De-qin
    • 1
    • 2
  • Zhang Huan-guo
    • 2
  1. 1.College of InformationSouth China Agriculture UniversityGuangzhou, GuangdongChina
  2. 2.State Key Laboratory of Software EngeeringWuhan UniversityWuhan, HubeiChina

Personalised recommendations