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

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

作　　者：刘文琦[1] 顾宏[1] 

机构地区：[1]大连理工大学电信学院,大连116023

出　　处：《电子与信息学报》2009年第6期1445-1450,共6页Journal of Electronics & Information Technology

基　　金：国家973规划项目(2002CB312201)资助课题

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

关 键 词：有色Petri网(CPN) 支付协议 公平性 可追究性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]