Abstract: 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.

Key words: mobile payment protocol, formal analysis, strand spaces, fairness, model checking

摘要： 为保证移动支付安全、顺利进行，必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境，选择采用对称加密的轻量级移动支付协议PCMS，使用串空间理论对其建模，进行形式化分析。通过图的方式直观描述协议的执行过程，分析协议安全目标，基于串空间理论的认证测试方法，对该协议的公平性形式化分析。针对PCMS协议不满足公平性，提出增加时间戳来解决，同时增加一个退款子协议完成后续退款操作。结合模型检测工具验证分析，结果表明，改进后的协议满足公平性。

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