一、Needham Schroeder协议的安全缺陷与改进（论文文献综述）
王建华,张岚[1]（2021）在《检测类型缺陷的形式化构造攻击方法》文中进行了进一步梳理针对密码认证协议的类型缺陷问题,细粒度地刻画了该类协议的消息类型结构特征,提出并证明了类型缺陷攻击存在性定理,基于原子消息加密数据结构及串空间模型提出了检测类型缺陷的形式化构造攻击方法,应用于密码认证协议的形式化分析,找到了一系列关于该类协议的类型缺陷攻击,指出了产生类型缺陷的根本原因以及修正措施,为了使密码协议设计渐趋精细化、标准化、科学化,给出了无消息-类型同态性、相似性、等价性等密码协议设计准则,突破了消息类型复杂多样、类型缺陷难以检测的密码协议设计关键技术.以Yahalom-Paulson协议为例,分析说明该方法的具体应用,检测出了该协议存在的两类类型缺陷攻击.理论推导和实例分析表明,经过该方法分析修正过的密码认证协议在Dolev-Yao模型规范的攻击者能力下能达到可证明安全,与其它的密码协议形式化工具方法相比较,该方法有明显的代数结构特征,而且形式化格式特征突出,极易判别,在全面检测密码协议的类型缺陷方面有优势,发现了一个在公开文献中未曾出现的Wide-Mouth Frog协议的新攻击.
冯皓楠[2]（2021）在《安全协议形式化分析技术的应用与研究》文中认为安全协议运用密码算法,实现认证和密钥分配等目标。但是安全协议本身仍然存在安全隐患,对安全协议的各类攻击,导致个人、企业或国家机密信息泄露,造成财产损失。借助计算机和数学手段,形式化分析技术可以自动、快速和全面地对安全协议进行分析,不但能寻找安全协议的漏洞,还可以证明协议的安全性。该技术自提出以来,已经被应用到大量协议的分析中,促进了安全协议的研究与发展。但是,形式化分析技术目前仍旧不够成熟。本文对安全协议的形式化分析技术进行应用与研究,深入探讨了ProVerif形式化分析工具的原理,提出了利用ProVerif工具对安全协议进行形式化分析的方法,并以FIDO UAF为例进行了验证分析,最后对ProVerif和形式化分析方法进行了评估,找到了 ProVerif工具以及形式化分析方法的相关缺陷,并提出了改进方案。本文的主要工作和创新点包括:（1）提出了一种基于ProVerif的安全协议形式化分析方法,该方法提出了进程通信模型下恶意实体的建模方法、不可链接性的验证方法以及最小化假设的验证方法。（2）使用本文提出的方法对UAF协议进行形式化分析。首先对UAF协议的文档进行梳理,并对协议流程、安全假设、安全目标进行形式化翻译。其次提出UAF协议的ProVerif模型,开发UAFVerif工具,对UAF协议的所有可能场景进行分析,并自动寻找协议的最小化安全假设。在此基础上,论文提出针对UAF协议的攻击方式,成功将认证器重绑定攻击实施在两类应用中,获得CNNVD漏洞。最后提出了对UAF协议的改进建议。（3）总结ProVerif工具以及形式化分析过程的缺陷并提出了改进方案,其中包括ProVerif难以支持非Dolev-Yao模型下的协议分析、难以支持复杂的数学操作和计数器模型、不支持实体操作可变下认证性的分析以及难以支持实体遭到破坏的场景下不可链接性的分析等。
杨锦翔[3]（2021）在《网络安全协议的形式化自动验证优化研究》文中进行了进一步梳理为了保障网络通信安全的协议是网络安全协议。网络安全协议能否在运行过程中,保证设计之初所预计的安全性不会发生变化,可以使用形式化验证的方式进行证明。形式化验证的含义是根据某些抽象表达的形式属性,使用数学方法对其证明。与非形式化验证的方式相比,使用形式化验证的方式能够全面地检测网络安全协议中存在的未知漏洞,发现新型攻击手段。现有的形式化验证可分为手工验证、半自动验证、全自动验证三种方式。由于网络安全协议的状态空间难以穷尽,因此全自动验证的方式与手工以及半自动验证方式相比,需要更加复杂的算法设计,来尽可能地缩小状态空间搜索范围。但全自动验证有无需形式化领域先验知识进行验证的优点,有助于网络安全协议的迅速发展与广泛运用。现存的针对网络安全协议进行全自动形式化验证的工具中,SmartVerif能够验证最多种类的网络安全协议。但SmartVerif存在对网络安全协议验证时间长,框架所使用的神经网络不具有通用性的缺陷。因此本文针对SmartVerif验证工具的缺陷进行相应的优化设计。实验结果表明,经过本文工作的改进,该全自动形式化验证框架与原方案相比,对网络安全协议验证时间更短。同时使得网络具有通用性,能够验证更多种类的网络安全协议。本文的具体工作如下:1.本文提出了约束求解规则的树形式结构转换技术。由于在形式化验证过程中会产生许多高度抽象的数据,因此为了能够更加清晰地表达数据的形式化语义,需要一种更合适的数据结构。在树形式数据中,每个结点包含两个属性,一是原形式化数据中的部分字符串,二是该部分字符串所对应的形式化语义。通过树形式数据转换的方式,能够更加清晰地表达数据的形式化语义信息。并且将形式化数据转换为神经网络输入向量时,能够保留更多的数据形式化特征。同时有助于对数据的形式化语义一致性进行判定。2.本文优化了证明定理树中的循环路径判定算法。在自动形式化验证中普遍存在着循环证明的问题,在本文使用的形式化验证工具中体现为,在定理树中产生了循环路径。为了保证对网络安全协议验证的高效性与准确性,需要尽可能早且准确地探测循环路径。优化算法能够提高对无循环路径判定的准确率,从而使得目前实验所使用的网络安全协议没有发生错误验证。3.本文优化了形式化自动验证中的深度强化学习算法。优化算法利用约束求解规则的树形式转换工作,能够在嵌入向量空间时保留更多约束中的不变形式化特征,使得网络能够学习到数据的形式化特征。优化算法还使用了基于蒙特卡洛树搜索的强化学习框架,使得神经网络具有通用性,因此可以使用多个网络安全协议训练一个神经网络,并且该神经网络能够用来验证新的网络安全协议。优化算法使用了对神经网络训练更有效的反馈设置,能够加速神经网络收敛过程。
苏诚[4]（2020）在《基于强化学习的安全协议形式化自动验证技术研究》文中研究说明近年来,网络安全问题日趋严重,针对计算机网络的安全和隐私研究已刻不容缓。为了解决网络协议安全性不足的问题,研究人员设计了各种网络安全协议（以下简称安全协议）,以增强网络的安全。但是,很多投入实际应用的安全协议在运行时并不能提供其声明的安全服务。因此,针对安全协议的安全性检测成为安全测试中的重要环节。研究人员在设计或优化安全协议后,需要进一步证明该协议的安全。与非形式化的安全协议验证技术相比,形式化方法能够更全面、深入的检测安全协议和软件中未知的漏洞,它不仅能够证明安全协议的安全性,而且有助于发现针对安全协议的新型攻击手段。但是由于安全协议的复杂性,现有的形式化验证技术并不能自动化证明所有的安全协议,在证明过程中需要专业验证人员辅助计算机完成证明。过高的人力成本和学习成本阻碍了形式化验证技术的进一步发展和运用。本文围绕安全协议的形式化自动验证相关问题,开展了深入的研究。主要研究成果总结如下:1.提出了一种基于强化学习的安全协议形式化自动验证技术,设计并实现了原型系统。本方法突破并解决了传统形式化自动验证中的状态空间爆炸问题。相比于传统的形式化验证工具,该系统可以全自动地搜索正确证明路径,无需任何手工辅助。研究成果可以挖掘给定目标的安全协议的所有安全漏洞,确保网络安全协议不会被攻击者攻破。据笔者所知,该系统是首个使用动态策略全自动形式化验证安全协议的工作。实验结果表明,该系统实现了安全协议的通用和全自动形式化验证,远优于现有的形式化验证工具。2.提出了一种面向可追责协议的形式化研究方法,设计并实现了原型系统。针对可追责协议的安全属性本文提出了形式化定义。基于该定义,提出并实现了针对可追责协议的形式化建模与验证方法。该方法扩展了应用pi演算语言,通过使用新定义的语法,用户只需要对正常参与方的操作流程进行手动建模,工具可根据用户建立的模型将相应的异常参与方操作自动转换为协议验证工具ProVerif可验证的模型语言。另外,本文提出了一套自动转换协议模型并生成安全目标的方法。该方法极大降低了形式化建模和验证协议的复杂性。实验结果表明,该方法可适用于两个典型的可追责协议的形式化研究,通过本方法,成功发现了不可否认协议的设计缺陷。3.提出了一种面向5G-AKA协议的形式化研究方法。该方法采用多重集合复写规则对5G-AKA协议进行建模。协议模型基于协议规范中的四方消息交互模型。攻击者能力比现有工作定义的攻击者能力要更全面。安全属性包含私密性、认证的相关属性以及隐私性。然后,使用通用全自动形式化验证系统验证形式化模型。实验结果表明,5G-AKA协议模型中的所有安全属性都成立。另外,使用前文定义的可追责属性针对5G-AKA协议进行了形式化分析,发现协议并未设计追责的流程,存在设计缺陷。针对此缺陷,对5G-AKA协议提出了改进措施,并使用通用全自动形式化验证系统对改进后的协议进行了验证,验证结果表明,修改后的协议保证了追责的公平性和完整性。
朱俊翔,张翔[5]（2020）在《基于Event-B对存在网络攻击的安全协议的改进研究》文中研究说明设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务。即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易。本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证改进后的协议可以防御已知的网络攻击。首先用初始模型对攻击场景高度抽象,通过对抽象模型的精化,得到反映真实攻击过程的具体模型。然后将描述协议行为的事件从模型中分离出来,单独对其进行精化改进,如果改进后的协议事件重组的模型与具体模型不存在精化关系,则改进的合理性可以得到验证。最后通过NSPK协议被攻击的案例展示了本研究所提出方法的可用性。该框架可用于开发协议,以避免由逻辑漏洞引起的攻击,并验证协议补丁的正确性。
赵怡静[6]（2020）在《基于单光子的双向量子身份认证协议及其安全性形式化分析》文中认为随着近年来量子通信领域快速的发展,量子安全通信是着重研究的方向之一,通信前的身份认证承担着保障通信合法的重要责任;量子身份认证（Quantum Identity Authentication,QIA）是密钥分发和量子通信前对通信用户合法性进行确认的重要步骤,因此完整的量子身份认证协议和流程显得尤为重要;同时随着量子基站的落成,用户的身份认证在验证合法性之前还需要考虑用户具备的不同量子能力,即考虑用户具备何种程度的量子能力;在完整的QIA协议中,协议的安全性概率分析也是重要的组成部分,从总体上来看量子密码的安全性分析上的现有发展较为缓慢,但近年来量子通信协议的形式化分析逐渐成为了量子领域热点,研究方向上也出现包括Petri技术、模型检测等新的尝试,这些方法如何应用在量子身份认证协议中的安全性分析中是值得研究的;针对现有的QIA协议的不足,我们提出了一种基于单光子可实现双向同步的量子身份认证协议,具体内容如下:（1）提出了一种有可信第三方参与的具体协议策略,协议准备阶段结合了Kerberos经典密码协议思想提出根据量子票据发起建立的认证流程。在认证阶段,采用了一种高效的新型编码方式,通过一次制备反复抛回的策略实现了同步认证,仅通过一次共享编码实现完整的双向认证流程。（2）考虑到用户可能具备的不同量子能力和通信环境,补充了基于相同策略但流程上有所改进的半量子通信环境下的完整QIA协议,在半量子环境下同样实现双向同步的、高效地认证。（3）就身份认证协议中面临的不同攻击方式进行了传统的数学概率计算和基于概率模型检测的形式化分析,并将二者进行比较和总结;在概率模型检测中使用了Prism工具对不同模块分别建模,得到了协议的可证明安全性。（4）补充了协议扩展到多用户的原则,通过“临时基站”的想法拟提高量子网络多用户认证中的独立性和私密性。
欧阳恒一[7]（2020）在《基于强化学习的网络安全协议形式化验证与应用技术研究》文中研究指明形式化验证是用数学的方法去证明系统的完备性。当前的形式化验证已经成功用于网络安全协议的证明,并发现了许多漏洞。但是现有的形式化验证方法主要是手工的验证和半自动化的验证。因为协议状态空间的过大会导致内存爆炸的情况发生,因此,对网络安全协议的自动化验证仍是一个挑战。智能合约是一种能根据接收到的信息自动履行合同条款的协议,随着以智能合约为代表的区块链应用的增长,其频发的安全事件也严重威胁着大众的经济财产安全。本文中,为了能对网络安全协议进行自动化验证,作者提出了一款能自动化验证协议的通用框架,我们采用了动态策略的方法,辅助形式化验证工具智能的在定理树上进行路径搜索。与现有的静态策略相比,该方法具有更灵活且不需要人工学习成本的特点。动态策略在经过训练后,能够根据协议自动的对神经网络进行优化,且不需要人工辅助,提高了验证成功的概率。为了解决智能合约中待验证合约数量多且需要较高安全等级的验证的问题,本文提出了一种代币智能合约的形式化建模方法,对5个存在整数溢出漏洞的智能合约进行建模,并使用了本文提出的自动验证框架形式化验证,成功且高效的找出了其存在的整数溢出漏洞。本文所提出的形式化验证框架的动态策略设计思想是:当在定理树中进行随机的路径搜索时,如果定理树中某个节点代表的引理不在正确的路径上时,我们应该给它赋予一个较低的权值。因此我们引入了一种强化学习算法DQN（Deep Q Network）来实现该策略。本文所提出的智能合约形式化建模方法需先对程序的一系列逻辑代码进行建模,再通过演算的方法,证明其安全属性是否得到满足或者是破坏。本文开展的主要工作有:1.为了能让强化学习中的神经网络能对形式化验证逻辑进行学习,本文设计了一种形式化数据提取技术。该技术对验证工具自动生成的中间定理进行了剪枝,提取了相应的逻辑语句来简化描述验证过程,解决了现有的形式化验证数据难以与神经网络直接进行交互的问题。并构建了定理树的存储结构,通过对冗余数据的剪枝以及使用神经网络来辅助定理树进行递归的构建,解决了定理树存储时容易造成状态空间爆炸的问题。2.为了解决监督学习及无监督学习算法因缺少数据集难以进行网络训练的问题,本文引入强化学习中的DQN神经网络到形式化验证中,并提出了一种特征向量的提取方法和判断循环检测的算法。提高了神经网络的通用性以及路径选择的成功率。与监督学习方法相比,该方法不需要提供数据集进行神经网络的训练。3.为了展示本文提出的自动形式化验证框架的应用场景,同时解决智能合约中存在的安全性问题,本文提出了一种代币智能合约的形式化建模方法。通过对智能合约的逻辑代码进行建模,来分析其安全属性是否得到满足或者是破坏。并通过本文的自动化验证框架进行验证后,成功且高效地发现了其存在的漏洞。
王晓晗[8]（2020）在《基于多反例的安全协议分析研究与实现》文中提出随着互联网在人们的生活中应用的越来越广泛,网络安全也变得愈加重要。安全协议作为信息安全的重要组成部分,对其进行分析具有重要的研究价值。目前分析安全协议的方法多种多样,模型检测作为一种形式化分析方法被广泛的应用于安全协议的分析。本文以模型检测器生成的反例为基础,对安全协议进行分析得到协议的攻击路径。模型检测相比于其他形式化方法具有很多优势。模型检测是一个高度自动化的技术,将使用者从繁杂的公式推理中解放出来。当输入模型违反系统规约时,模型检测器会产生一个从系统的初始状态到违反规约状态的路径,即反例。现有的模型检测器会产生多个违反系统规约的反例,然而其中很多反例都对应同一条错误路径,仅仅是在实例数据取值上存在不同。模型检测器产生的冗杂的反例集合给反例的分析带来了困难。在模型检测器检测协议模型的过程中,协议的建模显得尤为重要。本文以NSPK协议为例,使用模型检测器SPIN的建模语言promela对其进行建模,同时分析出该协议模型需要满足的安全性质,使用SPIN对协议模型进行检测后得到多个反例。为了解决模型检测器生成的众多反例间的数据相似性问题,本文提出使用反例的等价类对多反例进行精简的方法。该方法保证每个反例的等价类都只包含一个反例,使得精简后的反例集合中的每个反例都代表一条不同的反例路径,大大减少了反例的数量,提高了系统的运行效率,为多反例的分析打好了基础。在传统的基于单反例的协议分析的方法中,由于单个反例含有的信息有限,研究人员往往不能准确地找到系统错误。为了解决这个弊端,本文使用精简后的多反例集合对安全协议进行分析,充分利用了多反例包含的信息。我们使用Tarantula方法统计反例中语句出现的频率,计算各个语句的可疑度,并找到最有可能包含协议模型错误的反例,最终根据该反例得出安全协议的攻击路径。与原本的模型检测器SPIN相比,本文的方法在SPIN的基础上增加了多反例精简和多反例分析安全协议的功能。以NSPK协议为例,本文的方法将SPIN产生的1809个反例精简到13个,并且将系统的运行时间由0.67秒提高到0.31秒。最终,根据反例的分析结果发现协议中存在未添加协议通信双方标识符的漏洞并给出了改进意见。
杨科[9]（2019）在《基于事件逻辑的移动支付协议形式化分析》文中提出随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网络环境中,产生的错误很难发现,难以保证协议安全性分析的准确性,必须采用形式化方法和工具来分析。针对移动支付中存在的安全问题,对移动支付协议进行形式化分析,旨在发现移动支付协议中潜在的安全漏洞具有重要意义。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,可用于证明网络安全协议的安全性。本文基于事件逻辑理论并对其进行扩充,对移动支付协议进行形式化分析。本文主要研究内容如下:1.详细介绍事件逻辑理论的产生背景、发展现状、基本思想;对事件系统中的消息自动机和事件系统结构做了阐述,说明事件逻辑是如何去捕捉并描述一个分布式系统;给出事件逻辑理论中的基本定义,包括Atom原子、事件序、事件类,给出了事件逻辑证明系统中的六条公理以及相关引理及性质,其中着重对协议形式化建模中基于事件逻辑的协议建模逻辑与普通的消息-箭头描述方法进行了对比,突出了事件逻辑在协议建模方面的优势;总结归纳了基于事件逻辑的安全协议形式化证明流程图。2.针对移动支付协议中主体数目、协议交互步骤数目较多的情况下,提出迁移规则和可继承性,协议线程中的动作可以迁移到下一个序列中,对于多个协议主体数目、协议交互步骤数目多的协议,能够简化协议证明流程,有效减少协议证明的复杂性。通过事件逻辑理论分析移动支付协议KerNeeS协议安全性,对POS、NFC Phone和Authentication Server间交互进行分析。形式化描述协议双向认证过程、分析协议交互双方的基本序列,基于事件逻辑证明系统对强认证性质进行证明,得出POS和NFC Phone之间能够实现双向认证。3.针对事件逻辑只能分析安全协议认证性而不能分析不可否认性的缺陷,对事件逻辑理论进行扩展。增添了Has、CanProve、Claims、Controls等谓词,扩展协议证明系统,加入拥有公理、管辖公理、签名公理,让扩展的新方法能够对包含不可否认性的协议进行描述与分析。4.对不可否认性进行了定义与分析,使用事件逻辑对其进行形式化刻画说明,阐述了形式化分析不可否认性的具体步骤。首先列举协议的初始状态,包括协议的初始消息拥有集合和初始信念集合,对协议主体的初始状态集合进行了说明,并给出消息、信念的生成规则;接着列举发送方非否认证据EOO和接收方非否认证据EOR,分析EOO和EOR是否符合不可否认性要求;最后分析协议是否达到不可否认性目标,当协议运行在任何阶段时,是否有EOO∈和EOR∈同时成立,从而来分析协议的不可否认性是否满足。根据上述证明流程,以移动支付协议FMPP协议为例进行了形式化分析,说明了结果扩展的事件逻辑能够分析移动支付协议的不可否认性。
谌佳[10]（2019）在《无线体域网环境下三方认证协议的形式化分析与研究》文中认为无线体域网（Wireless Body Area Network）是一个附着在人体上的微型网络。无线传感器加入无线体域网后,医生与患者可以实时远程监控患者的生理数据。例如心跳、血压、胰岛素水平和呼吸等,为实现医疗服务行业中的智能操作、智能管理、智能监控提供了可能。然而无线传输的开放性导致患者生理数据在传输过程中容易受到非法者未经授权的访问和修改,造成隐私泄露、非法监听、数据篡改等信息安全问题,而这些操作可能会对患者产生不可逆的损害。本文重点关注无线体域网环境下的三方认证协议的认证性以及一致性,分别选取基于NTRU、3PAKE、ECDH三种密码体制的三方认证协议作为研究对象,采用形式化方法分析无线体域网环境下三方认证协议的安全性,研究成果如下:（1）基于Maggi的Promla建模方法,构建攻击者二次重放消息的能力。分别使用模型检测方法分析基于3PAKE、ECDH和NTRU密钥体制的三方认证协议,证明了模型检测方法的通用性,并成功发现基于3PAKE和基于NTRU密钥体制的三方认证协议存在Dos攻击漏洞。（2）分析基于3PAKE和NTRU密钥体制的三方认证协议存在攻击漏洞的原因,提出协议改进方法,并验证改进后协议的安全性。模型检测验证结果表明改进后的三方认证协议安全性更高,能够有效抵御Dos攻击漏洞;总结本文所研究的不同密钥体制下三方认证协议存在的安全隐患。（3）提出一种分类压缩的建模优化策略,对比采用语法重定序、偏序规约、类型检查、分类压缩优化策略后模型的状态迁移量等数据,实验结果表明加入分类压缩优化策略后能够有效缓解状态爆炸问题。
二、Needham Schroeder协议的安全缺陷与改进（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、Needham Schroeder协议的安全缺陷与改进（论文提纲范文）
（2）安全协议形式化分析技术的应用与研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第一章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 安全协议的形式化分析技术 |
| 1.2.2 安全协议形式化分析工具 |
| 1.2.3 协议形式化分析技术的应用 |
| 1.3 论文的主要工作 |
| 1.4 论文组织结构 |
| 第二章 ProVerif形式化分析工具的原理 |
| 2.1 ProVerif工具的基本架构 |
| 2.2 应用π-演算 |
| 2.2.1 发展历程 |
| 2.2.2 语法 |
| 2.3 语法检测与类型检测 |
| 2.4 从应用π-演算到Horn子句 |
| 2.4.1 Horn子句 |
| 2.4.2 攻击者子句翻译规则 |
| 2.4.3 协议子句翻译规则 |
| 2.4.4 安全目标翻译规则 |
| 2.5 子句推理和消解算法 |
| 2.6 攻击重构原理 |
| 2.7 本章小结 |
| 第三章 基于ProVerif的安全协议最小化假设分析方法 |
| 3.1 引言 |
| 3.2 协议的形式化描述方法 |
| 3.2.1 协议流程的形式化描述方法 |
| 3.2.2 安全假设的形式化描述方法 |
| 3.2.3 安全目标的形式化描述方法 |
| 3.3 基于ProVerif的形式化建模方法 |
| 3.3.1 基本建模流程 |
| 3.3.2 进程通信情景下恶意实体的建模方案 |
| 3.3.3 不可链接性的建模方案 |
| 3.4 最小化安全假设的验证方案 |
| 3.4.1 最小化安全假设的定义 |
| 3.4.2 最小化假设算法 |
| 3.5 本章总结 |
| 第四章 FIDO UAF协议的形式化建模 |
| 4.1 FIDO UAF协议概述 |
| 4.1.1 背景 |
| 4.1.2 FIDO UAF协议的基本架构 |
| 4.2 FIDO UAF协议的形式化描述 |
| 4.2.1 协议流程的形式化描述 |
| 4.2.2 安全假设的形式化描述 |
| 4.2.3 安全目标的形式化描述 |
| 4.3 FIDO UAF协议的形式化建模 |
| 4.3.1 协议流程的形式化建模 |
| 4.3.2 安全假设的形式化建模 |
| 4.3.3 安全目标的形式化建模 |
| 4.4 本章总结 |
| 第五章 FIDO UAF协议的形式化分析结论 |
| 5.1 分析结论 |
| 5.1.1 结论综述 |
| 5.1.2 协议设计的缺陷 |
| 5.2 攻击 |
| 5.2.1 认证器重绑定攻击 |
| 5.2.2 平行会话攻击 |
| 5.2.3 用户隐私追踪攻击 |
| 5.2.4 拒绝服务攻击 |
| 5.3 改进意见 |
| 5.3.1 明确并标准化安全目标 |
| 5.3.2 修改KHAccessToken机制 |
| 5.3.3 增加ASM对UC的认证机制 |
| 5.3.4 增加UA对UC的认证机制 |
| 5.4 本章总结 |
| 第六章 形式化分析过程的相关缺陷及改进方案 |
| 6.1 ProVerif工具的缺陷与改进 |
| 6.1.1 ProVerif难以支持非Dolev-Yao模型下的协议分析 |
| 6.1.2 ProVerif难以支持复杂的数学操作和计数器模型 |
| 6.1.3 ProVerif 2.00不支持实体操作可变情况下的认证性分析 |
| 6.1.4 ProVerif难以验证实体被破坏下的不可链接性 |
| 6.2 形式化分析方法的缺陷与改进 |
| 6.2.1 传统方法只能分析特定场景下的协议 |
| 6.2.2 没有规范的形式化建模方式 |
| 6.3 本章小结 |
| 第七章 总结与展望 |
| 7.1 工作总结 |
| 7.2 工作展望 |
| 参考文献 |
| 附录 缩略语表 |
| 致谢 |
| 攻读学位期间发表的学术论文目录 |
（3）网络安全协议的形式化自动验证优化研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第1章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 基于逻辑的方法 |
| 1.2.2 基于模型检测的方法 |
| 1.2.3 基于定理证明的方法 |
| 1.2.4 基于人工智能技术的方法 |
| 1.3 主要研究内容 |
| 1.4 论文组织结构 |
| 第2章 相关技术 |
| 2.1 形式化验证概述 |
| 2.2 形式化验证工具 |
| 2.2.1 GsVerif验证工具 |
| 2.2.2 Tamarin-prover验证工具 |
| 2.2.3 SmartVerif验证工具 |
| 2.3 数据的图形式转换 |
| 2.4 强化学习 |
| 2.4.1 强化学习模型 |
| 2.4.2 强化学习探索 |
| 2.4.3 有模型最佳策略 |
| 2.5 深度强化学习 |
| 2.6 本章小结 |
| 第3章 约束求解规则的树形式结构转换技术 |
| 3.1 引言 |
| 3.2 约束求解规则的树形式转换算法 |
| 3.2.1 约束的树形式转换算法 |
| 3.2.2 树形式约束中结点信息域的完善 |
| 3.3 本章小结 |
| 第4章 证明定理树中的循环路径判定算法 |
| 4.1 引言 |
| 4.2 约束求解规则语义一致性判定算法 |
| 4.2.1 树形式约束中结点的相似性 |
| 4.2.2 树形式约束的相似性判定 |
| 4.3 循环路径判定算法 |
| 4.4 实验评估 |
| 4.4.1 实验配置 |
| 4.4.2 循环路径判定算法有效性评测 |
| 4.4.3 循环路径判定算法判定效率评测 |
| 4.5 本章小结 |
| 第5章 自动形式化验证中的深度强化学习算法 |
| 5.1 引言 |
| 5.2 基于树形式约束的特征向量构建方法 |
| 5.3 深度强化学习算法 |
| 5.4 实验评估 |
| 5.4.1 实验配置 |
| 5.4.2 优化深度强化学习算法评测 |
| 5.4.3 优化深度强化学习算法分部对比评测 |
| 5.4.4 优化算法通用性评测 |
| 5.5 本章小结 |
| 第6章 总结与展望 |
| 6.1 本文工作总结 |
| 6.2 研究展望 |
| 参考文献 |
| 致谢 |
| 在读期间发表的学术论文与取得的研究成果 |
（4）基于强化学习的安全协议形式化自动验证技术研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第1章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 本文主要研究内容 |
| 1.3 本文的结构组织 |
| 第2章 国内外研究现状 |
| 2.1 安全协议自动化验证技术 |
| 2.2 针对可追责协议的形式化验证技术 |
| 2.3 针对5G-AKA协议的形式化验证技术 |
| 第3章 基于强化学习的安全协议形式化自动验证技术 |
| 3.1 引言 |
| 3.1.1 研究背景和研究问题 |
| 3.1.2 研究动机 |
| 3.1.3 研究方案和挑战点 |
| 3.2 预备知识 |
| 3.2.1 Tamarin Prover |
| 3.2.2 协议模型 |
| 3.3 系统设计 |
| 3.3.1 系统架构 |
| 3.3.2 信息收集模块 |
| 3.3.3 验证模块 |
| 3.4 实验评估 |
| 3.4.1 实验配置 |
| 3.4.2 实验结果 |
| 3.4.3 案例分析 |
| 3.5 讨论和未来工作 |
| 3.6 本章小结 |
| 第4章 面向可追责协议的形式化研究方法 |
| 4.1 引言 |
| 4.1.1 研究背景和研究问题 |
| 4.1.2 研究方案和挑战点 |
| 4.2 预备知识 |
| 4.2.1 ProVerif |
| 4.2.2 协议参与方和攻击者模型 |
| 4.2.3 第三方裁判的职责 |
| 4.3 系统设计 |
| 4.3.1 协议参与方行为定义 |
| 4.3.2 公平性定义 |
| 4.3.3 完整性定义 |
| 4.3.4 建模与验证过程 |
| 4.4 实验评估 |
| 4.4.1 不可否认协议 |
| 4.4.2 邮件认证协议 |
| 4.5 本章小结 |
| 第5章 面向5G-AKA协议的形式化研究方法 |
| 5.1 引言 |
| 5.2 协议描述 |
| 5.2.1 协议概述 |
| 5.2.2 协议参与方 |
| 5.2.3 协议流程步骤 |
| 5.2.4 安全属性 |
| 5.3 形式化建模与验证 |
| 5.3.1 通信信道 |
| 5.3.2 消息交互流程 |
| 5.3.3 威胁模型 |
| 5.3.4 安全属性 |
| 5.3.5 验证结果与分析 |
| 5.4 针对可追责属性的形式化研究 |
| 5.4.1 协议设计缺陷 |
| 5.4.2 改进措施 |
| 5.4.3 改进后的5G-AKA协议 |
| 5.4.4 验证公平性和完整性 |
| 5.5 本章小结 |
| 第6章 总结与展望 |
| 6.1 工作总结 |
| 6.2 下一步工作 |
| 参考文献 |
| 致谢 |
| 在读期间发表的学术论文与取得的研究成果 |
（5）基于Event-B对存在网络攻击的安全协议的改进研究（论文提纲范文）
| 0 引言 |
| 1 Event-B方法 |
| 1.1 Event-B模型 |
| 1.2 模型的精化关系 |
| 1.3 Rodin平台 |
| 2 对存在网络攻击的协议建模方法和分离规则 |
| 2.1 基本概念 |
| 2.2 建模过程 |
| 2.3 分离规则 |
| 3 对存在网络攻击的协议进行改进并验证改进的合理性 |
| 3.1 对协议进行改进 |
| 3.1.1 对协议部分进行精化 |
| 3.1.2 改变协议事件 |
| 3.2 对改进的合理性进行验证 |
| 3.2.1 用模型间的精化关系验证改进 |
| 3.2.2 用模型检测方法验证改进 |
| 4 案例分析 |
| 4.1 案例介绍 |
| 4.2 建模过程 |
| 4.2.1 初始模型 |
| 4.2.2 具体模型 |
| 4.2.3 精化改进协议 |
| 4.3 验证改进的合理性 |
| 5 结语 |
（6）基于单光子的双向量子身份认证协议及其安全性形式化分析（论文提纲范文）
| 摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 量子单光子源的制备技术条件和优势 |
| 1.2.2 量子身份认证协议的发展 |
| 1.2.3 量子安全形式化分析 |
| 1.3 本文的主要内容与创新点 |
| 第2章 理论知识 |
| 2.1 量子力学基本定理 |
| 2.1.1 量子比特 |
| 2.1.2 海森堡测不确定性 |
| 2.1.3 不可克隆定理 |
| 2.1.4 量子信息处理 |
| 2.2 量子密钥分发与量子身份认证协议 |
| 2.2.1 量子密钥分发协议 |
| 2.2.2 BB84协议 |
| 2.3 量子一次一密 |
| 2.4 量子通信网络中的不同方式 |
| 2.4.1 半量子通信 |
| 2.5 Kerberos身份认证协议 |
| 2.6 形式化分析方法 |
| 2.6.1 概率模型检测 |
| 2.7 本章小结 |
| 第3章 全量子通信协议 |
| 3.1 前期准备 |
| 3.2 双方通信流程 |
| 3.2.1 共享密码串 |
| 3.2.2 共享字符串 |
| 3.2.3 认证阶段 |
| 3.3 两方通信的安全性计算 |
| 3.4 本章小结 |
| 第4章 半量子通信身份认证 |
| 4.1 前期准备 |
| 4.2 双方通信流程 |
| 4.2.1 共享字符串 |
| 4.2.2 协议认证阶段 |
| 4.3 半量子两方通信的安全性计算 |
| 4.3.1 截获-重发攻击 |
| 4.3.2 替换攻击 |
| 4.4 本章小结 |
| 第5章 基于模型检测的安全性分析 |
| 5.1 量子密码协议常见攻击类型 |
| 5.2 建模 |
| 5.3 全量子协议安全性分析 |
| 5.3.1 Alice模块 |
| 5.3.2 Bob模块 |
| 5.3.3 信道模块 |
| 5.3.4 Eve模块 |
| 5.4 半量子协议建模 |
| 5.4.1 Alice模块 |
| 5.4.2 Bob模块 |
| 5.4.3 信道模块 |
| 5.4.4 Eve模块 |
| 5.5 拟验证结果 |
| 5.5.1 全量子环境 |
| 5.5.2 半量子环境 |
| 5.6 本章小结 |
| 第6章 协议补充扩展方向 |
| 6.1 准备阶段 |
| 6.2 协议原则 |
| 6.3 多方通信 |
| 6.4 本章小结 |
| 结论 |
| 论文的主要工作 |
| 后续工作展望 |
| 参考文献 |
| 攻读硕士学位期间所发表的学术成果 |
| 致谢 |
（7）基于强化学习的网络安全协议形式化验证与应用技术研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第1章 绪论 |
| 1.1研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 基于类BAN逻辑的方法 |
| 1.2.2 基于模型检测的方法 |
| 1.2.3 基于定理证明的方法 |
| 1.2.4 结合密码原语代数属性的形式化方法 |
| 1.2.5 结合机器学习的形式化证明方法 |
| 1.3 主要研究内容 |
| 1.4 论文组织结构 |
| 第2章 相关技术 |
| 2.1 形式化验证技术 |
| 2.2 形式化验证工具 |
| 2.2.1 AVISPA验证工具 |
| 2.2.2 ProVerif验证工具 |
| 2.2.3 StatVerif验证工具 |
| 2.2.4 Tamarin验证工具 |
| 2.3 强化学习 |
| 2.3.1 强化学习决策模型 |
| 2.3.2 强化学习算法 |
| 2.4 智能合约 |
| 2.5 本章小结 |
| 第3章 形式化验证数据的提取技术 |
| 3.1 研究目标 |
| 3.2 形式化中间验证数据提取技术 |
| 3.2.1 Tamarin工具初步研究 |
| 3.2.2 中间验证数据提取技术 |
| 3.3 定理树构建 |
| 3.4 本章小结 |
| 第4章 基于DQN的动态验证技术 |
| 4.1 强化学习及特征提取方法概况 |
| 4.2 基于强化学习的动态策略 |
| 4.3 循环检测算法 |
| 4.4 形式化验证数据的特征提取技术 |
| 4.4.1 轨迹公式减少规则 |
| 4.4.2 图约束求解规则 |
| 4.4.3 消息推理约束求解规则 |
| 4.4.4 特征向量提取方法 |
| 4.5 本章小结 |
| 第5章 代币智能合约的形式化建模方法 |
| 5.1 智能合约概述 |
| 5.2 智能合约的建模及流程 |
| 5.2.1 模型角色 |
| 5.2.2 建模属性 |
| 5.2.3 建模及验证流程 |
| 5.3 实验结果 |
| 5.4 本章总结 |
| 第6章 实验与分析 |
| 6.1 方案概述 |
| 6.1.1 实验环境与参数选择 |
| 6.1.2 框架流程 |
| 6.1.3 验证工具与安全协议选择 |
| 6.2 实验结果 |
| 6.3 本章小结 |
| 第7章 总结与展望 |
| 7.1 本文工作总结 |
| 7.2 研究展望 |
| 参考文献 |
| 致谢 |
| 在读期间发表的学术论文与取得的其他研究成果 |
（8）基于多反例的安全协议分析研究与实现（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 研究工作的背景与意义 |
| 1.2 国内外研究现状 |
| 1.2.1 模态逻辑方法 |
| 1.2.2 定理证明方法 |
| 1.2.3 模型检测方法 |
| 1.3 本文的主要贡献与创新 |
| 1.4 论文的结构安排 |
| 第二章 模型检测与安全协议理论基础 |
| 2.1 模型检测技术 |
| 2.1.1 模型检测技术简介 |
| 2.1.2 Kripke模型结构 |
| 2.2 时序逻辑 |
| 2.2.1 分支时序逻辑 |
| 2.2.2 线性时序逻辑 |
| 2.3 安全协议理论基础 |
| 2.3.1 安全协议概述 |
| 2.3.2 安全协议的分类 |
| 2.3.3 常见的安全协议攻击形式 |
| 2.4 本章小结 |
| 第三章 基于SPIN的安全协议多反例搜索 |
| 3.1 模型检测器SPIN |
| 3.1.1 SPIN的验证过程 |
| 3.1.2 Promela语言 |
| 3.1.3 基本算法 |
| 3.1.4 ispin图形化工具 |
| 3.2 安全协议的建模 |
| 3.2.1 安全协议的符号表示 |
| 3.2.2 通信主体建模 |
| 3.2.3 入侵者建模 |
| 3.2.4 协议满足的安全性质 |
| 3.3 SPIN验证安全协议得到多反例 |
| 3.4 本章小结 |
| 第四章 多反例精简与安全协议分析 |
| 4.1 基于多反例发现系统错误 |
| 4.2 多反例的精简 |
| 4.2.1 AC模型的介绍 |
| 4.2.2 扩展性有限状态机 |
| 4.2.3 反例等价类层级的划分 |
| 4.2.4 基于等价类精简多反例算法框架 |
| 4.2.5 等价类层级的LTL属性 |
| 4.3 多反例分析安全协议 |
| 4.3.1 Tarantula故障定位技术 |
| 4.3.2 Tarantula方法分析安全协议 |
| 4.4 本章小结 |
| 第五章 系统设计与实现 |
| 5.1 需求分析 |
| 5.2 系统的总体设计 |
| 5.3 系统实现 |
| 5.3.1 系统的开发环境 |
| 5.3.2 模型编辑检查模块 |
| 5.3.3 模型检测与多反例精简模块 |
| 5.3.4 多反例分析安全协议模块 |
| 5.4 本章小结 |
| 第六章 系统测试与实验结果 |
| 6.1 系统测试 |
| 6.2 实验结果 |
| 6.2.1 安全协议分析 |
| 6.2.2 与SPIN的对比结果 |
| 6.3 本章小结 |
| 第七章 全文总结与展望 |
| 7.1 本文工作总结 |
| 7.2 后续工作展望 |
| 致谢 |
| 参考文献 |
| 攻读硕士学位期间取得的成果 |
（9）基于事件逻辑的移动支付协议形式化分析（论文提纲范文）
| 摘要 |
| abstract |
| 符号说明 |
| 第一章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 移动支付协议及形式化分析研究现状 |
| 1.2.1 移动支付协议研究现状 |
| 1.2.2 移动支付协议形式化分析研究现状 |
| 1.3 研究内容 |
| 1.4 论文结构 |
| 第二章 移动支付协议及形式化方法概述 |
| 2.1 基于NFC的移动支付方案 |
| 2.1.1 基于安全模块的卡模拟方案 |
| 2.1.2 基于主机的卡模型方案 |
| 2.2 移动支付协议概述 |
| 2.2.1 移动支付 |
| 2.2.2 移动支付协议的安全威胁 |
| 2.2.3 移动支付协议的安全属性 |
| 2.3 形式化方法概述 |
| 2.3.1 模态逻辑 |
| 2.3.2 模型检测 |
| 2.3.3 定理证明 |
| 2.4 本章小结 |
| 第三章 事件逻辑理论 |
| 3.1 事件逻辑概述 |
| 3.2 事件系统 |
| 3.2.1 消息自动机 |
| 3.2.2 事件系统结构 |
| 3.3 事件逻辑 |
| 3.3.1 基本定义 |
| 3.3.2 事件逻辑基本框架 |
| 3.3.3 事件逻辑基公理、推论及性质 |
| 3.4 安全协议证明过程 |
| 3.5 本章小结 |
| 第四章 移动支付协议KerNeeS协议形式化分析 |
| 4.1 KerNeeS协议简介 |
| 4.2 协议形式化描述 |
| 4.3 KerNeeS协议形式化性分析 |
| 4.4 本章小结 |
| 第五章 移动支付协议FMPP协议形式化分析 |
| 5.1 基本假设 |
| 5.2 基本概念 |
| 5.2.1 一般协议主体的消息拥有集合及构成 |
| 5.2.2 一般协议主体的信念拥有集合及构成 |
| 5.3 扩展的事件逻辑的语法 |
| 5.4 事件逻辑公理与推理规则的扩展 |
| 5.5 基于扩展事件逻辑分析协议的步骤 |
| 5.6 FMPP协议形式化分析 |
| 5.6.1 FMPP协议 |
| 5.6.2 FMPP协议不可否认性形式化分析 |
| 5.7 本章小结 |
| 第六章 安全协议的形式化方法对比 |
| 6.1 事件逻辑理论与模态逻辑比较 |
| 6.2 事件逻辑与协议组合逻辑比较 |
| 6.3 事件逻辑与模型检测比较 |
| 6.4 本章小结 |
| 第七章 总结与展望 |
| 7.1 总结 |
| 7.2 展望 |
| 参考文献 |
| 个人简历在读期间发表的学术论文 |
| 致谢 |
（10）无线体域网环境下三方认证协议的形式化分析与研究（论文提纲范文）
| 摘要 |
| abstract |
| 主要符号说明 |
| 第一章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 研究现状 |
| 1.3 研究内容 |
| 1.4 论文结构 |
| 第二章 形式化分析方法理论基础 |
| 2.1 形式化方法概述 |
| 2.2 形式化方法研究现状 |
| 2.3 模型检测工具SPIN |
| 2.3.1 SPIN工作机理 |
| 2.3.2 建模语言Promela |
| 第三章 无线体域网环境下的三方认证协议 |
| 3.1 无线体域网环境下三方认证协议的网络模型 |
| 3.2 三方认证协议 |
| 3.2.1 LLYS协议 |
| 3.2.2 RVRKM协议 |
| 3.2.3 DQYSP协议 |
| 3.3 三方认证协议安全问题 |
| 第四章 基于SPIN的三方认证协议模型检测 |
| 4.1 协议建模假设 |
| 4.2 基于SPIN的 LLYS协议模型检测 |
| 4.2.1 LLYS协议诚实主体建模 |
| 4.2.2 LLYS协议攻击者建模 |
| 4.2.3 验证结果与分析 |
| 4.3 基于SPIN的 RVRKM协议模型检测 |
| 4.3.1 RVRKM三方认证诚实主体建模 |
| 4.3.2 RVRKM协议攻击者建模 |
| 4.3.3 验证结果与分析 |
| 4.4 基于SPIN的 DQYSP协议模型检测 |
| 4.4.1 DQYSP协议的形式化表示 |
| 4.4.2 DQYSP协议诚实主体建模 |
| 4.4.3 DQYSP协议攻击者建模 |
| 4.4.4 验证结果与分析 |
| 第五章 基于SPIN的改进协议模型检测 |
| 5.1 协议漏洞分析 |
| 5.2 协议漏洞改进 |
| 5.2.1 LLYS协议漏洞改进 |
| 5.2.2 DQYSP协议漏洞改进 |
| 5.3 协议模型优化策略 |
| 5.3.1 优化策略 |
| 5.3.2 分类压缩 |
| 5.4 协议安全问题小结 |
| 第六章 总结与展望 |
| 6.1 工作总结 |
| 6.2 未来展望 |
| 参考文献 |
| 个人简历 在校期间科研成果 |
| 致谢 |
四、Needham Schroeder协议的安全缺陷与改进（论文参考文献）
- [1]检测类型缺陷的形式化构造攻击方法[J]. 王建华,张岚. 密码学报, 2021(06)
- [2]安全协议形式化分析技术的应用与研究[D]. 冯皓楠. 北京邮电大学, 2021(01)
- [3]网络安全协议的形式化自动验证优化研究[D]. 杨锦翔. 中国科学技术大学, 2021(09)
- [4]基于强化学习的安全协议形式化自动验证技术研究[D]. 苏诚. 中国科学技术大学, 2020(01)
- [5]基于Event-B对存在网络攻击的安全协议的改进研究[J]. 朱俊翔,张翔. 中国电子科学研究院学报, 2020(06)
- [6]基于单光子的双向量子身份认证协议及其安全性形式化分析[D]. 赵怡静. 北京工业大学, 2020(06)
- [7]基于强化学习的网络安全协议形式化验证与应用技术研究[D]. 欧阳恒一. 中国科学技术大学, 2020(10)
- [8]基于多反例的安全协议分析研究与实现[D]. 王晓晗. 电子科技大学, 2020(07)
- [9]基于事件逻辑的移动支付协议形式化分析[D]. 杨科. 华东交通大学, 2019(07)
- [10]无线体域网环境下三方认证协议的形式化分析与研究[D]. 谌佳. 华东交通大学, 2019(07)