| 移动支付协议PCMS的形式化分析和验证 |
| |
| 引用本文： | 吴格格,庄雷,张坤丽,王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(1): 67-73 |
| |
| 作者姓名： | 吴格格 庄雷 张坤丽 王国卿 |
| |
| 作者单位： | ;1.郑州大学信息工程学院 |
| |
| 基金项目： | 国家973计划(2012CB315901)；国家自然科学基金(61379079)；河南省科技厅攻关项目(122102210042)；河南省科技厅基础研究项目(142300410231,142300410308) |
| |
| 摘 要： | 移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。
|
| 关 键 词： | 移动支付协议 模型检测 时间自动机 UPPAAL |
| 收稿时间： | 2015-10-26 |
| 修稿时间： | 2017-01-25 |
Formal analysis and verification of mobilepayment protocol PCMS |
| |
| WU Ge ge,ZHUANG Lei,ZHANG Kun li,WANG Guo qing. Formal analysis and verification of mobilepayment protocol PCMS[J]. Computer Engineering & Science, 2017, 39(1): 67-73 |
| |
| Authors: | WU Ge ge ZHUANG Lei ZHANG Kun li WANG Guo qing |
| |
| Affiliation: | （School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China） |
| |
| Abstract: | In recent years, the formal analysis and verification of mobile commerce protocols become an important research hotspot in the field of mobile commerce protocols. We take the secure Payment Centric Model (PCM) using symmetric cryptography protocol as the research object, design a timed automata to model the PCMS protocol, and use the computation tree logic (CTL) to describe some properties of the protocol. Then we use the model checking verification tool UPPAAL to verify deadlock free, timeliness, validity and money atomicity of the protocol. Verification results show that the PCMS protocol can satisfy the requirements of deadlock free, timeliness, validity and money atomicity. |
| |
| Keywords: | mobile payment protocol model checking timed automata UPPAAL |
|
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|
