密码协议安全性分析中的逻辑化方法——一种新的BAN类逻辑

密码协议安全性分析中的逻辑化方法——一种新的BAN类逻辑

李益发[1]2001年在《密码协议安全性分析中的逻辑化方法——一种新的BAN类逻辑》文中研究指明本文探讨了其它BAN类逻辑的缺陷及其产生原因,在此基础上提出了一种新的BAN类逻辑。 首先,本文探讨了BAN类逻辑的缺陷,并对产生缺陷的原因作了细致的分析,提出了作者自己独特的看法。 其次,本文首次阐释、构建了认证逻辑的理论基础。本文构造了一个带有二阶谓词的符号系统,在此基础上建立了一个二阶谓词逻辑公理系统,把该系统看作算术系统和集合论公理系统的扩充,并把认证逻辑看作该系统的一个特殊解释,从而把认证逻辑置于谓词逻辑这一坚实的理论基础之上。 第叁,本文进一步澄清了语义。本文以几个十分简单清晰的命题为出发点,重新刻划了认证逻辑语义,其中不少命题都是本文首次提出的。 第四,本文提出了新的认证逻辑公理系统。本文给出了十八类共四十条公理。这些公理刻划了所使用的一阶谓词和二阶谓词的特点,并且说明了每个公理在“认证逻辑”这一解释下都是成立的,这使公理系统的可靠性得到了保证。 第五,本文对密码协议尤其是身份认证协议和密钥建立协议作了详细的分类,刻划了各类型协议的安全目标,并对协议安全性作了明确定义。本文对所定义的每一类型协议的安全目标都作了统一的公式化描述,进而以是否达到了相应目标为准则定义了协议的安全性。 第六,本文对若干常见密码协议进行了安全性分析。本文主要对身份认证协议和密钥建立协议进行了详细的分析,发现了许多协议是不安全的。此外还对电子选举协议、电子邮件协议和非否认协议等进行了分析,展示了本文的方法有着广泛的适用范围。 本文方法的最大特点是,克服了其它BAN类逻辑在分析协议时需要理想化过程的重大缺陷。

张帆[2]2007年在《无线网络安全协议的形式化分析方法》文中研究说明随着无线网络应用的迅速发展,网络安全的问题日益重要,采用形式化方法设计及分析无线环境下的安全协议得到快速的发展以及广泛的应用。本论文对于安全协议的形式化分析方法从技术特点上做了分类和分析,对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结。具体内容包括:·对形式化分析方法—BAN类逻辑进行了研究,利用BAN类逻辑(WK逻辑),对中国无线局域网安全标准WAPI及其实施方案的认证基础设施WAI进行了形式化分析,指出其中存在的安全隐患,以及能够实现的安全目标。·对基于计算复杂性的方法进行了深入研究;重点研究内容包括:Canetti-Krawczyk模型和通用可组合模型,主要工作包括:1.通过Canetti-Krawczyk(CK)安全模型对IEEE802.11i四步握手协议模块进行了安全性证明。证明表明四步握手协议不仅满足CK模型下提出的会话密钥(SK)安全的定义,并且可以满足更高安全级别的通用可组合(UC)安全的定义,因此该协议可以作为无线局域网中安全的认证和密钥协商基础模块使用。2.利用CK模型,对中国无线局域网安全标准WAPI的认证模型进行了深入分析,针对WAPI中的安全缺陷,提出了一种增强的无线认证协议EWAP。该方案采用模块化及可组合的设计方法,在CK模型下提供了可证明的安全性,并具有相应的安全属性。3.提出了一个适合无线环境下使用的基于双重加密机制的会话密钥分发协议,该协议作为四步握手协议的上层协议,可以保证STA与AP安全共享PMK的目的。利用CK模型,在双重加密机制满足适应性选择密文攻击(CCA2)安全的定义下,对该会话密钥分发协议进行了安全性分析。4.供应链管理是RFID技术主要的应用领域之一,但是目前对该领域基于RFID技术的安全机制还没有较深入的研究。供应链环境对于RFID技术的特定安全需求决定了无法直接应用已有的各种RFID安全机制。定义了供应链环境下RFID通信协议必须满足的安全需求,提出了一个可以满足这些安全需求的通用可组合安全模型,并且设计了一个可以实现该模型的轻量级RFID通信协议。5.利用通用可组合安全模型定义并实现了一种适用于无线网络的匿名Hash认证理想函数,并在此基础上定义了一个具有普遍意义的Hash证书权威模型。定义了匿名Hash认证机制的安全需求和安全概念,并且证明在标准模型(非随机预言机模型)下所提匿名Hash认证机制的安全属性可以通过安全对称加密机制、安全数据签名机制、伪随机函数以及单向无碰撞Hash函数的组合得到保证。·最后,本文对安全协议的形式化分析方法的最新进展—协议组合逻辑PCL进行了深入研究,设计了一个基于RFID的供应链通信协议可以实现所定义的安全需求和可见性要求,并且用PCL给出了形式化的安全证明。

邓帆[3]2010年在《基于SPALL逻辑的安全协议设计与分析》文中指出随着网络技术的发展,网络应用已经日益渗透到人们生活的方方面面,网络在给人们带来巨大便利的同时也带来了一些不安全因素。安全协议是以密码学为基础的消息交换协议,其目的是在网络环境中提供各种安全服务,其中最基本的包括协议参与者身份的认证和参与者之间会话密钥的建立。安全协议是网络通信和应用必不可少的组成部分,是构筑信息安全体系的基础。但实践证明,即便是一个简单的协议,其设计也是不容易的,需要利用形式化的方法来指导安全协议的设计。本文探讨了基于构件的规范化的安全协议设计和分析方法,提出了运用组合方法进行安全协议的模块化设计。首先,该文给出协议中基件与组件的定义。其次,分析组件的安全属性并基于组件设计能实现相应安全目标的单步协议。最后,定义组合规则确保不同的单步协议能够组合成为一个复合协议的同时各个单步协议还能实现各自的安全目标。至此,根据具体的应用背景选择合适的单步协议按照组合规则组合后便可得到满足需求的安全协议。该方法可将一个复杂协议分解为若干基于组件的简单单步协议,使得协议的设计与分析都易于实现。具体而言,本文的主要研究工作有:(1)针对对称和非对称环境下的若干组件,本文运用SPALL(Security Protocol Analysis Latent Logic)逻辑分析了这些组件所具有的安全属性,同时基于这些组件设计了与其对应的若干单步协议。本文还定义了单步协议的组合规则,并逻辑化地给出了证明,通过选择合适的单步协议按照组合规则组合后便可得到所需协议,最后以对称及非对称环境下的双向认证协议和密钥协商协议的设计为例说明如何运用该方法设计安全协议。(2)以安全支付协议的设计为例说明了如何运用该方法进行复杂安全协议的设计,拓展了模块化设计方法的应用范围。同时,设计了标准模型下可证安全的认证密钥协商协议,该协议具有良好的前向安全性和密钥无托管性,通过用户间的显式认证,提高了协议成功运行的效率。与随机预言模型中的协议相比,在计算和通信效率方面相当。在对协议的安全性分析中,给出了可证安全的证明与逻辑化的分析,比较了两种方法各自不同的证明思路及过程。(3)在安全协议的形式化分析中,有两种完全不同的观点:模态逻辑和可证安全,两者各有优缺点。目前,将两者进行组合优化,建立统一的调和方法框架对安全协议进行分析是研究的热点和难点。本文通过对两种观点的研究,按照优势互补的原则将两者相调和,提出了一种折衷的形式化分析方法,该方法可提供更为完全的安全协议形式化分析。安全协议的形式化设计研究能够促进安全协议设计的自动化,以满足不断增长的安全协议应用需求,不但具有重要的研究价值,而且对于解决安全协议难于设计的问题有着重要的现实意义和广阔的应用前景。通过不同环境下多个安全协议的设计实例,本文所提出方法得到了有效的论证,然而,该方法并不旨在覆盖所有的安全协议设计,更多的在于提供一种新的安全协议设计思路。

石曙东[4]2009年在《网络协议安全性分析中的逻辑化方法研究》文中研究说明安全协议是建造网络安全环境的重要基石,是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性,成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法,对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击,但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善,存在一定的局限性,不能分析和验证某些类型安全协议的安全性:有些只能分析安全协议的不安全性,不能给出协议安全性的精确证明。在总结安全协议现存各种缺陷的基础上,根据缺陷产生各种原因将缺陷分为:过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为:重放消息型攻击、猜测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定型攻击等六类。Burrows,Abadi和Needham提出的BAN逻辑开创了用逻辑化方法分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象,逻辑处理的符号集是对现实具体协议的抽象;其初始假设、断言集合等均是从现实世界中抽象出来的要素。因此,其狭窄的符号集合定义也就决定了该方法存在不能分析某些类型协议安全性的缺陷,如:不能发现由于时间同步问题而导致的协议缺陷。另外使用BAN逻辑对安全协议分析时,很多初始假设是不合理的,如消息不可伪造假设就非常不合理,这些假设的不合理,妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷;语义不清晰缺陷;非严密的环境模型缺陷和无法有效预测对协议存在的攻击等缺陷。1995年由Raiashekar Kailar提出的Kailar逻辑主要用于描述和分析电子商务协议,但是它只能分析电子商务协议的可追究性,无法分析电子商务协议的另一个重要特性——公平性。与BAN逻辑一样,使用Kailar逻辑分析协议之前同样需要引入一些初始假设,而初始假设的引入仍然是一个非形式化的过程,具有一定的人为性,其不准确会导致安全协议分析的失败。另外,用Kailar逻辑解释协议语义时,只能解释签名的明文消息,这样限制了其使用范围,对某些安全协议不能分析。针对BAN类逻辑和Kailar逻辑的弱点,设计了一种新的安全协议分析逻辑CPL(Cryptographic Protocols Logic),CPL不但可用于分析协议的安全性,还可用来设计安全协议,即CPL逻辑把分析和设计安全协议纳入同一个逻辑体系中,消除了用不同方法分别设计和分析安全协议,将导致结果不一致性的缺陷,同时也简化了分析和设计安全协议时对初始条件和安全协议最终目标分别进行形式化的过程和步骤,提高了分析和设计安全协议的效率。定义了CPL逻辑的基本符号、给出了CPL逻辑用于分析协议安全性的六类二十五条逻辑分析规则和用于设计安全协议的二十九条逻辑设计规则。分析规则和设计规则可分别用于安全协议的分析和安全协议的设计。给出了基于Kripke的CPL逻辑的语义,并利用逻辑语义对CPL系统自身的正确性进行了详细证明。运用新逻辑的分析规则和协议运行的初始条件以及安全协议的执行步骤分析安全协议的安全性。运用新逻辑的设计规则和协议运行的初始条件以及协议的最终目标设计出满足安全要求的安全协议。使用新逻辑分析了两个不同类型协议的安全性——密钥建立协议和身份认证协议。

董玲[5]2008年在《密码协议工程与基于新鲜性的协议安全研究》文中进行了进一步梳理密码协议的安全性研究是网络安全研究的主要热点。本论文主要研究了如何应用系统工程思想和形式化方法来分析和设计密码协议,取得的主要研究结果如下:1.将系统工程思想引入密码协议设计,结合前人的研究成果,提出了10条密码协议工程原则:5条安全需求分析原则,4条详细设计原则以及1条安全性证明原则。将密码协议设计看作密码协议工程,从协议设计的不同阶段给出原则,是帮助研究人员按系统工程思想进行密码协议设计的有益尝试。实例分析表明,这些原则不仅较为完备,而且可操作性强,能帮助研究人员明确协议设计背后的隐含假设,发现和避免协议设计中的漏洞,简化协议设计。2.首次提出基于信任的新鲜性标识符分析密码协议的安全性,给出了新鲜性原则:对每个通信参与主体而言,密码协议的安全性取决于发送或者接收的、包含自身已相信新鲜的新鲜性标识符的单向变换。该原则找到了一条快捷、有效的密码协议安全性分析方法,论文示例了20多个经典密码协议的分析结果,分析出的针对协议的攻击或者安全隐患有12个是以往没有指出过的。新鲜性原则的特点是:①能有效区分消息是否新鲜,安全性的分析独立于并发运行环境的具体形式化描述,也独立于攻击者能力的具体形式化描述;②基于该原则得到的分析结果能够证明正确协议的安全性,也能够分析出不安全协议存在的安全属性缺失,以及由该缺失直接构造攻击的结构。3.基于新鲜性原则,提出了基于逻辑推理的信任多集形式化分析方法。以Needham-Schroeder公钥认证协议为例,说明了该分析方法的有效性、严谨性和自动化实现的可能。另外,针对无线网络的开放性和数据包易失的特点,扩展了信任多集方法,能有效用于无线密码协议分析。4.证明了保证认证协议安全的充分必要条件,这些条件在计算模型下分别满足基于匹配对话和不可区分性的4个可证安全定义。5.提出了信任多集自动分析工具的总体框架,通过在2种不同开发环境下信任多集自动分析工具初步实现的比较,给出了信任多集自动分析工具的详细设计。正在开发的信任多集自动分析工具已成功实现了对若干密码协议的安全性分析。6.基于新鲜性原则和因果一致性的分布式逻辑时间,建立了信任多集形式化设计方法。构造了一个公钥认证协议,并证明了该协议达到了消息数和轮数的下限。

鲁来凤[6]2012年在《安全协议形式化分析理论与应用研究》文中指出安全协议是一种运行在计算机网络或分布式系统中、借助于密码算法来达到密钥分配和身份认证等安全目标的通信协议,是解决计算机网络和分布式系统中安全问题的必要手段。然而,安全协议未必是安全的,它的安全性分析一直是一个复杂而困难的问题,对安全协议的研究已成为世界上信息与网络安全方面的一个重要研究方向。实践证明,形式化方法是安全协议安全性分析更为可靠和有效的途径。本文以安全协议作为研究对象,以DDMP理论为研究工具,对安全协议形式化分析方法从理论和应用两个层面展开研究,所取得的研究成果主要有:(1)设计了安全协议形式化分析模型。给出了安全协议的系统模型,设计了安全协议形式化分析的一般模型SPFAM和基于DDMP理论的安全协议形式化分析模型DDMP-SPFAM。在模型图的基础上,给出了相应的模型算法,具体阐述了形式化分析遵循的步骤,对安全协议的形式化分析和设计提供了宏观指导。(2)研究了基于协议组合逻辑(PCL)的形式化分析方法。给出了基于PCL证明协议安全属性的一般方法,选取国际标准ISO/IEC DIS11770-3中提出的重要认证协议Helsinki作为研究对象,讨论了该协议存在的缺陷及受到的攻击,改进协议,利用PCL对改进的协议方案进行形式化建模,并进行安全性证明。改进型的Helsinki协议基于PCL是安全的。(3)研究了安全协议的组合性问题。讨论了基于符号和基于计算复杂性的形式化分析领域中协议组合分析工具的代表PCL与UC,选取PCL作为协议组合分析的工具;详细阐述了PCL进行组合分析的过程;选择典型的包含可信第叁方的密钥交换协议Otway-Rees展开讨论,分析了协议本身的缺陷及其遭遇到的攻击形式,提出了改进方案(AOR协议);扩展PCL,利用PCL对改进后的AOR协议进行了形式化建模和模块化安全性证明。AOR协议能满足密钥保密属性。(4)从非形式化和形式化两个方面研究了安全协议设计方法。在非形式化方面,针对安全协议设计规范、原则展开讨论;在形式化方面,阐述了协议演绎系统PDS的设计思路和具体方法,针对现有PDS主要基于无可信第叁方参与的公钥密码体制下的安全协议演绎现状,设计出新的协议组件和操作集合,扩展了PDS系统,设计了一系列安全协议。

王滨[7]2004年在《公钥密码协议的形式化分析与设计研究》文中提出目前,密码系统中大量地使用基于公钥的密码协议,这些协议的安全性直接影响着网络系统的安全。一个安全的网络系统要求主体能够实现相互间的身份认证和建立并交换会话密钥,但是密码协议的设计是非常容易出现错误的,而且这些错误是很难被发现的。研究如何检测密码协议中存在的安全漏洞并加以改进,是密码学的一个重要研究领域。迄今为止,已经有很多方法用来检测密码协议中的安全漏洞,其中最着名的是由Burows,Abadi,Needham提出的BAN—逻辑形式化分析方法,以及以BAN—逻辑为基础的一系列BAN类逻辑分析方法,但是这些方法都具有其局限性,而且大都应用于对称密码体制设计的密码协议。 本文对基于公钥密码体制的密码协议的设计与分析方法进行了研究,取得了如下结果: 1.提出了基于实体认证和密钥认证模型的协议分析方法,该方法以确定协议的模型和目标为基础,实现对协议的安全性分析; 2.对基于公钥的密码协议进行原型抽象和分类,给出了基于协议原型的协议设计方法; 3.提取了Diffie-Hellman密钥交换协议抽象原型,分析了该协议原型的的前向保密性特点,继而利用单向函数和公钥密码体制,设计了一个具有前向保密的新的密码协议原型; 4.给出了一个抵抗拒绝服务攻击(DoS)的协议设计策略,设计了一个基于口令认证的强身份认证协议,并利用我们提出的协议分析方法,分析了该协议的安全性。

梅翀[8]2008年在《基于Petri网的安全协议分析与检测方法的研究》文中指出随着Internet技术持续突飞猛进地发展,网络上的信息安全问题日益突出。特别是电子商务、数字货币和网络银行等新业务的深入开展,信息的保密性、完整性和可用性等安全问题成了关键之所在。安全协议,又称密码协议,是以密码学为基础的协议,它在网络和分布式系统中提供各种各样的安全服务。安全协议的目标都与安全有关,例如,认证主体的身份;在主体之间分配会话密钥等。目前,安全协议已广泛应用于计算机网络与分布式系统中,当前关于安全问题的研究热点之一是安全协议的形式化描述与分析。目前安全协议常见的分析方法包括:逻辑方法、模型检测、定理证明等方法,它们都有各自的优点和缺点。本文主要研究以Petri网模型为基础融入其他方法,提出一种新的协议建模及分析检测方法,并使用该新方法对安全协议进行了分析检测,以验证其有效性。本文的主要创新点及研究成果如下:1.提出了一种新的安全协议建模方法,此方法根据通信主体的叁态建立的协议模型具有意义明确、便于分析等特点。2.目前国内外很多学者使用petri网分析安全协议时,往往是通过验证协议的不安全状态是否可达,来判断协议的安全性。而本文所提出的方法是从协议的初始状态出发去检测可能存在的攻击。3.在协议分析检测过程中,本文创造性地融入了其他分析方法,构建了各个通信主体分析集。4.本文研究制定了主体分析集更新规则、攻击检测规则。5.本文使用了该新方法对多个经典协议进行分析检测,并找到了可能存在的攻击。

高悦翔[9]2013年在《电子商务安全协议的设计与形式化分析》文中研究表明随着计算机网络的飞速发展,电子商务逐渐成为人们进行商务活动的新模式。电子商务安全协议是构建电子商务安全环境的基础,是保障电子商务顺利应用与发展的关键技术。电子商务安全协议是以密码学为基础的消息交换协议,参与者采取的一系列步骤去完成某一任务,其目的是在网络信道不可靠的情况下,确保通信安全以及传输数据的安全。电子商务安全协议除了需满足传统安全协议所需满足的认证性、保密性和完整性外,还需满足可追究性、公平性、时限性及匿名性等安全属性。因此电子商务安全协议的设计与分析面临着诸多困难和挑战,也成为了信息安全领域中的一个重要课题,具有重要的理论意义和现实应用价值。本文主要围绕电子商务安全协议的设计以及形式化分析技术展开研究,取得了些研究成果。对电子商务安全协议的基本概念、分类及其安全属性进行了综述和分析,对电子商务安全协议安全性设计及形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。指出了一个认证电子邮件协议在可追究性和公平性上存在的安全缺陷,在此基础上提出了一种基于在线第叁方的认证电子邮件协议,以满足认证电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放等攻击、及第叁方无法获得邮件内容等优点。采用组合协议分析方法及PCL逻辑分析了ECS2协议的弱公平性。指出了ZZW协议存在不满足保密性、可追究性和公平性的安全缺陷,并提出了改进方案。提出一种结合组合协议分析以及Kailar逻辑的分析思路,用于分析基于离线第叁方的电子商务安全协议的可追究性及公平性,并分析了改进后的ZZW协议,证明了该协议能够弥补原协议的安全隐患。针对移动环境中网络及计算条件受限的情况,在考虑有效性和支付效率的基础上,设计了一个适应于移动环境的公平移动支付协议。该协议由认证、支付、恢复、结算四个子协议构成。在认证协议中通过基于Hash函数的动态ID机制满足了双向认证、有限的匿名性和不可追踪性,并获取不可伪造性的、可重用的支付证书。在支付过程中基于变色龙Hash函数和双Hash链,实现了交易的匿名性、可追究性和公平性。最后利用Kailar逻辑对协议的可追究性和公平性进行了形式化分析,结果表明,协议在保持较高执行效率的同时能满足可追究性和公平性,适用于在移动环境以及类似的通信、计算条件受限的环境中使用。针对一般信念逻辑难于分析乐观公平交换协议的公平性和时限性的现状,将乐观公平交换协议定义为类似于Kripke结构的状态转换系统,对扩展Kailar逻辑增加了时间限定条件及状态转换分析。在分析不可否认证据有效性的基础上,通过考察主体认知及信仰的转换过程,达到分析乐观公平交换协议的公平性和时限性的目的。同时,对一个典型的乐观公平交换协议进行了分析,发现了该协议存在的两个安全缺陷,并给出了改进方案。指出了一个典型的多方认证邮件协议存在不满足公平性、可追究性以及个别不诚实参与方行为会导致整个协议执行失败等安全隐患。基于签密方案,对该协议进行了改进,并利用Kailar逻辑对改进后的协议的安全属性进行了分析。研究结果表明,该协议能够满足保密性、不可否认性及公平性,并具有抗篡改、重放、合谋等攻击的特点。本文的研究工作对于电子商务安全协议的设计以及形式化分析技术有一定的理论和实用意义,同时对于提高电子商务活动的安全性也具有一定的价值。

王力民[10]2007年在《IKE的分析及其基于CPK的改进》文中认为在众多的安全协议中,IPSec是因特网的基础协议,IPSec是IPv6中负责数据通信安全的部分,而IKE又是IPSec协议簇的重要内容,负责密钥的协商和管理。因此对IKE的安全性进行分析不仅具有理论意义,而且具有实用价值。鉴于IKE的重要性,论文的主要工作是对其进行的分析和改进。首先,对各种协议分析方法作了比较,并选择逻辑化方法作为分析工具。而后对逻辑化方法作了改进——增加和修改了若干公理,并证明了新的定理。其次,用逻辑化方法详细地分析了IKE(IKEv1和IKEv2)的安全性——对IKEv1第一阶段主模式的叁种认证模式(预共享密钥模式、数字签名模式、公钥加密模式)、第二阶段的快速模式和IKEv2都进行了详细的形式化分析。分析表明,IKEv1和IKEv2协议都是安全的。同时,也指出了IKE在效率方面的弱点。最后,为了提高IKE的效率,给出了基于CPK的IKE的改进方案。CPK的用户公钥由用户名来确定,证书与用户名之间存在一一对应关系。由于私钥是面对面分发,或由单位统一申请、分发,是一种直接的信任关系,可信度较高。而且,用户公钥的确认除了查询黑名单列表时需要访问中心外,其它的验证只需用户有本地主机上作一次查表即可,因而效率较之原协议有明显的提高。此外,逻辑化分析也表明,改进的协议具有较高的安全性。诚然,IPSec有其自身的优势——更好的开放性。所以,我们的方案并不是要完全取代IPSec协议。一般而言,在无边界的开放网络中,更适合用现有的IPSec协议。但在封闭的网络,如军事网、电子政务网中,我们方案则具有明显的优势。

参考文献:

[1]. 密码协议安全性分析中的逻辑化方法——一种新的BAN类逻辑[D]. 李益发. 解放军信息工程大学. 2001

[2]. 无线网络安全协议的形式化分析方法[D]. 张帆. 西安电子科技大学. 2007

[3]. 基于SPALL逻辑的安全协议设计与分析[D]. 邓帆. 解放军信息工程大学. 2010

[4]. 网络协议安全性分析中的逻辑化方法研究[D]. 石曙东. 华中科技大学. 2009

[5]. 密码协议工程与基于新鲜性的协议安全研究[D]. 董玲. 上海交通大学. 2008

[6]. 安全协议形式化分析理论与应用研究[D]. 鲁来凤. 西安电子科技大学. 2012

[7]. 公钥密码协议的形式化分析与设计研究[D]. 王滨. 解放军信息工程大学. 2004

[8]. 基于Petri网的安全协议分析与检测方法的研究[D]. 梅翀. 贵州大学. 2008

[9]. 电子商务安全协议的设计与形式化分析[D]. 高悦翔. 西南交通大学. 2013

[10]. IKE的分析及其基于CPK的改进[D]. 王力民. 解放军信息工程大学. 2007

标签:;  ;  ;  ;  ;  ;  ;  ;  ;  ;  

密码协议安全性分析中的逻辑化方法——一种新的BAN类逻辑
下载Doc文档

猜你喜欢