摘要
以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑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.
出处
《计算机科学》
CSCD
北大核心
2012年第3期75-78,92,共5页
Computer Science
基金
国家自然科学基金(70672041)
湖北省自然科学基金(2007ABA307)
中央高校基本科研业务费(2010MS112)资助
