电子支付协议可追究性的Petri网建模与分析  

Modeling and Analysis Method of Accountability in Payment Protocols Based on Petri Nets

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

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

出　　处：《系统仿真学报》2008年第20期5600-5604,5609,共6页Journal of System Simulation

摘　　要：可追究性是电子支付协议必须满足的安全属性之一,针对电子支付协议,建立了支持支付协议可追究性分析的分层有色Petri网模型,并基于此提出一种对支付协议可追究性分析的一般性方法。Kungpisdan等人曾提出一种可追究性逻辑,证明一个典型的移动支付协议KSL协议满足可追究性。但使用上述所提方法对该协议建模并进行可追究性分析,发现了可追究性逻辑未发现的漏洞,分析例证结果表明了所提方法的有效性。Accountability is one of the desirable secure properties which electronic payment protocols should achieve. Firstly,a modeling approach based on Hierarchical Coloured Petri nets （HCPN） for supporting accountability analysis was proposed. Then,the analyzing approach for the accountability in payment protocols based on the above payment protocol model was proposed. Lastly,the proposed approach was used to analyze the accountability in KSL protocol,which is a typical mobile payment protocol. Kungpisdan,et al. proposed a kind of accountability logic to analyze the accountability in KSL protocol and they proved the protocol achieved accountability. But the protocol does not satisfy the accountability requirement and there are some leaks in the protocol which are not found by the logic. By analyzing the result of the exemplification,the availability of the new approach could be proven.

关 键 词：PETRI NETS CPN 可追究性 电子支付协议 电子商务 

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