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

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