A roadmap to electronic payment transaction guarantees and a Colored Petri Net model checking approach

Electronic payment systems play a vital role in modern business-to-consumer and business-to-business e-commerce. Atomicity, fault tolerance and security concerns form a problem domain of interdependent issues that are taken into account to assure the transaction guarantees of interest. We focus on the most notable payment transaction guarantees: money conservation, no double spending, goods atomicity, distributed payment atomicity, certified delivery or validated receipt and the high-level guarantees of fairness and protection of payment participants’ interests. Apart from a roadmap to the forenamed transaction guarantees, this work’s contribution is basically a full-fledged methodology for building and validating high-level protocol models and for proving payment transaction guarantees by model checking them from different participants perspectives (payer perspective, as well as payee perspective). Our approach lies on the use of Colored Petri Nets and the CPN Tools environment (i) for editing and analyzing protocol models, (ii) for proving the required transaction guarantees by CTL-based (Computation Tree Temporal Logic) model checking and (iii) for evaluating the need of candidate security requirements.