Formal Analysis Of Mobile Payment Protocols Based On Logic Of Events

With the rapid popularization of mobile devices and the rapid development of mobile Internet,mobile payment brings great convenience to people's lives.Mobile payment is the key to the success of mobile e-commerce transactions,and secure mobile payment protocol is the cornerstone to ensure the safety mobile payment.Because security protocols often run in complex and insecure network environment,it is difficult to identify errors completely,and it is difficult to ensure the accuracy of protocol security analysis,so it's necessary to use formal methods and tools analyze them.Aiming at the security problems in mobile payment,the formal analysis of mobile payment protocol is of great significance to discover potential security vulnerabilities in mobile payment protocols.Logic of event theory(LoET)is a formal method for describing state migration in distributed systems,which can be used to prove security properties of network protocols.Based on the LoET and its extension,this paper makes a formal analysis of mobile payment protocols.The main contents of this paper are as follows:1.The background,development status and basic ideas of LoET are introduced in detail.The structure of message automata and event system in event system is elaborated,and how event logic captures and describes a distributed system is explained.The basic definitions of LoET,including atom,event sequence and event class are given,and the LoET proof system is given,six axioms and their related lemmas and properties are discussed.The LoET-based protocol modeling logic in modeling protocols is compared with the common message-arrow description method,which highlights the advantages of LoET in modeling protocols.The flow chart of formal proof of security protocols based on LoET is summarized.2.For mobile payment protocols with a large number of agents and a large number of protocol interaction steps,migration rules and inheritance are proposed.Actions in protocol threads can be migrated to the next sequence.For protocols with a large number of protocol agents and protocol interaction steps,the protocol proof process can be simplified and the complexity of protocol proof can be effectively reduced.The security of mobile payment protocol KerNeeS is analyzed by LoET,and the interaction among POS,NFC Phone and Authentication Server is analyzed.Formal description of the protocol's two-way authentication process,analysis of the basic sequence of the two sides of the protocol interaction,based on the LoET proof system to prove the strong authentication,it is concluded that the two-way authentication between POS and NFC Phone can be achieved.3.In view of the defect that LoET can only analyze the authentication of security protocols but not the non-repudiation,the LoET is extended.Adding predicates such as Has,CanProve,Claims and Controls,expanding protocol proof system,adding possession axioms,jurisdiction axioms and signature axiom,so that the new extended method can describe and analyze the non-repudiation protocol.4.Defineing and analysing non-repudiation property,useing LoET to describe it formally and elaborating the concrete steps for formal analysis of non-repudiation property.Firstly,the initial state of the protocol is listed,including the initial message ownership set and the initial belief set of the protocol,explaining the initial state set of the protocol agent,and giveing the rules for generating the message and belief;secondly,the sender's non-repudiation evidence EOO and the receiver's non-repudiation evidence EOR are listed,and analyzing whether EOO and EOR meet the non-repudiation requirement;lastly,whether the protocol meets the non-repudiation requirement is analyzed.The goal of non-repudiation is whether EOO?and EOR?established simultaneously when the protocol is running at any stage,so as to analyze whether the non-repudiation of the protocol is satisfied.According to the above proof process,the FMPP protocol is taken as an example for formal analysis,which shows that the extended LoET can analyze the non-repudiation of the mobile payment protocols.