Model checking a client-side micro payment protocol

Virtual payment systems overcome the drawbacks such as processing and operational cost of the traditional payment system. The main aim of the virtual payment system is to provide efficient services in terms of cost. Online payment using credit card is one of the most expensive of all payment means. This gives advantage to micropayment systems where only small amounts are used for e-commerce. Payment which are small will be costly if paid through credit card. Therefore, there are several micropayment systems that exist and some have been proposed. One of the proposed micropayment system that this paper will talk about is Netpay. We will do model checking to check the correctness of this payment system and to see whether the protocol designers property claim is valid. Correctness is important in payment systems because money is involved in it, therefore the protocol needs to be validated. This paper examines the client-side version of the Netpay protocol and provides its formalization as a CSP model. The PAT model checker is used to prove three properties essential for correctness: impossibility of double spending, validity of an ecoin during the execution and the absence of deadlock. We prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative. This is a very strong assumption for system built to prevent abuse, but further analysis suggests that without it the protocol does no longer guarantee all correctness properties. We compare the two variation of the protocol with each other and with the properties claimed by the protocol designers.