基于四方的安全电子商务支付协议分析与验证  

Analysis and Verification of Secure E-commerce Payment Protocol Based on Four Parties

作　　者：肖仕成[1] 李开[1] 甘早斌[1] 

机构地区：[1]华中科技大学计算机学院,武汉430074

出　　处：《计算机科学》2012年第3期75-78,92,共5页Computer Science

基　　金：国家自然科学基金(70672041);湖北省自然科学基金(2007ABA307);中央高校基本科研业务费(2010MS112)资助

摘　　要：以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑CTL公式,利用符号模型检测工具SMV对协议的原子性进行检测验证。验证结果证明,基于四方的安全电子商务支付协议满足电子支付的金钱原子性、商品原子性以及确认发送原子性,协议符合电子支付的原子性安全要求。Both the finite state model and the CTL （Computation Tree Logic） formulations were first constructed for the secure e-commerce payment protocol based on four parties （FSET） in this paper. Then, the symbolic model checking （SMV） was used to analyze and verify the atomicity of the FSET protocol. The result of analysis and verification indicates that the FSET can meet with the money atomieity, the goods atomicity and the certified delivery, as well as the electronic payment security requirements.

关 键 词：电子商务支付协议 模型检测 SMV 原子性 

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