随着移动支付的广泛应用,移动支付协议作为安全性的重要保障,已经成为了学术界的研究热点之一。为了保证移动支付协议的安全性和正确性,需要对移动支付协议进行形式化分析、建模和验证。但是移动支付协议是在移动环境中执行的,而且用户使用的移动设备在电量、计算能力和存储空间方面均受到限制,这些约束都给移动支付协议的形式化分析、建模和验证提出了新的挑战。因此,研究移动支付协议的形式化分析、建模和验证具有重大的意义。根据移动通信的不同场景,Jesús Téllez Isaac等人提出了使用对称加密技术以支付网关为中心的安全支付协议PCMS(Secure Payment Centric Model using Symmetric cryptography protocol),并在真实环境下对PCMS协议的执行时间和内存空间进行了分析和评估。结果表明,在服务器中心模型下,PCMS协议计算量少。但是未对PCMS协议的安全性质进行形式化分析和验证,因此在实际生活中并没有得到广泛应用。本文基于时间自动机对移动支付协议进行了建模。分别对系统主体、通信环境和主体操作进行了描述,并采用时间自动机对移动支付协议进行建模和分析。在使用时间自动机对移动支付协议建模的基础上,本文选取使用对称加密技术以支付网关为中心的安全支付协议PCMS为研究对象,使用模型检测工具UPPAAL对PCMS协议进行了分析和验证。结果表明,PCMS支付协议满足无死锁、时效性、有效性和钱原子性。