移动支付协议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.

参考文献［16］

［1］	Cao Yuzhi,Lu Yaobin,Gupta S,et al.The effects of differences between ecommerce and mcommerce on the consumers’ usage transfer from online to mobile channel ［J］.International Journal of Mobile Communications,2015,13(1):5170.
［2］	Isaac J T,Zeadally S.Design,implementation,and performance analysis of a secure payment protocol in a payment gateway centric model ［J］.Computing,2014,96 (7):587611.
［3］	Dahlberg T, Guo Jie, Ondrus J. A critical review of mobile payment research［J］.Electronic Commerce Research and Applications,2015,14(5):265284.
［4］	Lei Xinfeng,Song Shumin,Liu Weibing,et al.A survey on computationally sound formal analysis of cryptographic protocols［J］.Chinese Journal of Computers,2014,37(5):9931016.(in Chinese)
［5］	Dolev D,Yao A.On the security of public key protocols［J］.IEEE Transactions on Information Theory,1983,29(2):198208.
［6］	Zhou Diancui,Qing Sihan,Zhou Zhanfei.A new tool for analyzing electronic commerce protocols ［J］.Journal of Software,2001,12(9):13181328.(in Chinese)
［7］	Qing Sihan. A formal method for analyzing electronic commerce protocols ［J］.Journal of Software,2005,16(10):17571765.(in Chinese)
［8］	Wang Caifen,Ge Jianhua.A new approach for the analysis of electronic commerce protocols ［J］.Chinese Journal of Computers,2004,27(4):507515.(in Chinese)
［9］	Dong Rongsheng, Chen Dawei, Guo Yunchuan, et al.Finitestate analysis of a fair nonrepudiation protocol ［J］.Computer Science,2005,32(8):8386.(in Chinese)
［10］	Guo Hua,Zhuang Lei,Zhang Xiyong,et al.Verifying multiple runs of FR protocol using model checking ［J］.Computer Science,2008,35(5):9598.(in Chinese)
［11］	Guo Hua,Li Zhoujun,Zhuang Lei,et al.New approach for analyzing of ecommerce protocol ［J］.Computer Science,2010,8(1):5660.(in Chinese)
［12］	Kremer S, Raskin J F.A gamebased verification of nonrepudiation and fair exchange protocols ［J］.Journal of Computer Security,2003,11(3):399429.
［13］	Wen Jinghua, Zhang Mei, Li Xiang. Formal analysis of ecommerce protocols based on game ［J］.Journal on Communications,2006,27(3):7378.(in Chinese)
［14］	Wen Jinghua, Li Xiang, Zhang Huanguo, et al.Formal analysis of fair ecommerce protocols based on ATL ［J］.Journal of Electronics & Information Technology,2007,29(4):901905.(in Chinese)
［15］	Gan Zaobin, Xiao Shicheng, Li Kai, et al.Secure ecommerce payment protocol based on four parties ［J］.Computer Science,2011,38(10):3944.(in Chinese)
［16］	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.(in Chinese)
［17］	Isaac J T,Zeadally S.An anonymous secure payment protocol in a payment gateway centric model ［J］.Procedia Computer Science,2012,10:758765.
［18］	Alur R,Dill D L.A theory of timed automata ［J］.Theoretical Computer Science,1994,126(2):183235.
［19］	Larsen K G,Petterson P,Wang Yi.UPPAAL in a nutshell［J］.International Journal on Software Tools for Technology Transfer,1997,1(12):134152.
［20］	Behrmann G, David A, Larsen K G.A tutorial on Uppaal［M］.Berlin Heidelberg:Springer,2004:200236.
	附中文参考文献：
［4］	雷新峰,宋书民,刘伟兵,等.计算可靠的密码协议形式化分析综述［J］.计算机学报,2014,37(5):9931016.
［6］	周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具［J］.软件学报,2001,12(9):13181328.
［7］	卿斯汉.一种电子商务协议形式化分析方法［J］.软件学报,2005,16(10):17571765.
［8］	王彩芬,葛建华.一种分析电子商务协议的新方法［J］.计算机学报,2004,27(4):507515.
［9］	董荣胜,陈大伟，郭云川，等.公平非否认协议的有限状态分析［J］.计算机科学,2005,32(8):8386.
［10］	郭华,庄雷,张习勇,等.基于模型检测的多轮FR协议验证［J］.计算机科学,2008,35(5):9598.
［11］	郭华,李舟军,庄雷,等.一种新的电子商务协议分析方法［J］.计算机科学,2010,8(1):5660.
［13］	文静华,张梅,李祥.基于博弈的电子商务协议分析［J］.通信学报,2006,27(3):7378.
［14］	文静华,李祥,张焕国,等.基于ATL的公平电子商务协议形式化分析［J］.电子与信息学报,2007,29(4):901905.
［15］	甘早斌,肖仕成,李开,等.基于四方的安全电子商务支付协议研究［J］.计算机科学,2011,38(10):3944.
［16］	肖仕成,李开,甘早斌.基于四方的安全电子商务支付协议分析与验证［J］.计算机科学,2012,39(3):7578.

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