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

计算机工程与科学

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

吴格格，庄雷，张坤丽，王国卿

（郑州大学信息工程学院,河南郑州 450001）

收稿日期:2015-10-26 修回日期:2015-12-22 出版日期:2017-01-25 发布日期:2017-01-25
基金资助:
国家973计划(2012CB315901)；国家自然科学基金(61379079)；河南省科技厅攻关项目(122102210042)；河南省科技厅基础研究项目(142300410231,142300410308)

Formal analysis and verification of mobile

payment protocol PCMS

WU Gege，ZHUANG Lei，ZHANG Kunli，WANG Guoqing

（School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China）

Received:2015-10-26 Revised:2015-12-22 Online:2017-01-25 Published:2017-01-25

摘要/Abstract

摘要：

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

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

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.

Key words: mobile payment protocol, model checking, timed automata, UPPAAL

吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学.

WU Gege，ZHUANG Lei，ZHANG Kunli，WANG Guoqing.

Formal analysis and verification of mobile

payment protocol PCMS

[J]. Computer Engineering & Science.

[1]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[2]	白先平, 姚袭欣, 陈香兰, 刘翀, 李曦. 基于时间自动机的AADL端到端流规约验证方法[J]. 计算机工程与科学, 2023, 45(05): 810-819.
[3]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[4]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[5]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[6]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[7]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[8]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[9]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[10]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[11]	程道雷,肖美华,刘欣倩,梅映天,李伟. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. J4, 2015, 37(11): 2121-2127.
[12]	马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.
[13]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.
[14]	白海洋，李静，赵娜. 基于时间自动机的嵌入式软件模型可调度性验证[J]. J4, 2013, 35(3): 121-127.
[15]	张君华1,黄志球2,肖芳雄3. 基于抽取-精化的概率系统假设-保证验证[J]. J4, 2013, 35(3): 128-133.