Z＆G协议公平性的形式化验证

Zhou和Gollmann设计的公平非否认协议(Z&G协议)旨在为电子商务交易的双方提供非否认证据和公平性.提出一种基于状态转换的方法对其公平性进行分析.与以往方法不同,它是一种针对电子商务协议的专门分析工具:用状态转换系统为电子商务系统建模;用基于状态的形式系统描述协议,将协议的信任假设显式表示为协议的一部分.该方法按进程是否背离协议或者背离协议的程度将协议在系统中的执行序列定义为三类模式:遵守型、欺骗型和中断型.验证了Z&G协议在三种模式下的执行序列都满足公平性.     

基于动态博弈的电子支付系统模型及自利性*

使用通信顺序进程CSP和博弈理论提出了基于动态博弈的电子支付系统模型,提出了一种电子支付协议的新属性自利性; 基于纳什均衡理论给出了自利性的形式化定义,可以用于对电子支付系统安全属性的形式化分析。 与以前的工作相比,其主要贡献为：基于CSP事件对参与者的交叠并发和同步行为建模, 基于博弈策略理论对协议主体的多种不诚实行为和三种质量的通信媒介建模,可以用于分析协议主体与通信媒介之间的合作和竞争行为; 对进程失效和通信失效建模,其中通信失效模型考虑了消息延迟导致的失效,因此可以分析更多失效情况下协议的性质;自     

一种交换协议的理性模型及其公平机制设计

理性交换协议是解决小额支付的有效方法,但是由于参与者的自利性,理性交换协议的公平性较难满足。论文首先对理性交换过程中的集体利益进行形式化定义,并基于占优策略构建理性参与者模型,以及基于占优策略和集体利益建立理性交换协议的公平性模型;其次基于激励相容理论设计理性交换协议的公平机制,基于理性交换协议的公平机制和扩展式博弈构建理性交换协议的理性博弈模型,并基于理性交换协议的博弈模型设计了一个理性交换协议;最后基于相关博弈方法证明所设计协议满足正确性和理性公平性,并用一个案例说明方案的可行性。     

基于CSP和动态博弈的电子支付系统模型

分析电子支付系统的安全问题,提出基于通信顺序进程和动态博弈的电子支付系统模型。该模型对协议主体的各种不诚实行为和3种质量的通信媒介建模,可以用于分析协议主体和通信媒介之间的合作和竞争行为。对进程失效和由于消息丢失或消息延迟导致的通信失效建模,能分析各种失效情况下协议的安全属性。     

公平交换协议形式逻辑

在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将这些威胁归结为两类入侵者.基于模型检查思想,新逻辑将协议定义为Kripke结构的演化系统,将参与者看作异步环境中的通信进程,定义了时间算子控制实体行为的转换.同时,新逻辑继承了信任逻辑简单、实用的优点.以一个典型协议为例,采用逻辑结合模型检查的方法,演示了分析协议的过程.发现并改进了协议实例的安全缺陷.案例分析表明,新逻辑能够分析公平交换协议的公平性和时限性.     

对一个公平文件交换协议的博弈分析与改进

文献[1]提出了一个基于证书机制的公平文件交换协议——Ping-协议,文章利用文献[6]中提出的基于博弈论思想对公平交换协议进行形式化分析的方法对Ping-协议进行了建模和分析,发现当协议的接收方在交换子协议执行了两个步骤之后执行恢复子协议会破坏协议的公平性;同时文章对协议建模时也将通信信道形式化,从而发现,如果协议的一个参与方能够与通信信道合作,那么也可以破坏协议的公平性。文章针对发现的漏洞对Ping-协议进行了修改,修改后的协议能够满足协议公平性的要求。     

一种新的电子商务协议分析方法

基于卿-周逻辑给出了一些新的逻辑推理规则,并提出了一种扩展的通信有限状态自动机,用于分析电子商务协议的安全性质.该方法可描述协议参与者的行为与知识,且无需人为地引入初始假设.对扩展模型抽象并修改后,还可验证其它一些与加密、签名消息无关的性质.利用该方法分析了匿名可恢复的公平交换协议,发现其满足有效性、公平性、可追究性,但不满足匿名性,并用UPPAAL验证了协议的公平性、活性与时效性等.     

一种乐观电子商务协议的公平性分析

乐观电子商务协议通常具有复杂结构,由多个子协议组合而成,与传统认证协议具有显著不同。电子商务协议最主要目的是实现买卖双方的公平交换,同时假定交换双方都可能是不诚实的,需要考虑来自协议合法实体的内部攻击。文章在深入分析公平交换协议各项属性的基础上,定义了电子项的认证属性,对SVO逻辑进行了扩展,使用SVO逻辑语法定义了电子商务协议应满足的公平性。文章以一种真实的电子商务协议为对象,演示了基于SVO逻辑的电子商务协议公平性分析方法,并指出该协议存在安全缺陷,提出改进意见。     

一种基于令牌的认证密钥交换协议

对称密钥系统较之非对称密钥系统具有惊人的速度优势,但是管理对称密钥系统的密钥却是需要解决的一个难题。Diffie-Hellman密钥交换是一个可以使通信双方在不可信信道上一同建立共享密钥,并使之应用于后继对称密钥通信系统的一种密码协议。应当注意到,Diffie-Hellman密钥交换协议不支持对所建立的密钥的认证。处于两个通信参与者Alice和Bob之间的一个恶意的攻击者Mallary可以主动操纵协议运行过程的信息并成功实施所谓的中间人攻击(man-in-the-middleattack)。因此为了能够真正在两个通信参与者Alice和Bob之间协商一个密钥就必须确保他们在协议运行过程中收到的信息的确是来自真实的对方。本文就是给出一种基于令牌的认证密钥交换协议以对Diffie-Hellman密钥交换协议进行改进。这对于电子商务等等很多网络应用而言是至关重要的。本文也给出了这种协议的安全性分析,并描述了基于JAVA的实现。     

基于ATL的公平交换协议的形式化验证

如何对电子商务协议进行分析与验证一直是研究的热点,基于ATL（交替时态逻辑）对电子商务协议中的公平交换协议（Fair Exchange Protocols）进行形式化分析与验证,并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议,并使用ATS（Alternating Transition Systems,交替转移系统）来为公平交换协议进行形式化建模,再用形式化验证工具MOCHA对公平交换协议的公平性（Fairness）、及时性（Timeliness）和不可滥用性（Abuse-Freeness）进行有效的验证;对验证结果进行分析与讨论,发现了该协议不满足公平性和不可滥用性,不符合设计的要求。     

电子商务协议的串空间分析

电子商务协议常常具有复杂结构,协议可能由多个子协议组合而成.因此,电子商务协议的安全分析较认证协议更为复杂.传统的信念逻辑不适宜分析电子商务协议.Kailar逻辑适宜分析电子商务协议的可追究性,但不适宜分析协议的公平性.本文介绍并扩展了串空间逻辑,分析了ISI支付协议的串,并证明其不满足公平性.还提出一种新的串节点路径法,用以分析了ASW协议,该协议系由多个子协议组成的分支结构协议,通过串空间分析证明了该协议的公平性.通过对两个协议的分析,分别提供了对电子商务在线交易协议和离线交易协议的形式化分析方法.     

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

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

CMP协议的缺陷及改进

近年来，安全电子商务协议的设计和分析逐渐成为热点。机密性、公平性等性质是衡量电子商务协议安全与否的重要标志，也是协议能否顺利使用的重要前提。机密性和公平性是安全电子商务协议的基本性质，但可证实电子邮件协议CMP作为电子商务协议的一种却并不满足这些性质。该文指出可证实电子邮件协议CMP的几个缺陷，对其分析并提出了改进方案，改进后的协议满足了机密性和公平性。     

乐观公平交换协议的可追究性分析

可追究性是安全电子商务协议必须遵循的重要原则之一,乐观公平交换协议是一类重要的电子商务协议。目前没有针对乐观公平交换协议的可追究性进行形式化分析的具体方法。文章提出了一种分析乐观公平交换协议可追究性的形式化方法,该方法不再单独定义非否认证据,只是研究协议的目标设计是否能提供实现可追究性的证据,将可追究性证明与公平性等其它安全性质的证明分开讨论,这样不论协议是否满足其它安全性质,都可以讨论协议是否满足可追究性。     

一种电子商务协议形式化分析方法

提出了一种新颖的形式化方法,可以用于分析电子商务协议的安全性质,例如可追究性和公平性.与以前的工作相比较,主要贡献在于:(1)对协议主体的拥有集合给出了形式化定义,且主体的初始拥有集合只依赖于环境;(2)将协议的初始状态假设集合分为3类:基本假设集合、可信假设集合和协议理解假设集合,避免了因非形式化的初始假设而产生的分析错误;(3)对可信假设作细粒度的形式化规范,揭示协议的内涵;(4)建立公理系统,使新方法更为严格与合理.     

一种分析电子商务安全协议的新逻辑

针对典型电子商务安全协议逻辑分析方法存在的问题,如安全属性分析存在局限性、缺乏形式化语义、对混合密码原语的处理能力不强等,提出了一种新的逻辑分析方法。新逻辑能够分析电子商务安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。以匿名电子现金支付协议ISI作为分析实例,证明了新逻辑方法的有效性。分析找出了该协议的安全漏洞和缺陷:不满足商家的非否认性、密钥保密性、可追究性、公平性以及原子性,客户面临商家恶意欺骗的潜在威胁。     

基于有穷自动机模型的电子商务支付协议公平性研究

文中将形式化方法，即有穷自动机理论分析方法应用到电子商务支付协议的研究中，证明了ISI协议不满足支付过程的公平性，在此基础上提出了具体的修改办法。     

一种分析安全协议的新逻辑

提出了一种分析安全协议的新逻辑,既能有效地分析认证协议的认证性,又能分析电子商务协议的可追究性和公平性。该方法对认证协议的分析,不需要协议理想化,避免了因理想化而导致的各类问题。能够有效地分析电子商务协议的可追究性和公平性,用于分析实用协议。分析过程简单直观,便于实现机器自动验证。     

Kailar逻辑的缺陷

近年来,电子商务协议的设计逐渐成为热点.可追究性是指电子商务协议迫使个人或组织对自己在电子交易中的行为负责的能力.缺乏可追究性,电子交易容易引起争议.因此,Rajashekar Kailar提出了一种用于分析电子商务协议中可追究性的形式化分析方法,简称Kailar逻辑.该文指出这一逻辑的缺陷：（1） 不能分析协议的公平性;(2) 对协议语句的解释及初始化假设是非形式化的,存在局限性;(3) 无法处理密文.