Analysis of Fairness in Payment Protocols Based on Hierarchical Timed Coloured Petri Nets

Electronic payment protocol is a kind of important electronic commerce protocol, and fairness is one of the desirable secure properties payment protocols should achieve. A new approach based on Hierarchical Timed Coloured Petri Nets (HTCPN) for modeling and analyzing fairness in payment protocols is proposed in this paper. In the analysis of fairness, it takes the honesty of principals and the reliability of communication channels into consideration. Compared with other formal methods, it can analyze fairness of protocol more efficiently. By this approach, a typical payment protocol IBS is modeled and analyzed, and the analysis result can prove the availability of the proposed model and approach.