摘要：摘要：移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象，建立了PCMS协议的时间自动机模型，并用计算树逻辑CTL公式描述PCMS协议的部分性质，最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明，以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。

关键词：移动支付协议 模型检测 时间自动机 uppaal 

单位：郑州大学信息工程学院; 河南郑州450001