电子商务协议形式化分析工具的研究

电子商务协议形式化分析工具的研究作者：丁洁学位授予单位：南京邮电学院相似文献(10条)1.学位论文何加亮形式化逻辑方法在分析认证协议以及电子商务协议中的应用2004计算机网络的出现使世界的联系变得更加紧密。但是，开放式网络上和分布式系统上不断增长的各种应用尤其是电子商务的蓬勃发展，对系统的安全提出了巨大挑战，不能有效地解决计算机网络信息的安全问题，就会影响到计算机网络应用更广，更高，更深的发展。构造安全的计算机系统是一个复杂的体系，其中身份认证系统作为系统安全，网络安全的第一道防线，对整个系统的安全具有非常重要的作用。实现身份认证的方式有很多种，其中最安全的方式是基于密码技术的身份认证协议，但一个好的密码算法并不能保证协议的安全，许多认证协议在公布后被发现有漏洞，因此，如何保证认证协议的安全就成为研究人员的重要任务，在本文中我们研究的不是认证协议的密码算法，而是对协议本身结构的分析，我们采用形式化的逻辑方法来衡量一个认证协议的好坏，分析协议是否安全、高效等等。电子商务迅速发展产生的各种需求需要安全可靠公平合理的交易协议，电子商务安全的核心就是要解决交易主体之间相互信任的问题。电子商务是一种网络交易系统，用以实现电子货币的支付和服务的兑现，本身通过协议来实现。电子商务协议的设计必须满足可追究性原则，即参与交易的双方不能对自己的发出的信息进行否认，但是，电子商务协议是否遵循可追究性原则不仅依赖于所采用的密码算法的安全强度、依然与协议的自身结构有着密切的联系。在交易中我们不仅要满足主体对所分配的密钥的信任要求，更关键的是提出服务要求的主体要确信自己能得到所需要的服务，提供服务的主体也要确信自己能收到应得的电子货币，而作为两者中间的货币中介机构要能向双方提供证明和担保，并实施电子货币的支付。形式化的逻辑方法经过改进依然在分析电子商务协议中发挥重要作用。本文主要是对形式化逻辑方法在分析基于密码技术的认证协议和电子商务协议中的应用作了一些研究。其主要工作如下：1.对形式化分析方法的研究状况作了介绍，指出形式化分析方法能全面的，深刻的分析认证协议和电子商务协议中的设计漏洞。2.根据BAN逻辑对Needham-Schroeder公钥分配认证协议的分析结果，基于协议理想化规则和设计指导原则，本文对Needham-Schroeder公钥分配认证协议作了改进，设计了一个建立在对称密码体制上的认证协议的基本模型，并使用BAN逻辑给予了正确性证明。3.在认证协议中，入侵者在多数情况下是利用协议中的参与主体名称，新的会话密钥，新鲜性标识三者之间的关联关系的漏洞以及协议中出现的结构一致的消息而进行攻击的。本文总结了几条新的指导性设计原则来帮助协议分析者发现协议的漏洞，进而提出改进方法；协议设计者可以遵循这些原则来设计协议，避免一些已被发现的协议错误。4.鉴于Kailar逻辑缺乏对电子商务协议公平性分析功能的缺陷，扩展了其逻辑推理框架，将协议参与主体的局部状态定义成一个三元组，即主体当前相信的公式集合，主体曾看到的公式集合，主体拥有的密钥集合；并提出了几条新的推理规则；此方法可以用来分析电子商务协议的安全性，可追认性以及公平性等属性原则。本文用这种扩展逻辑对Bolignano电子支付协议公平性作了分析，并给出改进办法。5.由于逻辑推理所涉及的大多是符号和规则，此推理过程若要由人工来完成，则无论在人力上，还是在时问上均会造成极大的浪费，根据逻辑推理容易在计算机上实现的特点，我编写了基于这个逻辑框架的Prolog的协议验证系统，用来验证一些认证协议和电子商务协议，对认证协议的验证目标是一级信仰以及二级信仰，对于电子商务协议而言，则分析验证其可追究性以及公平性。其中协议的初始化过程以及协议转换成逻辑的过程由验证者来完成，推理部分则由系统来进行，来达到验证协议是否符合所要达到的目标的目的。6.不可否认性作为电子商务最基本的要求，必须提供不可否认证据的产生、收集和维护机制以防止交易的仔何一方试图对交易中已发生的特定事件或行为的否认。另外，公平性也是电子商务协议必须考虑的因素，它保证交易的任何一方在交易中不能通过作弊手段而取得优于另一方的优势地位。本文根据这两个需求提出了一个公平的，具有不可否认性的电子商务协议，并使用扩展的逻辑分析证明了它的不可否认性以及公平性原则。2.学位论文代新敏网络安全协议的形式化描述与验证2004网络安全协议的设计与分析是当前研究的热点，而安全认证协议和电子商务协议是电子商务不可缺少的关键环节，因此研究电子商务的认证协议和支付协议及其安全性对于促进电子商务的发展是十分重要的。该文以工商年审系统为背景，对电子商务认证和支付协议的设计和分析进行了相应的研究。主要内容：(1)介绍了安全协议、电子商务协议及形式化分析方法的研究状况。(2)对目前的一些典型的安全认证协议，如：Needham-Schroeder、Otway-Rees、Kerberos等进行了简要的分析，阐述了电子商务协议的设计原则，如匿名性、不可否认性、公平性、安全性等，介绍了相关的电子支付协议，并讨论了安全协议设计和分析中所要注意的一些问题。(3)对BAN逻辑、Kailar逻辑两种形式化逻辑证明方法进行了评述。(4)介绍了公钥基础设施PKI，安全认证体系结构标准X.509，安全认证的目录存取协议LDAP。(5)提出了基于X.509的适合于工商年审系统的安全认证协议，并对该协议进行了形式化描述。(6)使用逻辑验证语言进行形式化验证，对认证协议进行了修改，得出了较为完善的协议。并简要阐述了该认证协议在某工商网上年审系统中的应用，为工商年审系统的设计与实施提供了理论基础。该文还将上述完善的认证协议成功地应用于“基于信息安全的通用网络考试平台”软件产品中。3.期刊论文刘义春.张焕国.LIUYi-Chun.ZHANGHuan-Guo电子商务协议的串空间分析-计算机科学2008,35(2)电子商务协议常常具有复杂结构,协议可能由多个子协议组合而成.因此,电子商务协议的安全分析较认证协议更为复杂.传统的信念逻辑不适宜分析电子商务协议.Kailar逻辑适宜分析电子商务协议的可追究性,但不适宜分析协议的公平性.本文介绍并扩展了串空间逻辑,分析了ISI支付协议的串,并证明其不满足公平性.还提出一种新的串节点路径法,用以分析了ASW协议,该协议系由多个子协议组成的分支结构协议,通过串空间分析证明了该协议的公平性.通过对两个协议的分析,分别提供了对电子商务在线交易协议和离线交易协议的形式化分析方法.4.学位论文赵艳春串空间理论在电子商务协议形式化分析中的应用2007电子商务协议是保障电子商务安全的一种重要手段。非否认性和公平性是电子商务协议的重要性质，但相对于认证协议和密钥分配协议的保密性和认证性，电子商务协议及其非否认性和公平性的形式化研究还不够充分。论文对串空间模型的丛理论、诚实理论和认证测试理论进行深入的研究，并在此基础上探讨了将串空间模型应用于电子商务协议安全性形式化分析的方法。为了能反映电子商务协议中加密、签名、完整性保护等多种安全机制，扩展了密码原语，以满足分析复杂安全协议的需要。根据电子商务协议主体利益目标不一致、攻击主要来自内部的特点，扩展了攻击模型，对主体处理消息的能力进行了形式化的定义。为了解决电子商务协议中协议主体动态确定，协议执行路径不唯一确定的问题，扩展了串空间中结点间的因果依赖关系，来描述协议随着协议步骤的不断执行而使协议执行结果发生改变的内在逻辑关联。论文应用扩展的串空间模型对安全电子支付协议SET的安全性进行了较为全面的分析，首次应用形式化的分析方法对SET的保密性、认证性及完整性进行了严格的论证。同时由于SET协议无法满足交易公平性的缺陷，提出了SET协议的一个改进版本，该版本能满足数字商品交易的公平性。5.学位论文谢晓尧基于Petri网和有穷自动机形式化分析方法的电子商务协议研究与实现2004当今时代已进入互联网络的时代,网络的飞速发展给社会带来了巨大的变革,电子商务以及电子政务的蓬勃发展应用就是一个典型的例子.但这种应用及网络的开放性也带来了新的信息安全问题.信息安全已成为影响国家安全、社会稳定和经济发展的重要因素.基于信息安全的电子商务协议的设计和应用,就是为了保证网络和信息的安全.协议涉及到两个方面的内容,一是加密技术的选用,二是协议逻辑的设计.通常加密技术倍受重视而忽略了协议逻辑设计,这就为黑客的攻击,留下了许多隐患和漏洞.针对协议逻辑出现的问题,为保证基于信息安全的电子商务协议设计的正确性,就需要用形式化的分析工具来精确描述和仿真协议的行为、协议所要达到的目标以及能否达到其预期的目标.该论文重点研究了目前流行的电子商务协议的形式化分析方法、基于电子商务安全认证的基本协议和交易协议、以及基于公钥基础设施PKI的安全认证协议.在此基础上,论文的作者完成了如下的工作:①提出了某工商管理部门电子商务的安全认证协议.②创新性地提出了用Petri网理论描述了①的认证协议,建立了该协议的Petri网模型.在此基础上对模型进行了仿真分析,证明了协议存在的隐患和漏洞,并进行了修改.最后得到了较为完善的适合某工商管理部门电子商务的安全认证协议.③提出了某工商管理部门电子商务在完成认证之后要进行交易的支付协议.④根据支付协议的特点,创新性地提出了用有穷自动机理论建立③的支付协议的自动机模型.通过对模型的仿真分析,证明了:·③的支付协议满足可追究性·③的支付协议不满足公平性根据结果,作者提出了同时满足可追究性和公平性的完善的支付协议.⑤作者将上述完善的②、④协议,成功地应用到了基于信息安全的通用网络考试平台软件产品中和某工商管理部门的电子商务中.6.学位论文李志新基于串空间理论的电子商务协议安全性研究2008随着网络通信技术的发展，电子商务已经渗透到人们的日常生活中。电子商务协议的安全性是决定电子商务发展的关键因素之一，也是制约电子商务发展的瓶颈。目前分析电子商务协议安全性的方法主要有BAN逻辑、模型检测和归纳方法等。虽然上述方法都能够较好地分析协议的某些安全属性，但都具有一定的局限性。串空间理论是一种新的分析协议安全性的形式化方法，它充分吸收了前人的研究成果。但是串空间模型最初提出来只限于对认证协议的分析，很少涉及电子商务协议。电子商务协议比认证协议更为复杂，它不仅要满足认证协议的安全需求，还要考虑认证协议中未涉及的若干安全属性，因此有必要找到一种严谨有效的方法来分析电子商务协议的安全性。本文利用串空间理论分析了电子商务协议的安全性，提出了利用串空间模型形式化地描述和验证电子商务协议安全性的思路，设计了一个新的电子支付协议，并验证了该协议的安全性。主要工作包括：(1)在深入研究串空间理论的基础上，提出了利用串空间模型验证电子商务协议安全性的一般性方法，并以著名的电子商务协议—IBS协议为例，通过对其建立串空间模型并引用所提方法对其安全性进行分析，发现该协议的提供服务和传递发票阶段均不满足公平性，得出了与国内外学者用其他形式化方法分析相同的结论，从而验证了串空间模型的有效性和正确性。在此基础上对IBS协议进行了改进，利用串空间理论证明了改进后的协议满足安全性。(2)设计了一个基于同时生效签名的电子支付协议，该协议采用同时生效签名的算法，有利于实现交易的公平性：在交易过程中没有第三方的参与，提高了协议的执行效率，且可用于移动支付。通过对该协议建立串空间模型并进行形式化的分析，可验证其满足秘密性、认证性、公平性、不可否认性及可追究性，因此协议是安全的。(3)基于J2ME平台，利用手机模拟器，开发出上述支付协议的移动客户端。在安全性方面，引用BouncyCastle轻量级加密包，用于客户端移动手持设备对交易信息进行加密运算，保证了端对端的安全性，具有一定的现实意义。7.期刊论文刘英杰.姚正安.LIUYing-jie.YAOZheng-an一种分析安全协议的新逻辑-计算机工程2007,33(23)提出了一种分析安全协议的新逻辑,既能有效地分析认证协议的认证性,又能分析电子商务协议