| 基于四方的安全电子商务支付协议分析与验证 |
| |
| 引用本文： | 肖仕成,李开,甘早斌. 基于四方的安全电子商务支付协议分析与验证[J]. 计算机科学, 2012, 39(3): 75-78 |
| |
| 作者姓名： | 肖仕成 李开 甘早斌 |
| |
| 作者单位： | (华中科技大学计算机学院 武汉430074) |
| |
| 基金项目： | 国家自然科学基金(70672041);湖北省自然科学基金(2007ABA307);中央高校基本科研业务费(2010MS112)资助 |
| |
| 摘 要： | 以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑CTL公式,利用符号模型检测工具SMV对协议的原子性进行检测验证。验证结果证明,基于四方的安全电子商务支付协议满足电子支付的金钱原子性、商品原子性以及确认发送原子性,协议符合电子支付的原子性安全要求。
|
| 关 键 词： | 电子商务支付协议 模型检测 SMV 原子性 |
Analysis and Verification of Secure E-commerce Payment Protocol Based on Four Parties |
| |
| XIAO Shi-cheng LI Kai GAN Zao-bin. Analysis and Verification of Secure E-commerce Payment Protocol Based on Four Parties[J]. Computer Science, 2012, 39(3): 75-78 |
| |
| Authors: | XIAO Shi-cheng LI Kai GAN Zao-bin |
| |
| Affiliation: | XIAO Shi-cheng LI Kai GAN Zao-bin(School of Computer Science and Technology,Huazhong University of Science and Technology,Wuhan 430074,China) |
| |
| Abstract: | 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 (FSE7)in this paper. Then, the symbolic model checking (SMV) was used to analyze and verify the atomicity of the FSET protocol. I}he result of analysis and verification indicafes that the FSET can meet with the money atomicity, the goods atomicity and the certified delivery, as well as the elegy tromc payment security requmements. |
| |
| Keywords: | E-commerce payment protocol Model checking SMV Atomicity |
| 本文献已被 CNKI 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
