一、安全协议形式化分析理论与方法研究综述（论文文献综述）
陈焕新[1]（2021）在《基于Fabric的公平合同签署协议及其形式化验证研究》文中研究说明保证交易的公平性对于解决网络交易风险的不确定性具有至关重要的作用,为之出现的公平合同签署协议（Fair Contract Signing Protocol,FCSP）,根据有无可信第三方分为两种模式。其中传统中心化的有可信第三方管理模式随着网络交易的快速发展负担越来越大;而无可信第三方管理中引入区块链技术完成去中心化实现,不仅可以避免因第三方的频繁参与而导致的性能瓶颈,而且分布式实现模式降低了交易的公平成本。然而蓬勃发展的线上交易市场也使得区块链应用越来越复杂,如何利用区块链技术既保证交易的公平性又不影响交易效率是当前网络交易市场亟待解决的关键问题之一。在综合分析基于区块链公平合同签署协议的国内外研究现状后,本文研究并提出一种基于Fabric的公平合同签署协议及其形式化验证方法,设计了车险区块链中的公平合同签署协议,并给出其公平性形式化证明。论文的具体工作如下:针对现有的基于区块链的公平合同签署协议存在的问题,包括内容复杂、效率低、应用困难等,提出基于Fabric联盟链的快速公平合同签署协议（Towards Fair Contract Signing Protocol,TFCSP）,本文详细描述了该协议的设计思路,将协议划分为三个阶段,分别在交易的提交、验证、上传三个阶段提供了公平性保障。另外设计了车险区块链的架构,并在Fabric联盟链上模拟了车险交易环境,对多种基于区块链的公平合同签署协议进行性能比较,证明了本文所提出协议的有效性。针对区块链链码（智能合约）上链即不可修改的属性和线上存在大额交易现象,应用在区块链上的协议必须严格保证其正确,因此综合基于交替迁移系统（Alternating-time Temporal Logic,ATL）的模型检测和基于BAN（Burrows,Abadi and Needham,BAN）逻辑的定理证明,沿用一种已有的针对协议的形式化分析方法—状态转换模型,提出针对TFCSP的交替状态转换系统,通过对协议的消息、进程、规范和执行序列进行形式化描述,建立起协议的状态交替转换模型,并描述出其形式化验证目标。通过对协议系统状态转换的数学推导,证明系统状态在可信执行序列下能够满足公平性。另外,本文使用形式化验证工具对协议进行公平性自动化验证,同样证明了所提出协议的公平性。本文针对当前基于区块链的公平合同签署协议存在的各种问题,提出了基于Fabric的公平合同签署协议及其形式化验证方法,为公平合同签署协议的发展提供了新的思路。
冯皓楠[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]（2020）在《基于模型检测的区块链混币机制协议形式化分析与验证》文中研究说明区块链是对传统互联网的一种变革,被称作是下一代互联网。混币作为区块链中一种密码货币,受到很大关注并广泛应用于区块链领域中。然而,因混币中第三方的存在,其面临着与传统中心化系统同样的安全问题,可信第三方存在泄漏混币地址之间关联的可能,使得混币操作失去意义。区块链混币机制协议是保证区块链安全和隐私的关键方法,设计安全的区块链混币机制协议尤为重要。区块链混币机制协议是一种匿名通信协议,形式化分析区块链混币机制协议匿名性还处于发展阶段。MIXCOIN协议是一种典型的区块链混币机制协议,针对MIXCOIN协议存在可能泄漏用户地址关联性,使得MIXCOIN协议不满足匿名性。本文提出一种基于模型检测的形式化方法研究MIXCOIN协议匿名性安全问题。论文主要工作如下:（1）提出MIXCOIN协议形式化抽象表示方法。该方法在假设协议使用的密码系统是完备的情况下,首先简化MIXCOIN协议中实体个数,其次约简加解密钥串表示,最后定义比特币转移函数。通过该方法解决MIXCOIN协议难以使用形式化分析和形式化表示问题。（2）改进Dolev-Yao攻击者建模方法。该方法通过引入敌手控制通道,对网络通信假设进行扩展,可以更好地分析匿名通信协议。采用改进后的Dolev-Yao攻击者建模方法对MIXCOIN协议进行建模,运用线性时态逻辑对MIXCOIN协议性质进行刻画,通过SPIN工具对协议验证,实验生成攻击序列图,表明MIXCOIN协议不满足匿名性。（3）提出基于椭圆曲线盲签名机制和数组方式,对MIXCOIN协议关键信息进行盲签名和公钥地址更新的改进方法。该方法在椭圆曲线盲签名机制基础上引入辅助进程通道操作,通过该辅助进程通道实现协议盲签操作,同时用数组方式模拟实现公钥地址更新操作,可以更好地分析改进协议。MIXCOIN协议在消息项内增加盲签名操作和用数组方式模拟实现公钥地址更新操作,利用敌手控制通道,对改进后的MIXCOIN协议进行建模,通过SPIN验证,实验得出改进后的MIXCOIN协议是安全的,匿名性更强。本文所提出MIXCOIN协议形式化抽象表示方法以及改进的Dolev-Yao攻击者建模方法对此类区块链混币机制协议形式化分析具有重要意义;提出采用椭圆曲线盲签名机制对协议关键信息进行盲签名和用数组方式模拟实现公钥地址更新的改进方法,并引入辅助进程通道实现协议盲签操作,证明能提高协议发送者匿名性。可用于此类区块链混币机制协议的设计与分析。
薄尊旭[4]（2020）在《基于改进PBFT算法的区块链中Sybil攻击防御方法研究》文中指出随着区块链技术越来越受到人们的关注,区块链技术在实际应用中的安全问题也显得日益重要。从技术的本质上来说区块链是一个去中心化的数据库,在金融、医疗、物流运输等诸多方面展现出了巨大的潜在应用价值。但由于区块链中的网络架构采用的是P2P的网络架构,容易遭受Sybil攻击。Sybil攻击是由恶意节点通过伪造多个虚假身份加入到区块链网络中并试图对网络产生恶劣影响,通常配合Eclipse攻击一同来发起攻击。当区块链中的正常节点受到攻击时,无论是发出还是接收的请求信息都可能被Sybil节点截获并进行篡改,如果正常节点收到的信息是被Sybil节点篡改过的,那么就无法进行正常的共识过程,破坏网络的拓扑结构,阻碍区块链中的节点达成共识,从而为自身谋取不正当的利益。Sybil攻击不仅会破坏P2P网络中资源共享的安全性、消耗正常节点的计算资源,严重时甚至会控制整个网络系统,因此这种攻击对区块链技术有着极大的危害。为了防御区块链中的Sybil攻击,通过对PBFT算法进行改进,提出了一种基于改进PBFT算法防御区块链中Sybil攻击的方法。本文主要的研究内容如下:（1）本文提出的PBFT共识算法的改进设计借鉴基于权益证明（POS）的共识算法的思想。将节点的信誉值大小和节点在共识过程中的投票权重相联系,通过在区块链节点中建立信誉模型根据各节点共识过程中的行为来计算节点的信誉值,并依据信誉值的大小赋予节点不同的话语权。（2）同时在改进的PBFT共识算法中加入了Pre-Commit阶段来减少节点间通信的次数,提高节点间共识的效率。并且根据节点信誉值的大小和可信状态来更新共识过程中有问题的主节点,并且选取信誉值最高的节点作为主节点。（3）最后对改进后的共识协议进行形式化证明,通过实验证明改进后的共识协议仍然是安全的,可以有效的防御区块链中的Sybil攻击。
王旭阳[5]（2019）在《基于ProVerif扩展工具的附着协议关联性攻击验证》文中进行了进一步梳理安全协议是目前保证信息交互在安全条件下进行的基础。然而,安全协议从设计到部署的过程并不容易,因为安全协议通常会存在缺陷。故需要一套方案来检测安全协议的安全性。目前针对安全协议的安全问题验证,主要有逻辑分析方法、定理证明方法以及形式化验证等方法,其中形式化验证是目前普遍认可的方案。针对5G附着请求流程以及其他几个安全协议,本文使用形式化方法验证其安全性。其中在5G附着请求中失败附着流程可能会产生关联性攻击问题,而在形式化工具ProVerif中无法自动化验证,针对该问题,本文在ProVerif工具的基础上扩展。针对协议中的关联性攻击验证,扩展工具对输入的形式化描述的协议自动构建关联攻击相关属性。与ProVerif工具验证对比,扩展工具实现了自动化构建关联性攻击的相关安全属性,输入文件中无需构建相关属性。实验结果表明,本文的5G附着协议中失败的附着请求安全策略可以抵抗关联性攻击,扩展的工具也能够自动化验证安全协议的关联性攻击问题。本文通过形式化工具ProVerif验证表明本文5G附着请求安全策略是有效的,达到了抗关联性攻击的目的。其中针对安全协议中关联攻击验证问题,对ProVerif工具扩展,扩展后的工具可自动化验证关联性攻击,实验结果也表明该工具能达到此目的。
李娅楠[6]（2018）在《基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析》文中研究说明安全协议保障信息资源在交互过程中的机密性、完整性及可用性。形式化方法规范密码协议的安全特性,拥有较完善的理论体系及模型。定理证明是形式化方法的一种,基于严格数学理论知识和逻辑推导,确定协议是否在合理假设下满足要验证的安全属性。事件逻辑理论是一种描述并发与分布式系统中状态迁移和算法的定理证明方法,可用于证明网络协议的安全性。本文运用事件逻辑理论分析无线Mesh网络客户端认证协议安全性,降低协议分析过程中的冗余度及复杂度,提高协议分析效率。论文主要工作如下:（1）基于事件逻辑理论,结合事件结构、事件类、公理簇以及随机数引理等,提出置换规则保证协议交互用户在置换中性质的等价转换,推导出多组合信息交互、不叠加、事件匹配、去重复、去未来等性质,扩展事件逻辑理论在协议分析中的应用。（2）通过事件逻辑描述客户端与LTCA间交互协议的基本序列,对协议交互动作形式化描述。证明协议强认证性质,得出无线Mesh网络客户端与LTCA间认证协议在合理假设下是安全的。表明事件逻辑理论可以对安全协议不同身份主体间的认证性进行证明。（3）在客户端用户已得到LCA颁发的认证证书条件下,通过事件逻辑理论证明无线Mesh网络客户端间认证协议安全性,得出无线Mesh网络客户端间认证协议在合理假设下是安全的。表明事件逻辑理论不仅可以证明有线网络协议安全属性,对无线网络协议的安全属性也可以论证,从而保证安全协议在信息交互过程的可靠性。（4）详述事件逻辑理论证明协议安全属性过程,通过流程图简化协议形式化证明步骤,体现事件逻辑理论的指导实用性。比较分析事件逻辑理论与其它逻辑推理方法,表明事件逻辑理论具有通用性。
刘欣倩[7]（2016）在《基于事件逻辑的可证明网络安全协议形式化分析》文中研究表明形式化方法是分析网络安全协议的一种重要方法,也是信息安全领域的研究热点。形式化方法基于严格的数学概念和逻辑方法,对协议进行描述,在描述过程中可发现协议安全属性的不明确或不完整,有效地降低分析过程复杂度,使协议的安全分析简单、规范、实用。定理证明是形式化方法的一种,目的是证明无穷并发状态下网络安全协议是安全的。事件逻辑是在并发与分布式系统下描述协议和算法的逻辑,是定理证明中一种非常重要的逻辑方法。本文以事件逻辑为基础,对其进行扩展,提出强认证理论。针对Needham-Schroeder（NS）协议和Neuman-Stubblebine协议进行形式化描述及认证性证明。论文主要工作包括:1、基于事件逻辑,对安全协议的七种动作（生成挑战数、发送消息、接收消息、加密、解密、签名和验证）进行形式化描述,同时给出协议中密钥、挑战数和协议消息的形式化描述。定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出强认证理论。2、对两个主体的NS协议进行研究,针对协议漏洞,对其增加时间戳,避免了重放攻击,运用事件逻辑对改进后的协议进行形式化描述,通过对发送者和接收者的认证证明,说明强认证理论适用于两方的网络安全协议;对三个主体的Neuman-Stubblebine协议进行研究,运用事件逻辑对协议基本序列进行合法定义,证明发送者是安全的而接收者是不安全的,不能达到双向身份认证,说明强认证理论也适用于三方的网络安全协议。3、通过以上分析,认证协议可以通过只对协议诚实主体动作的推理来证明其认证性,事件逻辑适用于多个主体的网络安全协议认证性分析。
张兴,韩冬,马晓光[8]（2015）在《智能化电视网络安全协议的验证方法综述》文中研究说明在有线电视网络领域,安全的网络通信协议是信息安全传输的保障,因此研究有效的协议安全性验证方法显得至关重要。当前,随着互联网的普及,数字电视的双向化、智能化趋势日益明显,处于互联网中的数字电视将面临严峻的信息安全威胁,必须通过通信协议的安全性验证法选择出安全性更高的通信协议,才能确保双向数字电视传输网络的安全性。目前,关于验证通信协议的方法主要分为逻辑推理分析法、模型模拟检测法、定理归纳证明法以及其他衍生验证法。在前期研究的基础上,对近五年提出的典型协议验证方法进行总结比较,分析各验证方法的优缺点。最后,对协议验证领域存在的问题及未来的发展趋势做以阐述。
高尚,胡爱群,石乐,陈先棒[9]（2014）在《安全协议形式化分析研究》文中进行了进一步梳理计算机网络中,安全协议为通信双方的信息交互提供安全保证,是计算机网络安全的基础.而当安全协议中存在安全漏洞时,会对信息安全产生重大威胁,造成数据泄露、身份被冒用等危害.因此,对于安全协议安全性的研究,历来都属于安全领域的重要研究方向.目前的安全性分析方法主要是通过协议形式化分析与验证来实现.形式化分析方法的理论体系大致可分为三类:模态逻辑技术、模型检测技术和定理证明技术.在不同类别的理论体系中,所使用的技术方法各有不同,对安全协议分析的侧重点也略有不同.对于每一种理论体系,研究者们也提出了不同的方法,以及针对经典方案的改进来提高形式化分析的准确性.对于复合协议,其主要问题是通过对多种现有可靠安全协议加以组合,构成新的协议并保持其安全性可靠.对于复合协议的安全性分析,也有异于普通的安全协议形式化分析.本文总结了各种类别中的主要分析方法,并比较了每种方法的优缺点,同时特别针对复合协议的安全性分析技术进行了概述.最后指出了形式化分析方法中需要解决的问题,以及下一步的研究方向.
韩世宁[10]（2014）在《基于PCL的安全协议匿名性形式化分析方法的研究》文中研究表明目前,大量的安全协议已经被设计出来,如何验证这些协议是否满足声称的安全性是协议设计与分析的一个重要研究领域。为了验证和分析协议的安全性,密码学家提出了不同的基于符号的形式化方法,如模态逻辑,模型检测逻辑,定理证明逻辑。然而大多数形式化方法都集中在协议的认证性和机密性的分析上,且这些方面的研究已经很成熟,而其他安全属性,如匿名性的形式化分析还处在起步阶段。为了进一步完善安全协议形式化分析理论和更好地分析协议的匿名属性,本文提出一种基于协议组合逻辑（PCL）的匿名性分析方法。通过将观察等价思想和PCL理论相结合,提出分析协议匿名性的形式化方法,并且将这种新的形式化方法应用到具体的网络协议中,通过实例分析说明了该方法的可行性和正确性。本文首先阐述了协议形式化分析研究的背景及意义,指出匿名性形式化分析的研究现状和目前存在的一些不足,介绍了安全协议、匿名性和形式化方法的基本概念,并归纳总结了三类常见的形式化方法,详细描述和分析了一种主要的形式化分析方法——PCL模型。其次,针对协议组合逻辑（PCL）缺乏匿名性分析能力的问题,提出一种新的匿名性形式化分析方法。考虑到协议交互过程中涉及到的信息,将PCL中的消息重新定义为三类：明文,密文和组合消息；结合观察者的分析能力,针对以上三类消息,定义了五条消息等价定理,并归纳了消息等价的语义；在消息等价的基础上,结合迹的概念,定义了迹等价语义；并在迹等价定义的基础上,定义了发送者匿名性、接收者匿名性和关系匿名性。最后,为了验证新方法在形式化分析协议匿名性方面的可行性和正确性,本文选用直接匿名认证协议（DAA）作为新方法的应用实例。使用新方法分别对DAA的两个子协议的匿名性进行形式化推理证明,分析结果表明,DAA协议满足匿名性,并验证了新方法的可行性和正确性。
二、安全协议形式化分析理论与方法研究综述（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、安全协议形式化分析理论与方法研究综述（论文提纲范文）
（1）基于Fabric的公平合同签署协议及其形式化验证研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第1章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.2.1 基于区块链的公平合同签署研究现状 |
| 1.2.2 公平合同签署协议形式化验证研究现状 |
| 1.3 论文主要研究内容 |
| 1.4 论文组织结构 |
| 第2章 相关理论与技术 |
| 2.1 区块链技术 |
| 2.1.1 比特币 |
| 2.1.2 以太坊 |
| 2.1.3 Fabric |
| 2.2 形式化分析理论与技术 |
| 2.2.1 针对协议的形式化分析基础 |
| 2.2.2 基于交替迁移系统的模型检测 |
| 2.2.3 基于BAN逻辑的定理证明 |
| 2.3 本章小结 |
| 第3章 基于Fabric的快速公平合同签署协议 |
| 3.1 TFCSP设计思路 |
| 3.1.1 交易合同的发起机制设计 |
| 3.1.2 合同内容校验机制设计 |
| 3.1.3 合同签署完成机制设计 |
| 3.2 公平合同签署模式的车险区块链 |
| 3.3 实验分析 |
| 3.3.1 实验环境 |
| 3.3.2 评价指标 |
| 3.3.3 实验结果与分析 |
| 3.4 本章小结 |
| 第4章 TFCSP协议的形式化分析与验证 |
| 4.1 针对TFCSP的状态转换系统 |
| 4.1.1 消息建模 |
| 4.1.2 进程建模 |
| 4.1.3 状态转换系统模型 |
| 4.1.4 定义协议规范 |
| 4.1.5 定义执行序列 |
| 4.2 TFCSP协议分析 |
| 4.2.1 TFCSP协议 |
| 4.2.2 协议的抽象 |
| 4.2.3 TFCSP协议的形式化规范 |
| 4.3 交易过程的公平性定义 |
| 4.4 协议的形式化分析与证明 |
| 4.5 实验分析 |
| 4.5.1 实验环境 |
| 4.5.2 验证过程 |
| 4.5.3 实验结果 |
| 4.6 本章小结 |
| 第5章 总结与展望 |
| 5.1 总结 |
| 5.2 展望 |
| 参考文献 |
| 攻读学位期间取得的科研成果 |
| 致谢 |
（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.2 研究现状 |
| 1.3 研究内容 |
| 1.4 论文结构 |
| 第二章 基础知识 |
| 2.1 匿名相关概念 |
| 2.1.1 匿名性 |
| 2.1.2 匿名属性分类 |
| 2.2 椭圆曲线的盲签名方案 |
| 2.2.1 参数选择 |
| 2.2.2 消息签名及其验证 |
| 2.3 形式化分析方法及验证工具 |
| 2.3.1 形式化方法概述 |
| 2.3.2 模型检测工具SPIN |
| 2.4 区块链混币机制协议 |
| 2.4.1 混币机制协议分类 |
| 2.4.2 典型的MIXCOIN协议 |
| 2.4.3 MIXCOIN协议安全问题 |
| 2.5 本章小结 |
| 第三章 区块链混币机制协议的形式化分析与验证 |
| 3.1 协议形式化抽象表示方法 |
| 3.2 MIXCOIN协议形式化表示 |
| 3.3 协议通信模型假设及安全属性刻画 |
| 3.3.1 通信模型假设 |
| 3.3.2 安全属性刻画 |
| 3.4 基于SPIN的 MIXCOIN协议模型检测 |
| 3.4.1 诚实主体建模 |
| 3.4.2 攻击者建模 |
| 3.4.3 验证结果与分析 |
| 3.5 本章小结 |
| 第四章 基于椭圆曲线盲签名的改进协议模型检测 |
| 4.1 MIXCOIN改进协议 |
| 4.2 改进协议的模型检测 |
| 4.2.1 改进协议建模 |
| 4.2.2 验证结果与分析 |
| 4.3 本章小结 |
| 第五章 总结与展望 |
| 5.1 工作总结 |
| 5.2 未来工作展望 |
| 参考文献 |
| 附录 基于椭圆曲线盲签名机制的MIXCOIN协议模型检测Promela代码 |
| 个人简历在读期间发表的学术论文 |
| 致谢 |
（4）基于改进PBFT算法的区块链中Sybil攻击防御方法研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 研究背景与意义 |
| 1.2 国内外研究现状 |
| 1.2.1 区块链的研究现状 |
| 1.2.2 sybil攻击的研究现状 |
| 1.2.3 信誉模型的研究现状 |
| 1.3 研究内容 |
| 1.4 论文结构 |
| 第2章 相关技术综述 |
| 2.1 实用拜占庭容错算法 |
| 2.1.1 算法流程 |
| 2.1.2 视图变更机制 |
| 2.2 区块链技术 |
| 2.2.1 区块链概述 |
| 2.2.2 区块链底层技术原理 |
| 2.3 协议的形式化证明 |
| 2.3.1 SVO逻辑概述 |
| 2.3.2 SVO逻辑基本语义 |
| 2.3.3 SVO逻辑的基本公理 |
| 2.4 本章小节 |
| 第3章 共识算法的改进 |
| 3.1 系统模型 |
| 3.2 建立信誉模型 |
| 3.3 主节点更新算法 |
| 3.4 共识算法改进 |
| 3.5 本章小节 |
| 第4章 共识算法的形式化分析验证 |
| 4.1 共识协议的安全性分析 |
| 4.1.1 协议的理想化描述 |
| 4.1.2 协议的初始化假设 |
| 4.1.3 协议的安全目标 |
| 4.1.4 协议分析 |
| 4.2 协议的安全性测试 |
| 4.2.1 AVISPA测试工具 |
| 4.2.2 基本角色 |
| 4.2.3 会话场景 |
| 4.2.4 安全目标 |
| 4.2.5 实验结果 |
| 4.3 本章小节 |
| 第5章 改进算法的性能分析与评估 |
| 5.1 系统的设计与实验 |
| 5.1.1 系统开发环境 |
| 5.1.2 系统的设计 |
| 5.2 改进PBFT算法的安全性分析 |
| 5.3 实验结果及分析 |
| 5.3.1 区块链TPS性能的比较 |
| 5.3.2 生成区块延迟时间比较 |
| 5.3.3 时间复杂度的比较 |
| 5.4 本章小节 |
| 结论 |
| 参考文献 |
| 攻读硕士学位期间发表的学位论文 |
| 致谢 |
（5）基于ProVerif扩展工具的附着协议关联性攻击验证（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第1章 绪论 |
| 1.1 研究背景和意义 |
| 1.2 研究内容 |
| 1.3 论文组织结构 |
| 第2章 相关技术综述 |
| 2.1 安全协议 |
| 2.1.1 密码原语 |
| 2.1.2 安全协议应用 |
| 2.2 形式化方法 |
| 2.2.1 计算模型 |
| 2.2.2 符号模型 |
| 2.2.3 形式化应用领域 |
| 2.3 形式化验证工具 |
| 2.4 本章小结 |
| 第3章 安全协议描述及分析 |
| 3.1 基于归属地网络公钥而增强附着流程安全性协议 |
| 3.1.1 成功附着流程 |
| 3.1.2 失败附着流程 |
| 3.1.3 关联性攻击分析 |
| 3.2 基于口令和PKI的混合认证协议 |
| 3.2.1 基于口令和数字签名的方案 |
| 3.2.2 基于口令和公钥加密的方案 |
| 3.2.3 协议分析 |
| 3.3 基于IBC的And-link认证协议 |
| 3.4 本章小结 |
| 第4章 针对关联性攻击的ProVerif工具扩展 |
| 4.1 ProVerif介绍 |
| 4.1.1 ProVerif工具结构 |
| 4.1.2 Applied Pi演算 |
| 4.2 基于ProVerif的扩展工具设计 |
| 4.2.1 问题描述 |
| 4.2.2 扩展理论基础 |
| 4.3 基于ProVerif的扩展工具实现 |
| 4.3.1 扩展工具整体整体结构 |
| 4.3.2 扩展工具与ProVerif工具对比 |
| 4.4 扩展工具测试 |
| 4.5 本章小结 |
| 第5章 安全协议的验证 |
| 5.1 ProVerif验证过程 |
| 5.2 基于ProVerif的协议验证 |
| 5.2.1 基于口令和数字签名方案验证 |
| 5.2.2 基于口令和公钥加密方案验证 |
| 5.2.3 对基于IBC的Andlink认证协议验证 |
| 5.3 5G附着协议关联攻击的验证 |
| 5.3.1 ProVerif验证失败附着流程 |
| 5.3.2 扩展工具验证流程 |
| 5.3.3 扩展工具验证附着流程关联性攻击 |
| 5.4 本章小结 |
| 第6章 总结与展望 |
| 6.1 总结 |
| 6.2 未来展望 |
| 参考文献 |
| 发表论文和参加科研情况说明 |
| 致谢 |
（6）基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析（论文提纲范文）
| 摘要 |
| abstract |
| 符号说明 |
| 第一章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 发展历史及研究现状 |
| 1.3 本文主要内容 |
| 1.4 论文结构安排 |
| 第二章 无线Mesh网络协议及形式化方法概述 |
| 2.1 无线Mesh网络 |
| 2.1.1 无线Mesh网络概述 |
| 2.1.2 无线Mesh网络的安全威胁 |
| 2.1.3 无线Mesh网络认证协议的安全需求 |
| 2.2 无线Mesh网络客户端协议分析 |
| 2.2.1 WMN客户端与LTCA间认证协议 |
| 2.2.2 WMN客户端间认证协议 |
| 2.3 形式化方法概述 |
| 2.3.1 模型检测 |
| 2.3.2 定理证明 |
| 第三章 事件逻辑理论 |
| 3.1 事件逻辑理论 |
| 3.1.1 基本定义 |
| 3.1.2 加密系统建模 |
| 3.2 事件逻辑理论公理、推论及性质 |
| 3.2.1 事件逻辑理论公理 |
| 3.2.2 事件逻辑理论推论及性质 |
| 3.3 形式化方法描述协议 |
| 3.3.1 线程和基本序列 |
| 3.3.2 匹配会话及协议动作 |
| 3.3.3 事件逻辑方法描述协议 |
| 3.4 安全协议证明过程 |
| 3.4.1 事件逻辑理论方法证明流程详述 |
| 3.4.2 事件逻辑理论方法证明流程 |
| 3.5 本章小结 |
| 第四章 无线Mesh网协议形式化分析 |
| 4.1 WMN客户端与LTCA间双向认证协议证明 |
| 4.1.1 协议的形式化分析 |
| 4.1.2 协议证明过程 |
| 4.2 WMN客户端间双向协议认证性证明 |
| 4.2.1 协议的形式化分析 |
| 4.2.2 协议证明过程 |
| 4.3 本章小结 |
| 第五章 形式化方法对比分析 |
| 5.1 事件逻辑理论与模态逻辑比较 |
| 5.2 事件逻辑理论与PCL比较 |
| 5.3 事件逻辑理论通用性 |
| 第六章 总结与展望 |
| 6.1 总结 |
| 6.2 展望 |
| 参考文献 |
| 个人简历在读期间发表的学术论文 |
| 致谢 |
（7）基于事件逻辑的可证明网络安全协议形式化分析（论文提纲范文）
| 摘要 |
| abstract |
| 第一章 绪论 |
| 1.1 研究背景及意义 |
| 1.2 发展历史及研究现状 |
| 1.3 本文主要内容 |
| 1.4 论文结构安排 |
| 第二章 网络安全协议形式化概述 |
| 2.1 安全协议 |
| 2.1.1 安全协议分类 |
| 2.1.2 安全协议系统模型 |
| 2.1.3 安全属性 |
| 2.2 安全协议基础理论与方法 |
| 2.3 形式化分析方法 |
| 2.3.1 非形式化方法的不足 |
| 2.3.2 形式化方法的优点 |
| 2.3.3 两者之间的关系 |
| 第三章 事件逻辑理论 |
| 3.1 事件系统 |
| 3.1.1 消息自动机 |
| 3.1.2 分布式系统 |
| 3.1.3 事件系统语法和语义 |
| 3.1.4 事件系统结构 |
| 3.2 事件逻辑 |
| 3.2.1 基本定义 |
| 3.2.2 事件逻辑公理 |
| 3.2.3 推理规则及性质 |
| 3.2.4 基本序列 |
| 3.2.5 形式化协议 |
| 3.2.6 合法序列 |
| 3.3 强认证理论 |
| 3.3.1 线程 |
| 3.3.2 匹配会话 |
| 3.3.3 认证 |
| 3.4 本章小结 |
| 第四章 协议实例证明 |
| 4.1 改进的Needham-Schroeder协议证明 |
| 4.1.1 协议的形式化分析及描述 |
| 4.1.2 协议证明过程 |
| 4.2 Neuman-Stubblebine协议证明 |
| 4.2.1 协议的形式化分析及描述 |
| 4.2.2 协议证明过程 |
| 4.3 本章小结 |
| 第五章 总结与展望 |
| 5.1 总结 |
| 5.2 展望 |
| 参考文献 |
| 个人简历在读期间的成果 |
| 致谢 |
（8）智能化电视网络安全协议的验证方法综述（论文提纲范文）
| 1 逻辑推理分析法 |
| 2 模型模拟检测法 |
| 3 定理归纳证明法 |
| 4 其他衍生验证法 |
| 5 协议验证法的比较 |
| 6 总结与展望 |
（10）基于PCL的安全协议匿名性形式化分析方法的研究（论文提纲范文）
| 摘要 |
| Abstract |
| 插图索引 |
| 附表索引 |
| 第1章 绪论 |
| 1.1 研究背景及课题来源 |
| 1.2 国内外研究现状 |
| 1.3 选题意义 |
| 1.4 本文的主要研究工作 |
| 1.5 本文的结构安排 |
| 第2章 基础知识 |
| 2.1 安全协议 |
| 2.1.1 安全协议概述 |
| 2.1.2 安全协议分类及安全属性 |
| 2.2 匿名相关概念 |
| 2.2.1 匿名性基本概念 |
| 2.2.2 匿名属性分类 |
| 2.3 形式化方法的构成 |
| 2.3.1 形式化描述 |
| 2.3.2 形式化验证 |
| 2.4 形式化方法 |
| 2.4.1 协议分析的基本假设 |
| 2.4.2 模态逻辑方法 |
| 2.4.3 模型检测方法 |
| 2.4.4 定理证明方法 |
| 2.5 本章小结 |
| 第3章 PCL模型 |
| 3.1 协议组合逻辑概述 |
| 3.2 基本的PCL框架 |
| 3.2.1 协议的模型化 |
| 3.2.2 语法 |
| 3.2.3 语义 |
| 3.2.4 证明系统 |
| 3.3 PCL理论研究现状 |
| 3.4 PCL与其他形式化方法的比较 |
| 3.5 本章小结 |
| 第4章 基于PCL的匿名性形式化分析新方法APCL |
| 4.1 安全假设 |
| 4.2 语法 |
| 4.3 等价语义 |
| 4.3.1 消息等价语义 |
| 4.3.2 迹等价语义 |
| 4.4 基于等价的匿名框架 |
| 4.5 形式化分析DAA协议的匿名性 |
| 4.5.1 直接匿名认证协议(DAA) |
| 4.5.2 DAA协议的抽象化表示 |
| 4.5.3 DAA-Join协议的形式化分析 |
| 4.5.4 DAA-Sign协议的形式化分析 |
| 4.6 本章小结 |
| 结论与展望 |
| 参考文献 |
| 致谢 |
| 附录A 攻读学位期间所发表的学术论文 |
四、安全协议形式化分析理论与方法研究综述（论文参考文献）
- [1]基于Fabric的公平合同签署协议及其形式化验证研究[D]. 陈焕新. 太原理工大学, 2021(01)
- [2]安全协议形式化分析技术的应用与研究[D]. 冯皓楠. 北京邮电大学, 2021(01)
- [3]基于模型检测的区块链混币机制协议形式化分析与验证[D]. 王西忠. 华东交通大学, 2020(05)
- [4]基于改进PBFT算法的区块链中Sybil攻击防御方法研究[D]. 薄尊旭. 北京工业大学, 2020(06)
- [5]基于ProVerif扩展工具的附着协议关联性攻击验证[D]. 王旭阳. 天津大学, 2019(06)
- [6]基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析[D]. 李娅楠. 华东交通大学, 2018(12)
- [7]基于事件逻辑的可证明网络安全协议形式化分析[D]. 刘欣倩. 华东交通大学, 2016(04)
- [8]智能化电视网络安全协议的验证方法综述[J]. 张兴,韩冬,马晓光. 电视技术, 2015(23)
- [9]安全协议形式化分析研究[J]. 高尚,胡爱群,石乐,陈先棒. 密码学报, 2014(05)
- [10]基于PCL的安全协议匿名性形式化分析方法的研究[D]. 韩世宁. 兰州理工大学, 2014(10)