Formal Verification And Instance Of Mobile Payment Protocol Based On Timed Automata

With the wide application of mobile payment, mobile payment protocol is an important guarantee of its security, has become a research focus in the academia. To ensure the safety and correctness of mobile payment protocol, we need to formal modeling, analysis and verification of it. Mobile payment protocol is implemented in a mobile environment, and mobile devices are limited in power, computing power and storage space, those posed new challenges to formal analysis, modeling and verification of mobile payment protocol. Thus, formal analysis and verification of mobile payment protocol has important significance.According to the different scenarios of mobile communication, Jesús Téllez Isaac et al. proposed a secure payment centric model using symmetric cryptography protocol(hereafter referred to as PCMS), and present analysis and performance evaluation(in terms of execution time and memory space) of the PCMS protocol in a real environment. The results show that PCMS protocol requires less computation in server centric scenario. But they do not formal analysis and verification of security properties of PCMS protocol, so PCMS protocol doesn’t get a wide range of applications in real life.This thesis is modeling based on timed automata for mobile payment protocol. Respectively subjects of system, communication environment and subject operation are described; and using timed automata to model and analysis of mobile payment protocol. On the basis of timed automata modeling, this thesis select PCMS protocol as the research object, use model checking tool UPPAAL to analyze and verify of PCMS protocol. Verification results show that the PCMS protocol satisfy deadlock-free, timeliness, validity and money atomicity.