移动支付协议PCMS的形式化分析和验证  

Formal analysis and verification of mobile payment protocol PCMS

作　　者：吴格格 庄雷[1] 张坤丽[1] 王国卿[1] WU Ge-ge ZHUANG Lei ZHANG Kun-li WANG Guo-qing(School of Information Engineering,Zhengzhou University,Zhengzhou 450001 ,China)

机构地区：[1]郑州大学信息工程学院,河南郑州450001

出　　处：《计算机工程与科学》2017年第1期67-73,共7页Computer Engineering & Science

基　　金：国家973计划(2012CB315901);国家自然科学基金(61379079);河南省科技厅攻关项目(122102210042);河南省科技厅基础研究项目(142300410231;142300410308)

摘　　要：移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。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.

关 键 词：移动支付协议 模型检测 时间自动机 UPPAAL 

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