Abstract:

In recent years, the formal analysis and verification of mobile commerce protocols become an important research hotspot in the field of mobile commerce protocols. We take the secure Payment Centric Model (PCM) using symmetric cryptography protocol  as the research object, design a timed automata to model the PCMS protocol, and use the computation tree logic (CTL) to describe some properties of the protocol. Then we use the model checking verification tool UPPAAL to verify  deadlockfree, timeliness, validity and money atomicity of the protocol. Verification results show that the PCMS protocol can satisfy the requirements of deadlockfree, timeliness, validity and money atomicity.

Key words: mobile payment protocol, model checking, timed automata, UPPAAL