李梦君[1]2005年在《安全协议形式化验证技术的研究与实现》文中认为协议是指两个或者两个以上的参与者为完成某一项特定任务相互约定的执行步骤和执行规则。协议的定义包含叁层含义:(1)协议至少有两个参与者;(2)协议在参与者之间表现为消息交换和消息处理交替进行的一系列步骤;(3)协议的执行是为了能够完成某项任务或达成某种共识。 安全协议就是建立在密码体制基础上的—种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。 安全协议的正确性对网络应用的安全至关重要。安全协议攻击者的破坏和安全协议无穷多个会话的并发交迭运行使得安全协议运行时往往难以实现它的设计目标。形式化方法已被证明是分析和验证安全协议的有效手段,安全协议的形式化分析与验证已经成为当前形式化方法领域的一个研究热点。 本文以安全协议作为研究对象,以有效的形式化验证方法作为主要研究内容。本文的主要贡献包括: (1) 安全协议形式化建模、安全协议形式化验证方法和安全协议反例的自动构造算法。 Bruno Blanchet提出了基于Horn逻辑的安全协议模型,它是由基于线性逻辑的安全模型经过抽象解释和程序变换、并对带存在量词的公式进行Skolem化而得到的一个安全协议模型。基于进程代数的安全协议模型使用一组变换规则也可以转换为基于Horn逻辑的安全协议模型。在基于Horn逻辑的安全协议模型,没有描述消息的发送者和接受者,无法区分安全协议诚实角色与安全协议攻击者的形式化刻画。 在对基于Horn逻辑的安全协议模型进行深入分析的基础上,本文提出了基于Horn逻辑的安全协议扩展模型和基于进程代数的安全协议扩展模型。基于Bruno Blanchet的验证方法,本文提出了基于Horn逻辑的安全协议扩展模型的安全协议验证方法,从该方法的验证过程中能自动构造不满足安全性质的安全协议反例。 基于Horn逻辑的安全协议模型是对基于线性逻辑的安全模型进行抽象解释得到的模型。如果安全协议的验证过程表明基于Horn逻辑的安全协议模型满足安全性质,抽象解释保证安全协议满足安全性质;如果安全协议的验证过程表明基于Horn逻辑的安全协议模型不满足安全性质,由于抽象解释可能引入了虚假攻击,抽象解释并不保证安全协议一定不满足安全性质。自动构造不满足安全性质的安全协议反例有助于辨识虚假攻击,有助于分析安全协议出现漏洞的原因,以便对安全协议进行校正。基于Horn逻辑的安全协议扩展模型的安全协议验证过程,本文提出了不满足安全性质的安全协议反例的自动构造算法。
武涛[2]2009年在《基于增量式可满足性求解的安全协议形式化验证方法》文中提出随着现代计算机技术和网络技术的不断更新,它们的应用领域也在向着更宽更深的方向发展,这也对计算机网络安全提出了更高的要求。被设计用来解决这一问题的安全协议在一定程度上为网络通信的正常运行起到了积极的作用。但是,由于其自身设计中的一些缺陷而最终导致的安全漏洞也成为了现代非常严重的网络安全问题。所以人们就在安全协议设计与分析中投入了大量的工作。安全协议设计规则为安全协议的制定提供了标准,而安全协议分析为安全协议能够成功实现其安全性能提供了保障。并且,随着现代通信技术的不断发展和网络技术的广泛应用,这两个方面越来越受到人们的关注。这其中就包括对安全协议的形式化分析这一重要内容。安全协议的形式化分析大体来说有叁种方法,形式逻辑,模型检验和定理证明。其中,作为形式化分析的重要组成部分和有效分析手段的模型检验技术在分析安全协议这一过程中更是凸显了其重要的作用和地位。其中,有一种基于可满足性问题的模型检验技术已经在安全协议形式化分析中得到了应用。本文的主要工作就是对形式化分析的叁种方法进行了研究,特别是在基于可满足性问题的模型检验技术上更是投入了大量的工作。基于可满足性(SAT)问题的模型检验技术从功能结构上可分为两个部分:SAT编码和SAT求解。通过研究,我们发现了其算法中有一些可以改进的地方,提出了基于增量式可满足性问题的模型检验方法,其主要工作包括两部分:一是关于增量式SAT编码过程的实现,另一个是关于增量式SAT求解过程的实现。
刘锋[3]2002年在《安全协议模型检验技术研究与实现》文中指出随着计算机网络通信的迅猛发展，安全协议的重要性越来越得到重视。安全协议负责密钥分发和身份认证，一旦其自身出现漏洞，那么将会对通信的安全造成威胁。模型检验方法在对安全协议的验证中体现出了巨大的优越性。 本课题的研究目的是采用模型检验工具对安全协议进行验证。本文研究了验证安全协议的各种形式化方法，详细研究了符号化模型检验工具SMV的工作机制；确定了使用SMV作为工具对安全协议进行模型检验，验证了认证版Needham-Schroeder公钥协议和Woo and Lam Π对称钥协议。 通过使用SMV对Needham-Schroeder公钥协议进行建模和验证，理解了符号化模型检验和小系统模型的原理，并发现了一个协议漏洞，该漏洞与Gavin Lowe用FDR所发现的相一致。 为了突破小系统模型的局限性，我们使用SMV验证Woo and Lam Ⅱ对称钥协议时，建立了允许诚实的通信实体运行两次协议的模型，在这个模型上发现了一个已知的协议漏洞，攻击者利用诚实通信实体的两次运行，成功地进行了攻击。 在对SMV的大量使用中，我们发现了SMV的一个bug和其产品说明书中所忽略的一些值得注意的问题。 文章主要介绍了安全协议的概念、分类和性质，安全协议的形式化验证方法，以及小系统模型的原理；重点分析和研究了符号化模型检验工具SMV的原理和语法及其对安全协议进行模型检验时的工作机理，而且使用SMV对Needham-Schroeder公钥协议和Woo and Lam Π对称钥协议进行了形式化建模与模型检验，发现了它们的安全漏洞。
周倜[4]2008年在《复杂安全协议的建模与验证》文中研究指明随着网络的发展,互联网络的安全问题变得越来越棘手,越来越重要,安全协议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问题最有效的手段之一,使用安全协议在开放的互联网络上可以实现身份认证等多项安全功能。由于在计算机网络中,相互通信的双方不能通过生物特征识别对方,因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码体制基础上的一种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。然而,设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明的安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。设计和开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领域的一个研究热点,也是验证复杂安全协议的关键环节。本文以Bruno Blanchet提出的Horn逻辑模型为基础,对反例构造算法和复杂协议验证方法进行了系统、深入的研究,主要工作包括以下几个方面:1.基于Horn逻辑的安全协议反例的自动构造算法。Bruno Blanchet提出了基于Horn逻辑的安全协议模型,该模型可高效地验证安全协议。为了将消息的角色信息保留在模型中,本文设计了相关的数据结构,给出了反例自动构造的算法实现,使验证工具能从不满足安全性质的消解序列中自动地构造出标准形式的反例,从而方便人们使用基于Horn逻辑的验证工具验证协议。2.不动点计算的不停机性预测。安全协议验证的不停机性源于不动点计算的不停机性。通过研究安全协议逻辑程序解形式不动点计算不终止的特征,本文给出了不动点计算不终止的预测方法。基于此方法,可以在协议验证时自适应地选择(精确或抽象)验证方法验证(停机或不停机的)安全协议。3.抽象与精化迭代验证框架。安全协议的正确性验证问题是不可判定的,使用抽象解释理论能够有效地验证安全协议。通过研究Horn逻辑模型中协议验证的特点,给出了安全协议基于抽象-精化的迭代验证理论框架。抽象验证保证停机,而精化过程可有效地去除虚假反例。因此,抽象-精化迭代框架可对Horn逻辑模型中验证过程不停机的安全协议进行有效验证。为了提高抽象模型的精度,本文进一步提出了局部抽象-精化迭代验证的理论框架。局部抽象可以提高整个验证过程的验证效率,为复杂协议的验证提供了有效的途径。4.时间敏感安全协议的建模与验证。通过将描述时间的事件加入到进程代数模型中,使得时间戳能方便有效地在协议模型中描述出来。将时间元素的线性约束加入到基于Horn逻辑的安全协议模型中,使得Horn逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解的关系,找到了确定时间相关元素的时间先后关系的办法,提出了两阶段验证方法。一条规则是否可用,此时还需考察其所对应的约束系统是否可满足。因此,本文对该模型下的约束系统进行了研究,提出了一个高效判断其可满足性的判定算法,并证明了该算法是多项式时间算法。由于约束系统中存在大量冗余的不等式,本文还深入研究了该系统,针对其本身的特性,提出了约束的抽象理论简化约束系统,该方法能有效地降低时空开销。5.设计并实现了一个高效的安全协议验证工具SPVT-II。本文提出了不停机性预测和抽象-精化迭代验证框架的实现算法,在安全协议自动分析工具SPVT的基础上,结合抽象-精化迭代验证框架,设计并实现了一个自适应选择验证方法的高效的协议验证工具SPVT-II。该工具既能发现协议中可能的反例,也能尽可能地减少虚假反例的产生。6. Kerberos协议协议的分析与验证。本文通过对Kerberos协议进行分析,将公钥Kerberos协议的认证服务交换阶段进行了建模,并用SPVT-II对协议模型进行了自动化的验证。实验结果表明SPVT-II能自动发现PKINIT-26中认证服务阶段的攻击。
李文全[5]2004年在《基于符号模型检验的电子商务协议原子性的研究与实现》文中研究指明随着电子商务在全球范围的广泛应用,电子商务的纠纷也越来越多。在众多的电子商务纠纷中,相当一部分是由于电子支付协议本身的缺陷引起的。因而电子支付协议成了电子商务发展的瓶颈。而电子支付协议的原子性是用来规范电子交易活动中的资金流、信息流、和物流,因而是导致支付过程中产生纠纷的重要原因之一。因而,近年来,电子商务协议的原子性成了研究的热点。人们针对电子支付协议的原子性提出了诸多的协议,企图解决这个问题。电子商务协议的设计是一个十分庞大和复杂的工作,而且极易出现意想不到的错误,一个看是完美无缺的协议可能存在各种漏洞。这样电子商务协议的原子性的分析验证就成了一个现实的课题。 目前对电子商务协议的检验手段主要有:直观的分析,实际攻击测试和形式化的检验分析技术。由于形式化分析借助于形式化分析方法和工具完成,具有逻辑严密和断言普遍的优点,但是形式化分析中的逻辑验证需要初始假设的非形式化过程,以及对协议进行理想化等缺陷。Gavin Lowe首先使用CSP和模型检验技术对密码协议进行分析,它克服了逻辑验证的上述缺陷。模型检验在电子商务协议安全性分析验证方面得到了广泛的应用。 本文应用符号模型检验器(SMV)对电子商务协议的原子性进行分析,在对SET协议进行形式化描述的基础上,对SET协议进行分析和检验,指出了协议的缺陷。同时对该协议进行改进,又对改进后的协议的进行分析和检验,表明应用符号模型检验器对电子商务协议分析检验的可行性。
吴振强[6]2007年在《无线局域网安全体系结构及关键技术》文中进行了进一步梳理无线局域网(WLAN)与蜂窝网相比具有更高的传输速率和更好的灵活性,目前,WLAN已经在大学校园、咖啡厅、机场和一些企业等得到了初步的应用,未来这种具有移动Ad Hoc和无线Mesh网络功能的WLAN将会在一些特定的应用领域变得越来越普及。下一代的移动互联网将是基于Internet的核心网络和无线接入网络,它们需要高效地融合有线和无线网络基础设施,以支持新的网络体系结构、协议和控制机制,提供新的无线多媒体服务与应用。然而,无线传输介质具有在一定范围内提供开放接入特性,WLAN的安全性已经成为一个非常严重的问题。论文对无线局域网安全体系结构的方法与技术进行了比较全面的研究,研究内容包括:WLAN安全体系结构框架、安全接入协议、快速切换安全协议、Mesh安全协议、WLAN的匿名协议与匿名度量模型、自适应安全策略、安全性能评估及可信的WLAN体系结构等。论文从设计、实现与评价一个WLAN安全系统的体系结构入手,重点对WLAN安全体系结构的“点、线、面、空间”等多个视角进行技术研究,主要成果有:(1)在“点”上对WLAN安全体系结构的横向技术进行研究,提出了自验证公钥的认证和密钥协商协议、基于位置的快速切换安全方案、基于身份的Mesh认证协议、无线局域网动态混淆匿名算法与匿名连接协议、基于联合熵的多属性匿名度量模型等,并对Mesh网络的接入认证技术进行了原型实现;(2)在“线”上对WLAN安全体系结构的设计与实现技术进行研究,该研究从两个方面进行:一方面从无线局域网安全管理角度,提出了基于管理的无线局域网安全体系结构;另一方面从移动终端角度,提出了自适应终端集成安全认证体系结构方案,给出了方案的技术原理与原型实现,通过软件系统的原型实现,验证了方案的可行性;(3)在“面”上对WLAN安全体系结构的系统角度进行研究,重点对无线局域网安全体系结构的自适应安全策略和安全体系结构的安全性能评估两个方面进行了初步探索,提出了基于策略的WLAN安全管理框架,并给出了基于熵权系数的WLAN安全威胁量化方案;(4)在“空间”上对WLAN安全的发展趋势和可信性体系结构进行了探索研究,结合安全体系结构的可生存性和TPM技术的发展,对服务可信的WLAN体系结构进行了初步的研究,提出了基于TPM的移动互联网可信体系框架。
王强[7]2012年在《安全协议形式化验证方法研究》文中认为随着计算机网络技术的不断发展，网络信息安全已经成为信息时代的一个至关重要的问题。安全协议作为网络安全通信的基础技术，是确保网络信息安全的有效手段之一。然而实践表明，设计正确可靠的安全协议是一项十分困难的工作，许多广泛使用的安全协议被指出存在各种安全漏洞。因而，分析和验证协议的安全性具有重要的应用价值。目前，研究人员主要采用形式化方法来分析和验证协议的安全性。本文以符号模型下安全协议的形式化验证方法为研究内容，主要分析和拓展了基于应用Pi演算的安全协议建模和关键安全属性的自动化验证技术，取得了一系列有价值的研究成果。主要研究内容和成果体现在：（1）基于应用Pi演算的安全协议建模和验证方法研究。首先分析了应用Pi演算框架下安全协议及其安全属性的建模方法，其次分析了两类不同的安全属性形式化验证技术：基于协议迹的可达性分析技术和基于协议进程观测等价的互模拟验证技术，指出了上述两种技术方法的优缺点和存在的挑战，给出了进一步改进的思路。（2）基于约束系统的保密性验证方法和约束求解算法研究。针对可达性分析技术存在的不可判定的缺点，首先提出了基于约束系统的安全协议建模与验证方法。约束系统是对协议执行迹的符号化表示，将无穷的协议迹抽象为有限的约束系统，并将安全性验证问题转换为带安全属性公式的约束系统的可满足性判定问题；其次深入研究了HubertComon-Lundh的约束求解算法，分析了该算法的正确性、完备性和停机性。该算法可以实现安全协议的自动化验证，但存在时间复杂度较高的不足。（3）改进的协议进程迹等价判定算法研究与实现。针对应用Pi演算中观测等价性不可判定的不足，研究了应用Pi演算的可判定子集—简单进程的迹等价判定算法。首先深入分析了Vincent Cheval的不含异或算子的迹等价判定算法，对原算法进行了适当改进，降低了复杂度，给出了该算法Ocaml语言实现；其次，首次提出了含异或算子的迹等价判定算法，该算法可以用于简单进程的自动化迹等价判定，也可用于安全协议的复杂安全属性的形式化验证。由于简单进程的迹等价和观测等价是一致的，该算法也可用于观测等价性的判定。
莫燕[8]2005年在《网络安全协议模型检测技术研究与应用》文中研究说明安全协议的安全性是网络安全的重要基础，运用形式化方法分析安全协议的安全性已成为目前研究的主要热点。本文主要研究运用形式化技术分析安全协议的理论与技术，对基于模型检测技术的运行模式分析法进行深入的研究，并把其应用到实用安全协议的分析与设计中去。主要的研究成果如下： (1) 对安全协议的背景及基本概念、安全协议的形式化分析方法的叁种思路进行了系统的介绍； (2) 介绍两方安全协议的运行模式分析法，对只包括一个可信第叁方服务器的协议的运行模式分析法进行归纳，提出多于一个可信第叁方服务器协议的运行模式分析法； (3) 计算运行模式的数量上界，并给出有效的约束条件，构造与具体模型检测工具相独立的运行模式组合集，进一步提出了多方安全协议的运行模式分析法； (4) 使用运行模式分析法成功分析了实用的安全协议，如SSL3.0、TMN、Kerberos等协议，得到了较好的结论； (5) 根据协议的安全缺陷提出了安全协议的设计原则，并设计了一个安全的密钥建立协议； (6) 总结模型检测法，并与其他经典形式化分析方法进行了详细的比较。
李梦君, 潘国腾, 欧国东[9]2018年在《基于Event-B方法的安全协议设计、建模与验证》文中进行了进一步梳理随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展,研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上,综述了基于Event-B方法的安全协议形式化设计、建模与源程序验证的典型研究工作,主要包括从需求规范到消息传递形式协议的安全协议精化设计、基于TPM(trusted platform module)的安全协议应用的精化建模以及从消息传递形式协议到代码的源程序精化验证.
刘锋, 李舟军, 李梦君, 宋震, 张艳[10]2004年在《基于SMV的安全协议模型检验》文中认为SMV是一个基于线性时态逻辑的符号化模型检验工具。本文利用SMV对Needham-Schmeder公钥协议的简化版本进行了验证,发现了利用消息重放进行的攻击。
参考文献：
[1]. 安全协议形式化验证技术的研究与实现[D]. 李梦君. 国防科学技术大学. 2005
[2]. 基于增量式可满足性求解的安全协议形式化验证方法[D]. 武涛. 北京交通大学. 2009
[3]. 安全协议模型检验技术研究与实现[D]. 刘锋. 中国人民解放军国防科学技术大学. 2002
[4]. 复杂安全协议的建模与验证[D]. 周倜. 国防科学技术大学. 2008
[5]. 基于符号模型检验的电子商务协议原子性的研究与实现[D]. 李文全. 东北大学. 2004
[6]. 无线局域网安全体系结构及关键技术[D]. 吴振强. 西安电子科技大学. 2007
[7]. 安全协议形式化验证方法研究[D]. 王强. 国防科学技术大学. 2012
[8]. 网络安全协议模型检测技术研究与应用[D]. 莫燕. 西安电子科技大学. 2005
[9]. 基于Event-B方法的安全协议设计、建模与验证[J]. 李梦君, 潘国腾, 欧国东. 软件学报. 2018
[10]. 基于SMV的安全协议模型检验[J]. 刘锋, 李舟军, 李梦君, 宋震, 张艳. 计算机工程与科学. 2004
标签：互联网技术论文; 安全协议论文; 计算机网络论文; 逻辑模型论文; 形式化方法论文; 逻辑符号论文; 信息安全论文; 逻辑框架论文; 电子商务分析论文; 关系逻辑论文; 建模软件论文; 网络安全论文; 算法论文; 科技新闻论文;