Formal Analysis And Security Research Of Mobile Payment Protocol

With the mature application of the fourth generation mobile communication technology and the rise of various smart devices,mobile payment covers almost all aspects of people's lives with its advantages such as convenience and speed.In order to ensure the smooth and safe implementation of the mobile payment,the security of the mobile payment protocol used in communication and data transmission becomes the focus of people's attention.Currently,formal analysis is one of the effective methods for protocol security analysis.Therefore,in the field of information security,the formal analysis and security research of mobile payment protocol has become an important issue.The mobile payment protocol runs in the mobile device.Different from the traditional payment protocol,considering that the mobile device is limited in terms of storage space,power consumption and calculation level.Therefore,mobile payment protocol which uses lightweight encryption and symmetric key should be selected.In 2008,Tan Soo Fun et al.proposed the LMPP protocol(Lightweight Mobile Payment Protocol)based on mobile operator MNO,which uses symmetric key operation,not only reduces the computational operation and the communication between related parties,but also achieves the payer's complete privacy protection which meets the end-to-end security attributes and all the standards required by all parties.In 2012,they continued to analyze the protocol,proposed four analytical objectives,and used KP logic for analysis and verification.The results show that the LMPP protocol satisfies the accountability.In 2016,Farahnaz Zamanian et al.analyzed the LMPP protocol and found thatthe payee had security problems in anonymity and unlinkability,so they proposed a solution to satisfy the payee's anonymity and unlinkability.This paper selects the LMPP as the research object,a lightweight privacy protection mobile payment protocol with Mobile Operator Network(MNO)as the value chain,and analyzes the two parts of the protocol.In the registration protocol,the Diffie-Hellman algorithm is improved,and a certain number of large prime numbers are selected for experiment.The experimental results show that the improved algorithm reduces the amount of computation required for shared key generation,and the computation time is also significantly reduced,thus the improved protocol can be more suitable for mobile devices with limited resources.In the payment agreement,the SVO logic method is used to formally analyze the mobile payment protocol.Through reasoning,it is found that the agreement does not satisfy the fairness,so the agreement is improved.Then,SVO logical is used again for the improved protocol,and the verification analysis is performed by using the model detection tool SPIN modeled by Promela language.The results show that the improved protocol satisfies the fairness,thus ensuring the security attributes of the protocol itself.The research work of this paper is mainly reflected in: the improved key exchange algorithm reduces the calculation amount and operation time at a certain extent,so that the protocol can meet the lightweight requirements better;The improved payment protocol guarantees the fairness of the protocol between payer and payee,thereby enhancing the security of mobile payment.