轻量级移动支付协议公平性分析  

Lightweight mobile payment protocol fairness analysis

作　　者：李茜 王峥 马建芬 李娜[2] LI Qian;WANG Zheng;MA Jianfen;LI Na(College of Computer Science and Technology,Taiyuan University of Technology,Taiyuan 030024,China;State Grid Shanxi Electric Power Company,Taiyuan 030024,China)

机构地区：[1]太原理工大学计算机科学与技术学院 [2]国网山西省电力公司

出　　处：《计算机工程与应用》2018年第19期82-87,共6页Computer Engineering and Applications

基　　金：山西省重点研发计划国际合作项目(No.201603D421013)

摘　　要：为保证移动支付安全、顺利进行,必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境,选择采用对称加密的轻量级移动支付协议PCMS,使用串空间理论对其建模,进行形式化分析。通过图的方式直观描述协议的执行过程,分析协议安全目标,基于串空间理论的认证测试方法,对该协议的公平性形式化分析。针对PCMS协议不满足公平性,提出增加时间戳来解决,同时增加一个退款子协议完成后续退款操作。结合模型检测工具验证分析,结果表明,改进后的协议满足公平性。To ensure the safe and smooth development,the protocol of mobile payment must be security.In view of the limited computing and storage capacity of mobile devices and unreliable mobile environment,the typical lightweight protocol-a secure Payment Centric Model using Symmetric cryptography protocol(PCMS)is taken as an example,the strand spaces theory is used to model it and do formal analysis.The execution process of the protocol is visually described in a graphical way,it gives security objectives of the protocol and analyzes the fairness of the authentication test method based on the strand spaces theory.Put forward to increase the timestamp to solve that the PCMS agreement does not meet the fairness,meanwhile adding a refund agreement to complete the following refund operation.Model checking tool validation analysis,results show that the improved protocol meet fairness.

关 键 词：移动支付协议 形式化分析 串空间 公平性 模型检测 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]