Abstract: With the rise of wireless network and various intelligent devices, mobile payment becomes more and more important, so it is necessary to adopt a secure Lightweight Mobile Payment Protocol（LMPP） to ensure the mobile payment going smoothly. For mobile devices with limited resources and payment scenarios with limited environment, the LMPP, a lightweight privacy protection mobile payment protocol with Mobile Network Operator（MNO） as the value chain, is selected as the research object. The SVO logic is chosen to analyze the protocol and prove that the protocol does not meet the fairness. And the other secure attributes of the LMPP are analyzed and the part of the protocol which does not satisfy the fairness is improved. Meanwhile, the SPIN model checking tool is used to detect the improved protocol. The results show that the fairness is satisfied in this improved protocol.

Key words: Lightweight Mobile Payment Protocol（LMPP）, Mobile Network Operator（MNO）, SVO logic, fairness, SPIN

摘要： 无线网络以及各种智能设备的兴起，使得移动支付越来越重要，因此必须采用安全的轻量级移动支付协议（Lightweight Mobile Payment Protocol，LMPP）来保障移动支付的顺利进行。针对资源有限的移动设备及环境受限的支付场景，选取以移动运营商（Mobile Network Operator，MNO）为价值链的轻量级的隐私保护移动支付协议为研究对象。采用SVO逻辑形式化分析协议，证明协议不满足公平性。并对LMPP协议其他安全属性进行分析，针对协议不满足公平性的部分做出改进。同时运用SPIN模型检测工具进行检测，验证结果表明，改进后的协议满足公平性。

关键词: 轻量级移动支付协议（LMPP）, 移动运营商（MNO）, SVO逻辑, 公平性, SPIN