Formal Analysis And Research Of Mobile Payment Protocol

With the popularization of mobile devices and the promotion of mobile Internet technology,mobile e-commerce covers all areas of user's life with advantages of convenience and rapidity.Mobile payment,as one of the important applications of mobile commerce,is also the main tool of mobile finance and it is necessary to do in-depth research in related fields.At the same time,in order to ensure the safe and smooth implemetation of mobile payment and to provide greater convenience for people's lives,a secure mobile payment protocol must be adopted when communicating and transmitting data.Therefore,the formal analysis and research of mobile payment protocol has become an important topic in the field of information security.Mobile payment protocol implementation in mobile environment should take into account the characteristics of storage space or power limitation,and mobile payment is easily blocked in the middle,the low level of calculation etc.,so try to choose lightweight mobile payment protocol using symmetrical encryption.In 2004,Kungpisdan S et al.established a KSL protocol that is compatible with wireless networks and accounts.It introduced a symmetric encryption algorithm,eliminating the need for encryption and decryption of the subject public key,reducing the computational load on the mobile terminal,and improving protocol execution efficiency.Continuing the design philosophy of Kungpisdan S et al.,in response to different communication scenarios,Jesús Téllez Isaac and Sherali Zeadally,in 2012,proposed the PCMS protocol centered on the Payment gateway(a secure Payment Centric Model using Symmetric cryptography protocol).This protocol replaces the customer's real identity with a temporary identity to protect customer privacy.A further analysis of the PCMS protocol in 2014 showed that the protocol requires less computational and storage space and can be deployed on mobile devices with limited computing resources to enable payment transactions to be effectively performed on wireless networks.In this paper,a representative mobile payment protocol that is applicable to different communication scenarios is selected for analysis.Based on theorem proving string space theory,the above two protocols are modeled separately,and the mobile payment protocol is formally analyzed.Visually describe the implementation of the protocol through the diagram and summarize the potential security issues of the protocol.By using the authentication test method,the fairness of the agreement is analyzed and improved.The improved protocol was modeled and verified by the Promela programming of the model detector SPIN.The theorem using the formal analysis method proves the security attributes of the forward analysis protocol and uses the model checking tool SPIN to detect whether there is a loophole in the reverse detection protocol,and finally optimizes the protocol with security risks.According to the results,the agreement(improved)meets fairness and ensures the security properties of the agreement itself.In this paper,the research work has certain theoretical and practical significance for the design of mobile payment protocols and formal analysis techniques.At the same time,the improved protocol can ensure the fairness of different subjects in each mobile payment,and have certain value in enhancing the safety of mobile payment.