随着移动设备的普及和移动互联网技术的提升,移动电子商务以其便利性、快捷性等优势覆盖了用户生活的各个领域。移动支付,作为移动商务的重要应用之一,也是移动金融的主要工具,有必要对其在相关领域做深入研究。同时,为保证移动支付安全、顺利的进行,给人们的生活提供更大的便利,在进行通信以及传输数据时,必须采用安全的移动支付协议。因此,对移动支付协议的形式化分析和研究目前已经成为信息安全领域中的一个重要课题。移动支付协议执行在移动环境中,应当顾及到由于存储空间或是电量限制,移动支付极易中途阻断,计算水平低等特点,因此尽量选取采用对称加密的轻量级移动支付协议。2004年,Kungpisdan S等人建立和无线网络相配套、面向账户的KSL协议,引入了对称加密算法,无需对主体公钥加解密计算,减轻移动终端的计算负荷,提高协议执行效率。承接Kungpisdan S等人的设计思想,针对不同的通信场景,Jesús Téllez Isaac和Sherali Zeadally于2012年提出了以支付网关为中心的PCMS协议,该协议用临时身份代替客户的真实身份,保护客户隐私。在2014年对PCMS协议进一步的分析中表明,该协议需要更少的计算量和存储空间,可以部署在计算资源有限的移动设备上,使支付交易在无线网络上有效地执行。本文选取适用于不同通信场景、具有代表性的移动支付协议进行分析,基于定理证明的串空间理论对上述两协议分别建模,对移动支付协议进行形式化分析。通过图的方式直观描述协议的执行过程,总结协议潜在的安全问题。运用认证方法来着重分析协议的公平性,对协议内容做出改进。对改进后的协议,用模型检测器SPIN的Promela语言编程建模,验证分析。使用形式化分析方法的定理证明正向分析协议的安全属性,用模型检测工具SPIN模型检测器逆向检测协议是否存在漏洞,最后对有安全隐患的协议做出优化。根据结果,协议(改进后)符合公平性,确保了协议自身的安全属性。本文的研究工作对于移动支付协议的设计以及形式化分析技术有一定的理论和实用意义,同时改进的协议能够确保移动支付中不同主体各自的公平性,对增强移动支付的安全性有一定的价值。