基于分层时间有色Petri网的支付协议公平性分析

电子支付协议是一种重要的电子商务协议，公平性是其重要的安全属性之一。该文提出一种基于分层时间有色Petri网(HTCPN)的电子支付协议形式化分析方法。该方法在进行公平性分析时，充分考虑了两个环境因素:主体是否诚实和通信信道是否可靠，与其他形式化方法相比，可以更有效地分析协议公平性。使用该方法对典型支付协议IBS协议进行分析，分析结果验证了所提模型和方法的有效性。

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.