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

摘要：

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

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

所属期刊栏目：39

分类号：TP309(计算技术、计算机技术)

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

在线出版日期：2017-03-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：67-73