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

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