Kailar逻辑的缺陷及改进

近年来,电子商务协议的设计逐渐成为热点。Kailar提出了一种用于分析电子商务协议中可追究性的形 式化分析方法,简称Kailar逻辑。指出这一逻辑的缺陷:在发生重放攻击时不能正确分析各方面的责任,在验证 协议是否满足公平性原则时,具有一定的局限性。针对上述缺陷提出改进措施。

Kailar逻辑的串空间语义

Kailar 在1996年发表了“电子商务协议中的可追究性”一文,使得电子商务协议的形式化分析得到了重大的发展。但是 Kailar 逻辑的语义一直没有人提出来过,而逻辑的语义对于逻辑的正确性是至关重要的。本文的主要工作就是给出了 Kailar 逻辑的串空间语义,从语义的角度证明了 Kailar 逻辑的规则的正确性。

Kailar逻辑推理中初始状态假设

Kailar逻辑用于分析电子商务协议的可追究性,但初始状态假设引入不当会导致Kailar逻辑分析协议失败.通过对利用Kailar逻辑证明CMP1(b)协议与CMP1协议可追究性的过程以及对初始状态假设进行分析研究,针对初始状态假设所存在的问题,给出了初始状态假设应遵循的两个原则.实例表明,遵循该原则能够发现初始状态假设存在的问题,从而修正不适当的假设、补充新的假设,避免其引入不当所导致的Kailar逻辑分析协议失败问题.

一种分析电子商务协议的新工具

提出了一种新的形式化分析方法 ,可用于分析电子商务协议 .与 Kailar逻辑相比 ,它有 3个优点 :(1)能够有效地分析协议的公平性 ,在进行公平性分析时充分考虑了通信信道的可靠性 ;(2 )初始化拥有集合只依赖于环境 ,不需要人为地引入初始化假设 ;(3)增加了密文理解规则 ,能够有效地分析包含有签过名的加密公式的消息 .

一种安全高效的在线移动支付协议

针对现有移动支付中客户端有限的功耗、处理能力及安全性等问题,提出了一种安全高效的在线移动支付协议。该协议采用客户与银行共享的离线伪随机数作为密钥进行高效认证,能实现高效身份认证及会话密钥协商。客户与商家交易过程中采用共享密钥加密敏感信息,能有效减轻客户端计算开销及实现非否认性。经过效率分析比较及BAN逻辑证明,该协议能以较低的计算及通信量获得较高的安全性,非常适合在移动终端上实现。

基于ATL的电子商务协议建模与形式化分析

LTL和CTL等由于把协议看成封闭式并发系统进行研究,不能有效描述协议与外部环境的联系.引入一种新的基于博弈逻辑的ATL分析方法,能够对日益复杂的多方电子商务协议进行建模与分析.利用新方法对Markowitch和Kremer提出的多方非否认协议进行建模与严格的形式化分析,发现该协议存在的不公平性问题并提出改进方法.

一种分析电子商务协议的知识与信念模型

针对现阶段电子商务协议形式化分析的处理比较混乱、表述精确度不高且通用性较差、存在一些不合理的假设等问题,运用现代模态逻辑理论,结合知识与信念,提出了一种分析电子商务协议的模型:知识与信念模型。该模型主要包含安全环境、知识集、信念集、能力集、切入点和知识化等因素。知识与信念模型很好地解决了上述问题,能够细致、精准地对各种电子商务协议进行形式化描述,并为不同的分析方法提供了模型支持。

验证电子商务协议的新逻辑分析方法

通过典型实例分析,发现并指出SVO逻辑在验证电子商务协议中存在的缺陷,并在此基础上,充分考虑交易信道的可靠性和交易实体的诚实情况,对其分析框架进行扩展,提出一种验证电子商务交易协议的新逻辑分析方法.新逻辑分析方法符合电子商务协议运行特征,不仅可以静态验证协议的不可否认性,而且可以动态验证协议的公平性.同时,对协议的分析只依赖协议的运行环境,不需人为引入初始化假设,是一种更为严密的形式化分析方法.最后,以经典协议对新方法的正确性、有效性进行验证.

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

提出了一种新的形式化分析逻辑 ,可用于分析协议的安全性 .它有 3个优点 :(1)能分析协议的可追究性 ,(2 )能分析协议的公平性 ,(3)能有效的分析协议能否抵御重放攻击 ,(4 )增加了密文理解规则 。

网络安全的三道防线一密码、协议和防火墙(英文)

讨论了密码、协议和防火墙边三道网络安全防线。首先评价了美国国家标准技术局颁布的15个先进加密标准的候选算法，从中可以看出密码的发展趋势。然后重点探讨了电子商务协议的逻辑分析。最后介绍了超级防火墙的新思想及其功能和设计原理。

电子支付协议安全性的形式化分析

本文用Kailar逻辑对Bolignano电子协议的安全性作了较为详细的分析 ,进而对Kailar逻辑也作了一些讨论。

一种新型的电子商务协议及形式化分析

该文提出了一个可运行在不安全、不可靠信道上的电子商务协议NRP,该协议可使通信双方处于平等的地位,并有效地防止欺骗行为的发生。通过使用扩展BAN逻辑有效地分析了NRP协议的正确性,对电子商务协议的设计和分析具有重要的指导作用。

移动电子商务的电子支付模型研究

电子支付技术是电子商务中的核心技术 ,也是目前制约电子商务发展的一个根本性问题 ,移动电子商务也不例外。文章对移动电子商务中的支付体系进行了深入的探讨 ,提出了适合移动电子商务发展的 M SET移动支付模型 ,并用 BAN逻辑对其安全性进行了验证。

一个新的电子支付协议及其形式化分析

在安全电子支付协议中,付款方和收款方的可追究性及公平性非常重要。通常可以采用电子支付中的双方可追究协议来达到这个目的。在克服ISI支付协议缺陷的基础上,提出了一种新的公平可追究电子支付协议。经过使用改进的Kailar逻辑分析验证,新的协议满足可追究性和公平性原则。

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

当前,高效、安全的支付方式已成为移动电子商务发展的首要问题。但目前移动电子商务研究中对移动支付协议的设计尚不健全,如何对移动支付协议认证备受关注。本文浅析电死商务协议认证中SVO逻辑验证的应用。

一种新的复合型电子支付协议及其形式化分析

针对现有复合型支付协议AECPP的单向身份认证中易受匿名攻击、支付子协议的完整性不能有效保证这些不足,提出一种新的复合型电子支付协议。新协议实现了用户与服务供应商之间的双向认证,通过引入Hash函数和经由第三方信息的转发进一步提高了支付子协议的完整性和保密性。通过SVO逻辑和Kailar逻辑形式化分析验证可知,新的复合电子支付协议满足双向认证性、可追究性和公平性。

面向第三方支付平台的移动安全交易协议研究

为提升移动支付交易安全性和质量,该文致力于设计一种能够在移动终端上搭载的面向第三方支付平台的安全交易协议模型STPT。该协议保留了SET协议及MSET协议双重签名的特性,用对称算法替换了大部分非对称算法环节,显著提升了计算效率,降低了计算量和计算时间,使其能够在移动终端上实现搭载。通过改造MSET协议的初始化流程,显著强化了协议整体的安全性并使其具有明显的不可否认性特征。基于对SET协议和MSET协议的分析,提出STPT模型,并对其可认证性、保密性、完整性、不可否认性、原子性进行分析,证明其能够提供较为全面的安全性服务。并运用Kailar逻辑证明其能够达到预定的安全目标。