Xiao-Qi Ma and Xiao-Chun Cheng. Formal Verification of the Merchant Registration Phase of the SET Protocol. International Journal of Automation and Computing, vol. 2, no. 2, pp. 155-162, 2005. DOI: 10.1007/s11633-005-0155-5
Citation: Xiao-Qi Ma and Xiao-Chun Cheng. Formal Verification of the Merchant Registration Phase of the SET Protocol. International Journal of Automation and Computing, vol. 2, no. 2, pp. 155-162, 2005. DOI: 10.1007/s11633-005-0155-5

Formal Verification of the Merchant Registration Phase of the SET Protocol

  • This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the secrecy of online purchases. A number of concepts, notations, functions, predicates, assumptions and rules are introduced. We describe the knowledge of all legal participants, and a malicious spy, to assess the security of the sub-protocol. Avoiding search in a large state space, the method converges very quickly. We implemented our method in the Isabelle/Isar automated reasoning environment, therefore the whole verification process can be executed mechanically and efficiently.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return