随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网络环境中,产生的错误很难发现,难以保证协议安全性分析的准确性,必须采用形式化方法和工具来分析。针对移动支付中存在的安全问题,对移动支付协议进行形式化分析,旨在发现移动支付协议中潜在的安全漏洞具有重要意义。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,可用于证明网络安全协议的安全性。本文基于事件逻辑理论并对其进行扩充,对移动支付协议进行形式化分析。本文主要研究内容如下:1.详细介绍事件逻辑理论的产生背景、发展现状、基本思想;对事件系统中的消息自动机和事件系统结构做了阐述,说明事件逻辑是如何去捕捉并描述一个分布式系统;给出事件逻辑理论中的基本定义,包括Atom原子、事件序、事件类,给出了事件逻辑证明系统中的六条公理以及相关引理及性质,其中着重对协议形式化建模中基于事件逻辑的协议建模逻辑与普通的消息-箭头描述方法进行了对比,突出了事件逻辑在协议建模方面的优势;总结归纳了基于事件逻辑的安全协议形式化证明流程图。2.针对移动支付协议中主体数目、协议交互步骤数目较多的情况下,提出迁移规则和可继承性,协议线程中的动作可以迁移到下一个序列中,对于多个协议主体数目、协议交互步骤数目多的协议,能够简化协议证明流程,有效减少协议证明的复杂性。通过事件逻辑理论分析移动支付协议KerNeeS协议安全性,对POS、NFC Phone和Authentication Server间交互进行分析。形式化描述协议双向认证过程、分析协议交互双方的基本序列,基于事件逻辑证明系统对强认证性质进行证明,得出POS和NFC Phone之间能够实现双向认证。3.针对事件逻辑只能分析安全协议认证性而不能分析不可否认性的缺陷,对事件逻辑理论进行扩展。增添了Has、CanProve、Claims、Controls等谓词,扩展协议证明系统,加入拥有公理、管辖公理、签名公理,让扩展的新方法能够对包含不可否认性的协议进行描述与分析。4.对不可否认性进行了定义与分析,使用事件逻辑对其进行形式化刻画说明,阐述了形式化分析不可否认性的具体步骤。首先列举协议的初始状态,包括协议的初始消息拥有集合和初始信念集合,对协议主体的初始状态集合进行了说明,并给出消息、信念的生成规则;接着列举发送方非否认证据EOO和接收方非否认证据EOR,分析EOO和EOR是否符合不可否认性要求;最后分析协议是否达到不可否认性目标,当协议运行在任何阶段时,是否有EOO∈和EOR∈同时成立,从而来分析协议的不可否认性是否满足。根据上述证明流程,以移动支付协议FMPP协议为例进行了形式化分析,说明了结果扩展的事件逻辑能够分析移动支付协议的不可否认性。