随着第四代移动通信技术的成熟应用以及各种智能设备的兴起,移动支付凭借着它的便利性和快捷性等特点几乎覆盖了人们生活的各个方面。为了保证移动支付顺利、安全的进行,在进行通信以及数据传输时,所采用的移动支付协议的安全性就成为人们关注的重点。目前,形式化分析是协议安全性分析的有效方法之一。因此,在信息安全领域中,对移动支付协议的形式化分析与安全性研究已成为一个重要课题。移动支付协议在移动终端中运行,与传统支付协议不同的是,应当考虑到移动终端在存储空间、电量及计算水平等方面均有限的特点,因此应尽量选取轻量级的采用对称密钥加密的移动支付协议。Tan Soo Fun等人于2008年基于移动运营商MNO提出LMPP协议(Lightweight Mobile Payment Protocol),该协议采用对称密钥加密,减少了相关各方之间的计算量和通信量,并实现了对买方的完全隐私保护,满足了端到端的安全属性和各方要求的所有标准,并在2012年继续对协议进行可追究性分析,提出了4个分析目标,运用KP逻辑进行分析验证,验证结果表明,LMPP协议满足可追究性。Farahnaz Zamanian等人于2016年对LMPP协议进行分析,发现卖方在匿名性和不可链接性存在安全问题,提出了一种解决方案,从而满足了卖方的匿名性和不可链接性。本文选取以移动运营商MNO为价值链的轻量级隐私保护的移动支付协议为研究对象,对协议的两个部分进行分析。注册协议部分,对Diffie-Hellman算法进行改进,并选取一定数量的大素数进行实验,实验结果表明改进后的算法降低了共享密钥生成所需的计算量,运算时间也明显降低,从而使协议更适用于资源有限的移动设备。支付协议部分,采用SVO逻辑方法形式化地分析移动支付协议,通过推理证明,发现协议不满足公平性,对协议作出改进。然后对改进后的协议,再次运用SVO逻辑推理证明,并通过使用Promela语言建模的模型检测工具SPIN进行验证分析。结果均表明,改进后的协议满足公平性,从而保障了协议自身的安全属性。本文的研究工作主要体现为:改进后的密钥交换算法在一定程度上降低了计算量和运算时间,使协议更满足轻量级要求;改进后的支付协议保证了移动支付中不同主体的公平性,从而增强了移动支付的安全性。