检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

移动支付协议PCMS的形式化分析和验证

计算机工程与科学 2017年第1期39卷 67-73页

作者：吴格格庄雷张坤丽王国卿郑州大学信息工程学院河南郑州450001

移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,... 详细信息

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

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

在线全文

学校读者我要写书评

暂无评论

移动支付协议的形式化分析与研究

移动支付协议的形式化分析与研究

作者：李茜太原理工大学

学位级别：硕士

随着移动设备的普及和移动互联网技术的提升,移动电子商务以其便利性、快捷性等优势覆盖了用户生活的各个领域。移动支付,作为移动商务的重要应用之一,也是移动金融的主要工具,有必要对其在相关领域做深入研究。同时,为保证移动支付安... 详细信息

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

关键词：移动支付协议形式化分析串空间模型检测 SPIN

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

移动支付协议的形式化分析与安全性研究

移动支付协议的形式化分析与安全性研究

作者：杨文霞太原理工大学

学位级别：硕士

随着第四代移动通信技术的成熟应用以及各种智能设备的兴起,移动支付凭借着它的便利性和快捷性等特点几乎覆盖了人们生活的各个方面。为了保证移动支付顺利、安全的进行,在进行通信以及数据传输时,所采用的移动支付协议的安全性就成为... 详细信息

随着第四代移动通信技术的成熟应用以及各种智能设备的兴起,移动支付凭借着它的便利性和快捷性等特点几乎覆盖了人们生活的各个方面。为了保证移动支付顺利、安全的进行,在进行通信以及数据传输时,所采用的移动支付协议的安全性就成为人们关注的重点。目前,形式化分析是协议安全性分析的有效方法之一。因此,在信息安全领域中,对移动支付协议的形式化分析与安全性研究已成为一个重要课题。移动支付协议在移动终端中运行,与传统支付协议不同的是,应当考虑到移动终端在存储空间、电量及计算水平等方面均有限的特点,因此应尽量选取轻量级的采用对称密钥加密的移动支付协议。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进行验证分析。结果均表明,改进后的协议满足公平性,从而保障了协议自身的安全属性。本文的研究工作主要体现为:改进后的密钥交换算法在一定程度上降低了计算量和运算时间,使协议更满足轻量级要求;改进后的支付协议保证了移动支付中不同主体的公平性,从而增强了移动支付的安全性。

关键词：移动支付协议轻量级 SVO逻辑 SPIN 公平性

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

一种移动支付协议的模型检验分析

计算机工程与应用 2006年第33期42卷 46-49,52页

作者：刘霞古天龙郭云川桂林电子工业学院计算机系广西桂林541004

给出了移动支付协议的一种有限状态机建模方法,该方法在传统支付协议的基础上充分考察了移动环境中移动装置和无线网络的特点,所建立的模型具有全面、准确、直观、简洁的特点。以一个典型的移动支付协议KSL为例,对该协议进行有限状态机... 详细信息

给出了移动支付协议的一种有限状态机建模方法,该方法在传统支付协议的基础上充分考察了移动环境中移动装置和无线网络的特点,所建立的模型具有全面、准确、直观、简洁的特点。以一个典型的移动支付协议KSL为例,对该协议进行有限状态机建模,并通过模型检验工具对其公平性进行了分析验证,指出了其缺陷并进行了改进,从而表明了方法的有效性。该方法具有一定的通用性,以其为基础,可对其他类型的移动电子商务协议进行模型检验分析。

关键词：移动支付协议模型检验公平性

在线全文

学校读者我要写书评

暂无评论

轻量级移动支付协议公平性分析

计算机工程与应用 2018年第19期54卷 82-87页

作者：李茜王峥马建芬李娜太原理工大学计算机科学与技术学院国网山西省电力公司

为保证移动支付安全、顺利进行,必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境,选择采用对称加密的轻量级移动支付协议PCMS,使用串空间理论对其建模,进行形式化分析。通过图的方式直观描述协议的执... 详细信息

为保证移动支付安全、顺利进行,必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境,选择采用对称加密的轻量级移动支付协议PCMS,使用串空间理论对其建模,进行形式化分析。通过图的方式直观描述协议的执行过程,分析协议安全目标,基于串空间理论的认证测试方法,对该协议的公平性形式化分析。针对PCMS协议不满足公平性,提出增加时间戳来解决,同时增加一个退款子协议完成后续退款操作。结合模型检测工具验证分析,结果表明,改进后的协议满足公平性。

关键词：移动支付协议形式化分析串空间公平性模型检测

在线全文

学校读者我要写书评

暂无评论

基于事件逻辑的移动支付协议形式化分析

基于事件逻辑的移动支付协议形式化分析

作者：杨科华东交通大学

学位级别：硕士

随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网... 详细信息

随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网络环境中,产生的错误很难发现,难以保证协议安全性分析的准确性,必须采用形式化方法和工具来分析。针对移动支付中存在的安全问题,对移动支付协议进行形式化分析,旨在发现移动支付协议中潜在的安全漏洞具有重要意义。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,可用于证明网络安全协议的安全性。本文基于事件逻辑理论并对其进行扩充,对移动支付协议进行形式化分析。本文主要研究内容如下: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协议为例进行了形式化分析,说明了结果扩展的事件逻辑能够分析移动支付协议的不可否认性。

关键词：形式化方法事件逻辑理论移动支付协议认证性不可否认性

基于时间自动机的移动支付协议的形式化验证及实例

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于时间自动机的移动支付协议的形式化验证及实例

作者：吴格格郑州大学

学位级别：硕士

随着移动支付的广泛应用,移动支付协议作为安全性的重要保障,已经成为了学术界的研究热点之一。为了保证移动支付协议的安全性和正确性,需要对移动支付协议进行形式化分析、建模和验证。但是移动支付协议是在移动环境中执行的,而且用户... 详细信息

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

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

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

一种终端认证简化的在线移动支付模式与协议

计算机研究与发展 2013年第2期50卷 291-301页

作者：王红新杨德礼姜楠马慧大连理工大学管理科学与工程学院辽宁大连116024 大连民族学院计算机科学与工程学院辽宁大连116024

信息安全技术在移动互联网中最重要的应用是移动支付,移动终端认证又是移动支付首先要解决的问题.移动支付的特殊性要求移动终端的认证要尽可能简单并对设备的依赖性最小,为此提出终端认证简化的移动支付模式.该模式建立在基于"预信任"... 详细信息

信息安全技术在移动互联网中最重要的应用是移动支付,移动终端认证又是移动支付首先要解决的问题.移动支付的特殊性要求移动终端的认证要尽可能简单并对设备的依赖性最小,为此提出终端认证简化的移动支付模式.该模式建立在基于"预信任"的分层认证模型与公共服务域为特征的支付系统架构上.通过建立商户为起点的信任传递链以及公共服务域中的帐户寻址与管理机制来实现系统安全可控及终端认证简化的目标.给出了相关研究综述、模式的系统架构、认证模式以及相应的支付协议,并对协议的安全性进行了分析.

关键词：移动终端认证公共服务域支付模式移动支付协议支付安全

基于预信任与公共服务域的柔性在线移动支付模式与协议

在线全文

学校读者我要写书评

暂无评论

大连理工大学学报 2013年第2期53卷 298-305页

作者：王红新杨德礼王建军马慧大连理工大学管理与经济学部辽宁大连116024

为动态适应电子商务不断创新以及客户对跨支付平台、跨支付方式的个性化需求,移动支付必须具备架构上的柔性与服务的柔性.为此,提出一种基于预信任与公共服务域的柔性在线移动支付模式,它支持支付系统架构的动态变化,支持跨平台支付服务... 详细信息

为动态适应电子商务不断创新以及客户对跨支付平台、跨支付方式的个性化需求,移动支付必须具备架构上的柔性与服务的柔性.为此,提出一种基于预信任与公共服务域的柔性在线移动支付模式,它支持支付系统架构的动态变化,支持跨平台支付服务,以线下信任与线上信任相结合以及依托公共服务域的办法解决支付系统的柔性问题,解决柔性与安全性之间的矛盾,并给出了该模式下的支付协议.通过对协议的分析,证明该模式与协议可以满足移动支付的柔性与安全性.

关键词：支付系统柔性预信任公共服务域移动支付协议支付安全