Design and verification of WM protocol for Electronic Commerce Transactions

Nowadays, much of commerce is taking place in the electronic world. E-commerce transactions take place mainly in three forms: C2C (customer to customer), B2B (Business to business), and B2C (business to customer). Out of these forms, B2C type of e-commerce is the most important one. Therefore, there is a need for a secure protocol to perform the B2C type of e-commerce transactions. In the case pf B2C type, the main participating entities are customers, websites, and merchants. In this paper, the communication between website and merchant was represented by WM protocol. The design of WM protocol must consider several issues such as problem definition, services, environment, vocabulary, and message formats. The verification of WM protocol was also performed with respect to the protocol procedure rules based on linear temporal logic. The procedure rules related to the protocol were specified in process meta language. Verification was performed using SPIN model checker and the corresponding results were reported.