电子邮件协议的非否认性形式化分析

非否认性是考量电子商务协议的重要方面。SVO逻辑以其简洁的特点在协议的安全性验证方面被广泛应用。本文通过对SVO逻辑分析推理规则进行扩展,将其运用到对电子商务协议的非否认性的验证上,对CMP1进行了形式化分析。形式化分析的结果表明CMP1满足非否认性。     

改进的可证安全的相互认证及密钥协商方法

提出一种新的用于移动通信的相互认证和密钥协商方法——NMAKAP。NMAKAP采用基于阿贝尔群的模幂运算和散列函数进行身份认证,取代了传统公钥密码算法和数字签名方案,降低了协议的计算开销和实现成本。在SVO逻辑系统证明下,NMAKAP协议是安全的。SVO逻辑是安全协议形式化分析的一种重要方法,文章扩展了SVO逻辑分析散列函数的逻辑语法。SVO逻辑方法的认证目标被发现存在中间人攻击,为此提出了新的认证目标,并分析了新目标的安全性。分析了一种可用于移动通信的认证协议——MAKEP。MAKEP协议通过预计算,大大降低了移动设备的计算量,但被认为存在Hijacking攻击。分析表明针对原MAKEP协议的Hijacking攻击并不成立,但该协议被发现存在未知共享密钥攻击,为此提出了改进意见。     

不可否认协议时限性的形式化分析

虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质.     

一个新的公平非否认协议

在安全数据传输协议中，发送方和接收方的非否认性及公平性非常重要。通常可以通过采用数据传输中的双方非否认协议来达到这个目的。在克服CMPI协议缺陷的基础上，提出了一种新的公平非否认电子邮件协议。经过使用改进的Kailor逻辑分析验证，新的协议满足非否认性和公平性原则，可广泛应用于电子邮件、电子合同等电子商务应用中。     

非否认协议中认证保密性的设计与形式化分析

探讨了非否认协议的保密性认证目标,用攻击的方法验证了A(0)协议在认证保密性方面的不足;对其消息格式和会话密钥建立后确认方式做了修改,提出了NA(0)协议;进一步运用SVO逻辑对NA(0)协议进行了形式化的分析,验证了NA(0)协议满足主体身份的认证性和会话密钥的保密性.     

基于SVO逻辑的3G AKA协议形式化分析

AKA协议是3G通讯中的一个重要安全协议。利用SVO逻辑对该协议进行形式化分析,以期发现其是否存在安全缺陷。运用信息隐藏的方法对该协议的缺陷进行了修正。另外指出SVO逻辑不能分析协议运行中的关键性明文对协议安全性的影响,以及不能分析旁听攻击这两个新的缺陷,并对SVO逻辑进行了扩展。     

一种高效的无线移动网络安全协议*

无线移动网络具有节点资源受限的特点,为其设计和实现高效而可靠的安全协议很困难.基于可信第三方和fail-safe协议,提出了一种适合于资源受限网络环境的安全协议.利用SVO逻辑对协议的安全性进行了形式化验证.     

一种离线TTP公平非否认协议的安全性分析方法

给出了一种离线TTP公平非否认协议的分析方法,离线TTP公平非否认协议得到了广泛的研究,针对离线TTP公平非否认协议的分析并不是那么广泛.针对离线TTP公平非否认协议具有协议簇的特点,将协议实例化,实例化后可以对单个协议实例的非否认性和有效性进行分析;通过扩展Kailar逻辑,增加时间相关限定词来表述协议的执行序列,用协议执行序列来表达和分析协议的公平性和时效性.利用该方法,对两种公平非否认协议进行分析,分析的结果表明CCD不符合公平性,而ZG的时效性不能够得到满足.     

基于改进语义SVO逻辑的二维认证协议分析

一种基于二维几何距离的实体认证协议无需在非安全信道当中传送密钥,使得认证的过程更加安全与便捷,然而该协议的正确性与安全性并未得到严格论证。考虑该实体认证协议的特点,采用改进语义的SVO逻辑对其进行合理性描述,并对其运行过程进行形式化的具体分析,发现该协议在认证过程中存在着双方认证不确定的缺陷。针对此缺陷提出了一种修正方案,以确保认证协议的正确性,并且通过改进语义SVO逻辑的形式化分析证明了该改进认证协议的安全性。     

Kailar逻辑的改进及应用

综合Kailar逻辑和SVO逻辑两种协议分析方法的优点,借助SVO逻辑的思想对Kailar逻辑进行了改进,使其更好地应用于不可否认协议的可追究性分析和设计。同时,将改进后的Kailar逻辑应用在类NG协议的分析中,分析结果证明了该协议可追究方面的安全性质。     

公平的多方不可否认协议

电子商务中保证信息交换的不可否认性是一项必不可少的安全服务,而多方不可否认协议则是当前的研究重点之一。论文通过分析当前已发表的多方协议或方案,指出当前多方不可否认协议存在由于发送方占优势导致的不公平问题,并提出了基于双重组加密方法的多方不可否认协议,进一步削弱了发送方的优势。最后用SVO逻辑的形式化分析方法证明了协议的正确性。     

SaaS模式下新型认证方案的设计与分析

针对软件即服务(SaaS)应用系统下认证协议的应用及安全性问题,提出一种新型认证方案。通过加密用户口令,将散列结果传输到网络上,只有服务器私钥才能解密,从而实现客户端及服务器双向认证一次性口令技术,提高认证系统的安全性。采用SVO逻辑对该协议进行形式化分析,结果验证了其安全性。     

电子商务支付协议认证性的SVO逻辑验证

与证伪法（如模型检测）相比,采用证真法（如定理证明和逻辑推理）能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。     

一种改进的A(0)协议及其形式化分析

针对A(0)协议不能抵抗重放和伪冒攻击的不足,在修改原协议的消息格式和增加握手确认消息的基础上,提出了一种A(0)协议的改进方案,并应用SVO逻辑对改进后的协议进行了形式化的安全性分析。改进后的协议在保持原协议简洁、高效优点的基础上,增加了抵抗重放和抵抗伪冒攻击的能力。     

普适环境下的一种跨域认证机制

由于普适计算的高度移动性,通信的双方经常位于不同的区域,为了保证服务的合法访问以及消息的安全传输,需要进行跨域认证以及安全会话密钥建立。提出了一种新的跨域认证与密钥建立协议,该协议采用生物加密技术省去了证书管理的负担,合理设计了通信双方及其各自服务器之间的交互,完成了跨域双向认证,并采用签密技术为通信双方派生密钥。对协议进行了安全及性能的分析,并用经典的SVO逻辑证明了其正确性。     

适应受限环境的认证协议及其SVO逻辑分析

针对认证协议在受限通信网络环境中的应用和安全问题,提出一种基于椭圆曲线密码技术的认证协议,使用对称密码为协议中的交互信息提供机密性,在协议最后生成参与者共享的会话密钥。采用扩展的SVO逻辑对推荐协议进行形式化分析,结果证明该协议的安全性符合要求。     

3G中安全增强的AKA协议设计与分析

提出了3G安全保密系统框架,设计了安全增强的认证与密钥协商协议,并对其进行了基于SVO逻辑的安全性分析。结果表明,SE-AKA协议在永久身份保密、双向认证、不可否认性等方面的安全性都优于3GPP-AKA协议,使UMTS接入网络能够抵抗改向攻击和主动攻击。而且协议中消除了重同步机制,避免了序列号操作困难带来的危害。这些安全功能满足了3G环境下特殊部门高级别的安全需求。     

基于攻击者行为能力的SVO协议分析

SVO原逻辑不适用于证明基于证书的认证与密钥交换协议安全性问题。为此,提出2个SVO逻辑相关公理,对证书真实性与会话密钥安全性进行判断及验证,并结合Dolev-Yao安全模型,从攻击者行为能力的角度评估密码协议的安全性。经分析证明Mangipudi协议未能提供前向安全且存在假冒攻击的安全缺陷,因此给出一个在Dolev-Yao安全模型下可证明安全的解决方案。     

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

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