导读:本文包含了非形式化分析论文开题报告文献综述及选题提纲参考文献，主要关键词:Kerberos,PKINIT,一次性口令,口令猜测攻击
非形式化分析论文文献综述
马利民,张伟,宋莹[1]（2019）在《一种基于一次性口令的增强Kerberos协议方法及其形式化分析》一文中研究指出Kerberos协议是分布式网络中一种重要的基于可信第叁方认证协议,广泛应用于各主流操作系统以及云计算、无线网络等场景,但容易受到口令猜测攻击、重放攻击等。虽然基于公钥密码学的PKINIT协议可以增强Kerberos协议对这些攻击的抵抗能力,但需引入过多的计算资源和通信代价。为此,文章提出并实现了一种基于一次性口令机制以增强Kerberos协议安全性的方案,并基于BAN逻辑进行形式化分析。实验结果显示,该方案与PKINIT协议相比,计算复杂度降低,初始认证服务所需时间减少为PKINIT协议的67.7%,并具有容易部署的优点。(本文来源于《信息网络安全》期刊2019年10期）
杨文霞[2]（2019）在《移动支付协议的形式化分析与安全性研究》一文中研究指出随着第四代移动通信技术的成熟应用以及各种智能设备的兴起,移动支付凭借着它的便利性和快捷性等特点几乎覆盖了人们生活的各个方面。为了保证移动支付顺利、安全的进行,在进行通信以及数据传输时,所采用的移动支付协议的安全性就成为人们关注的重点。目前,形式化分析是协议安全性分析的有效方法之一。因此,在信息安全领域中,对移动支付协议的形式化分析与安全性研究已成为一个重要课题。移动支付协议在移动终端中运行,与传统支付协议不同的是,应当考虑到移动终端在存储空间、电量及计算水平等方面均有限的特点,因此应尽量选取轻量级的采用对称密钥加密的移动支付协议。Tan Soo Fun等人于2008年基于移动运营商MNO提出LMPP协议(Lightweight Mobile Payment Protocol),该协议采用对称密钥加密,减少了相关各方之间的计算量和通信量,并实现了对买方的完全隐私保护,满足了端到端的安全属性和各方要求的所有标准,并在2012年继续对协议进行可追究性分析,提出了4个分析目标,运用KP逻辑进行分析验证,验证结果表明,LMPP协议满足可追究性。Farahnaz Zamanian等人于2016年对LMPP协议进行分析,发现卖方在匿名性和不可链接性存在安全问题,提出了一种解决方案,从而满足了卖方的匿名性和不可链接性。本文选取以移动运营商MNO为价值链的轻量级隐私保护的移动支付协议为研究对象,对协议的两个部分进行分析。注册协议部分,对Diffie-Hellman算法进行改进,并选取一定数量的大素数进行实验,实验结果表明改进后的算法降低了共享密钥生成所需的计算量,运算时间也明显降低,从而使协议更适用于资源有限的移动设备。支付协议部分,采用SVO逻辑方法形式化地分析移动支付协议,通过推理证明,发现协议不满足公平性,对协议作出改进。然后对改进后的协议,再次运用SVO逻辑推理证明,并通过使用Promela语言建模的模型检测工具SPIN进行验证分析。结果均表明,改进后的协议满足公平性,从而保障了协议自身的安全属性。本文的研究工作主要体现为:改进后的密钥交换算法在一定程度上降低了计算量和运算时间,使协议更满足轻量级要求;改进后的支付协议保证了移动支付中不同主体的公平性,从而增强了移动支付的安全性。(本文来源于《太原理工大学》期刊2019-06-01）
邓炜[3]（2019）在《汉语比较关联句的形式化分析》一文中研究指出比较关联句式是一种普遍的语言现象,汉语的比较关联句式指的是“越...越...”这一句式。在管制约束理论和形式语义相关理论的框架下,本论文对汉语的比较关联句式进行了句法和形式语义上的分析。按照比较项“越”所修饰的词性分类,本研究将汉语比较关联句可以分为越_1+AdjP+越_2+AdjP;越_1+VP+越_2+AdjP;越_1+AdjP+越_2+VP;越_1+VP+越_2+VP;越_1+PP+越_2+AdjP五种类型。句法上,本研究继承了关联句的叁分结构,并提出了汉语关联句的句法结构。形式语义上,本研究认为量化副词“越”实际上是一个从时间、空间和个体算子到“越”所修饰的谓词程度的比较的映射,用语义函数YUE_(PREDICATE)(x)(t)(w)表示。按照“越”及其所修饰的谓词所组成词组的词性分类,本研究将“越”的语义类型分为<<e,t>,<e,t>>、<<t,t>,<t,t>>、<<<e,t>,<e,t>>,<<e,t>,<e,t>>>叁种类型。当“越”修饰谓词或者定语时,“越”的类型为<<e,t>,<e,t>>;当“越”修饰的副词是用于修饰句子时,“越”的类型为<<t,t>,<t,t>>;当“越”修饰的副词是用于修饰谓词时,“越”的类型为<<<e,t>,<e,t>>,<<e,t>,<e,t>>>。比较项“越”在句法上只有作为副词一种词性,在语义上则映射出叁种类型,从而证明了从句法到语义的多重映射关系。(本文来源于《上海外国语大学》期刊2019-05-01）
尤江东[4]（2019）在《基于形式化分析法的情报应用模式研究》一文中研究指出网络信息环境下大数据的兴起为情报学领域带来新机遇和新挑战,该文简述了情报与情报分析的概念,指出情报分析员面临的现实挑战,对情报分析法的特点优势进行了概述,归纳了形式化情报分析法的5种应用模式,为弥补情报界在分析技术方面的不足提供了借鉴,帮助分析人员克服思维误区,为明智决策、任务成功提供更优化的情报支持。(本文来源于《科技资讯》期刊2019年11期）
姚萌萌,朱正超,刘明达[5]（2019）在《一种改进的基于认证测试的形式化分析方法》一文中研究指出近年来,认证测试定理得到了改进,并应用于各种安全协议的分析。但是这些改进定理在应用范围和准确性方面存在一定的缺陷。针对这些缺陷,文章提出了一种改进的输入测试定理及加密测试定理,并给出了改进定理的证明。通过分析认证测试中常规节点的判定、证明过程中的错误、参数一致性证明过程中的不准确性和错误,指出了认证测试在使用过程中的缺陷。基于这些缺陷,文章提出了一种改进的基于认证测试的形式化分析方法——递归测试,并通过该方法证明了BAN-Yahalom协议。分析结果表明,该方法扩大了认证测试使用范围,且可以有效地、准确地分析安全协议。(本文来源于《信息网络安全》期刊2019年01期）
钟小妹,肖美华,李伟,谌佳,李娅楠[6]（2018）在《RFID超轻量级认证协议RCIA形式化分析与改进》一文中研究指出无线射频识别(RFID)是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具SPIN对RCIA协议的认证性及一致性进行验证,结果表明RCIA协议存在去同步攻击漏洞。针对此漏洞,提出基于密钥同步机制的修补方案,对RCIA协议进行了改进。对改进后的协议进行形式化分析与验证,结果表明改进后的RCIA协议具有更高的安全性。提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。(本文来源于《计算机工程与科学》期刊2018年12期）
高强,林星辰,林宏刚,金大鹏[7]（2018）在《安全协议抗DoS攻击的形式化分析研究》一文中研究指出随着拒绝服务攻击给协议的可用性带来的危害越来越大,需要行之有效的方法对安全协议的抗DoS性进行分析.但是目前对安全协议的抗DoS性进行分析的方法模型都存在一些缺陷,有的只能分析部分的DoS攻击,有的只关注协议各方计算资源的消耗,而忽略了存储资源消耗.针对以上不足,本文对基本的串空间模型进行扩展,引入消息相关度集合和代价函数,提出了一种分析安全协议抗DoS性的新方法,并利用该方法,对JFK协议的抗DoS性进行了详细分析.(本文来源于《四川大学学报(自然科学版)》期刊2018年06期）
李伟[8]（2018）在《基于模型检测的超轻量级RFID双向认证协议形式化分析与验证》一文中研究指出物联网的飞速发展掀起了继计算机、互联网后世界信息产业的第叁次浪潮。RFID技术作为物联网的核心技术,被广泛运用于公共安全、环境监测、智能交通、智能家居等领域。然而,RFID中阅读器与标签之间的无线通信方式使RFID系统更易遭受安全攻击。RFID安全认证协议是保障RFID系统通信安全的有效途径,协议自身安全性至关重要。形式化方法作为协议安全性分析的重要手段,可保证协议分析过程的准确性和可靠性。本文重点关注超轻量级RFID双向认证协议的安全性问题。选取两个典型的超轻量级双向认证协议,Type 1型协议RCIA和Type 2型协议RAPP作为研究对象,采用形式化方法分别分析RCIA和RAPP协议的安全性,所取得研究成果有:(1)提出协议抽象建模方法。克服因超轻量级RFID双向认证协议底层加密复杂,而不便于直接使用形式化方法分析的局限,使模型检测技术能应用于RFID协议分析领域。(2)拓展Maggi的Promela建模方法。实现超轻量级安全认证协议交互过程中特有的密钥选择和密钥更新操作,运用SPIN工具验证得到RCIA和RAPP中均存在去同步攻击漏洞。(3)构建超轻量级双向认证协议通用模型G-UMAP。统一描述Type 1和Type 2型协议交互流程,以及G-UMAP中的去同步攻击漏洞。(4)提出基于G-UMAP密钥同步机制的漏洞通用修补方案,分别对RCIA和RAPP协议进行改进。改进协议形式化验证结果表明,改进后的RCIA和RAPP协议具有更高安全性。本文提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞通用修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。(本文来源于《华东交通大学》期刊2018-06-30）
李娅楠[9]（2018）在《基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析》一文中研究指出安全协议保障信息资源在交互过程中的机密性、完整性及可用性。形式化方法规范密码协议的安全特性,拥有较完善的理论体系及模型。定理证明是形式化方法的一种,基于严格数学理论知识和逻辑推导,确定协议是否在合理假设下满足要验证的安全属性。事件逻辑理论是一种描述并发与分布式系统中状态迁移和算法的定理证明方法,可用于证明网络协议的安全性。本文运用事件逻辑理论分析无线Mesh网络客户端认证协议安全性,降低协议分析过程中的冗余度及复杂度,提高协议分析效率。论文主要工作如下:(1)基于事件逻辑理论,结合事件结构、事件类、公理簇以及随机数引理等,提出置换规则保证协议交互用户在置换中性质的等价转换,推导出多组合信息交互、不迭加、事件匹配、去重复、去未来等性质,扩展事件逻辑理论在协议分析中的应用。(2)通过事件逻辑描述客户端与LTCA间交互协议的基本序列,对协议交互动作形式化描述。证明协议强认证性质,得出无线Mesh网络客户端与LTCA间认证协议在合理假设下是安全的。表明事件逻辑理论可以对安全协议不同身份主体间的认证性进行证明。(3)在客户端用户已得到LCA颁发的认证证书条件下,通过事件逻辑理论证明无线Mesh网络客户端间认证协议安全性,得出无线Mesh网络客户端间认证协议在合理假设下是安全的。表明事件逻辑理论不仅可以证明有线网络协议安全属性,对无线网络协议的安全属性也可以论证,从而保证安全协议在信息交互过程的可靠性。(4)详述事件逻辑理论证明协议安全属性过程,通过流程图简化协议形式化证明步骤,体现事件逻辑理论的指导实用性。比较分析事件逻辑理论与其它逻辑推理方法,表明事件逻辑理论具有通用性。(本文来源于《华东交通大学》期刊2018-06-30）
丁月,汪学明[10]（2018）在《一种新的复合型电子支付协议及其形式化分析》一文中研究指出针对现有复合型支付协议AECPP的单向身份认证中易受匿名攻击、支付子协议的完整性不能有效保证这些不足,提出一种新的复合型电子支付协议。新协议实现了用户与服务供应商之间的双向认证,通过引入Hash函数和经由第叁方信息的转发进一步提高了支付子协议的完整性和保密性。通过SVO逻辑和Kailar逻辑形式化分析验证可知,新的复合电子支付协议满足双向认证性、可追究性和公平性。(本文来源于《计算机应用与软件》期刊2018年06期）
非形式化分析论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
随着第四代移动通信技术的成熟应用以及各种智能设备的兴起,移动支付凭借着它的便利性和快捷性等特点几乎覆盖了人们生活的各个方面。为了保证移动支付顺利、安全的进行,在进行通信以及数据传输时,所采用的移动支付协议的安全性就成为人们关注的重点。目前,形式化分析是协议安全性分析的有效方法之一。因此,在信息安全领域中,对移动支付协议的形式化分析与安全性研究已成为一个重要课题。移动支付协议在移动终端中运行,与传统支付协议不同的是,应当考虑到移动终端在存储空间、电量及计算水平等方面均有限的特点,因此应尽量选取轻量级的采用对称密钥加密的移动支付协议。Tan Soo Fun等人于2008年基于移动运营商MNO提出LMPP协议(Lightweight Mobile Payment Protocol),该协议采用对称密钥加密,减少了相关各方之间的计算量和通信量,并实现了对买方的完全隐私保护,满足了端到端的安全属性和各方要求的所有标准,并在2012年继续对协议进行可追究性分析,提出了4个分析目标,运用KP逻辑进行分析验证,验证结果表明,LMPP协议满足可追究性。Farahnaz Zamanian等人于2016年对LMPP协议进行分析,发现卖方在匿名性和不可链接性存在安全问题,提出了一种解决方案,从而满足了卖方的匿名性和不可链接性。本文选取以移动运营商MNO为价值链的轻量级隐私保护的移动支付协议为研究对象,对协议的两个部分进行分析。注册协议部分,对Diffie-Hellman算法进行改进,并选取一定数量的大素数进行实验,实验结果表明改进后的算法降低了共享密钥生成所需的计算量,运算时间也明显降低,从而使协议更适用于资源有限的移动设备。支付协议部分,采用SVO逻辑方法形式化地分析移动支付协议,通过推理证明,发现协议不满足公平性,对协议作出改进。然后对改进后的协议,再次运用SVO逻辑推理证明,并通过使用Promela语言建模的模型检测工具SPIN进行验证分析。结果均表明,改进后的协议满足公平性,从而保障了协议自身的安全属性。本文的研究工作主要体现为:改进后的密钥交换算法在一定程度上降低了计算量和运算时间,使协议更满足轻量级要求;改进后的支付协议保证了移动支付中不同主体的公平性,从而增强了移动支付的安全性。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
非形式化分析论文参考文献
[1].马利民,张伟,宋莹.一种基于一次性口令的增强Kerberos协议方法及其形式化分析[J].信息网络安全.2019
[2].杨文霞.移动支付协议的形式化分析与安全性研究[D].太原理工大学.2019
[3].邓炜.汉语比较关联句的形式化分析[D].上海外国语大学.2019
[4].尤江东.基于形式化分析法的情报应用模式研究[J].科技资讯.2019
[5].姚萌萌,朱正超,刘明达.一种改进的基于认证测试的形式化分析方法[J].信息网络安全.2019
[6].钟小妹,肖美华,李伟,谌佳,李娅楠.RFID超轻量级认证协议RCIA形式化分析与改进[J].计算机工程与科学.2018
[7].高强,林星辰,林宏刚,金大鹏.安全协议抗DoS攻击的形式化分析研究[J].四川大学学报(自然科学版).2018
[8].李伟.基于模型检测的超轻量级RFID双向认证协议形式化分析与验证[D].华东交通大学.2018
[9].李娅楠.基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析[D].华东交通大学.2018
[10].丁月,汪学明.一种新的复合型电子支付协议及其形式化分析[J].计算机应用与软件.2018