导读:本文包含了安全协议自动化验证论文开题报告文献综述及选题提纲参考文献，主要关键词:安全协议代码,形式化分析,模型抽取,认证性
安全协议自动化验证论文文献综述
陈伟[1]（2014）在《基于计算模型自动化验证安全协议Java代码认证性》一文中研究指出随着信息时代的发展，人们越来越关注隐私数据的保护，信息安全问题变得越来越突出。安全协议作为网络通信中保证数据安全传输的基石，其安全性与有效性成为大众关注的热点，也是安全协议研究者的研究重点。形式化方法是分析与验证安全协议的重要技术，主要包括：形式化安全协议，建立安全协议抽象模型，应用自动化分析工具验证协议的安全属性。安全协议形式化分析取得了丰硕成果，已提出了多个安全模型及发布了多种自动化分析工具。尽管安全协议的形式化分析技术能够证明安全协议的安全属性，但分析主要是建立在协议的抽象模型上，实用性差。实践表明，已被正确证明的安全协议在编码实现时会引入新的安全问题，因此分析安全协议代码的密码学安全属性不可避免。目前对安全协议代码的研究较少，模型抽取和代码生成是其中的主要技术。本文基于模型抽取技术，对安全协议的Java源码进行分析，抽取出其安全模型，并形式化为Blanchet演算代码。使用基于计算方法的自动化证明工具CryptoVerif证明该源码的认证性。主要工作如下：(1)描述了安全协议的形式化技术和安全协议代码形式化技术。重点介绍计算方法的相关理论和模型抽取技术。(2)分析安全协议的Java实现和Java的语法规范，建立安全协议实现的Java语法子集SubJ。介绍了基于计算方法的形式化语言Blanchet演算，定义SubJ与Blanchet演算间的语法映射关系。(3)基于模型抽取技术，开发模型抽取工具SubJ2CV。该工具主要对协议的ubJ代码首先进行词法分析、语法分析和生成抽象语法树，之后化简抽象语法树，抽取出安全模型。将其转换为Blanchet演算的抽象语法树，最后生成Blanchet演算代码。(4)使用SubJ2CV抽取一个认证协议Java实现代码的安全模型，将其转换为Blanchet演算代码，应用自动化分析工具CryptoVerif分析安全属性，证明协议代码的认证性。(本文来源于《中南民族大学》期刊2014-04-15）
刘燕玲[2]（2011）在《基于串空间模型的安全协议自动化验证方法研究》一文中研究指出随着网络技术和信息技术的迅速发展,计算机网络在诸多领域内的应用日益普及,然而由于其运行环境具有开放性,使得计算机网络在给人们带来巨大便利的同时,也产生一系列的安全问题,因此如何确保网络中信息的安全性成为亟待解决的问题。安全协议又称密码协议,是以密码学技术为基础,在不安全的公共网络和分布式系统中提供各种安全服务的一种通信协议。由于安全协议的安全性是评价网络好坏的一个重要指标,所以在安全协议投入使用之前,对其安全性分析就显得尤为重要。至今,安全协议的形式化分析和自动化检测己成为分析和研究安全协议领域的两个重要方向,而研制可靠实用的安全协议自动化分析工具也逐渐成为主流趋势。本文以串空间理论为基础,通过对当前存在的一些安全协议形式化方法和自动化技术进行比较分析,深入地研究了安全协议的自动化分析方法。主要内容包括：1)深入研究了安全协议的安全性质,针对当前运用比较广泛的形式化分析方法——串空间模型,通过研究构造方法,重点介绍了NSL协议的分析过程；同时,以SSM协议为例,探讨了如何使用认证测试验证协议的过程及设计原理。2)给出了一种基于串空间模型的安全协议自动化验证方法。在该方法中,针对参与方不检测某些消息的来源,只是将其作为消息的子项参与协议的运行的问题,通过构造和合法串结构相同的攻击者串的方式,给出了一种自动化验证方法；它不仅能够分析具有加密类型的攻击缺陷的协议,还将可信方引入到协议的参与方,使之能够分析具有重放类型攻击缺陷的协议,整个过程无需人工干预,直观和高效。在文章的最后借助两个实例,详细说明了该系统的验证过程,结果表明系统具有良好的性能。(本文来源于《郑州大学》期刊2011-05-01）
张孝红,李谢华[3]（2011）在《基于串空间的安全协议自动化验证算法》一文中研究指出以串空间模型为理论基础,提出安全协议自动化验证算法IVAP。对于有漏洞的协议,针对不安全属性逆向搜索主体串树,自动生成改进协议并对其进行验证,直至生成一个安全的改进协议。实验结果证明了该自动化验证算法的有效性,与AAAP算法相比,其协议验证效率更高。(本文来源于《计算机工程》期刊2011年05期）
张孝红[4]（2010）在《基于形式化方法的安全协议自动化验证算法的研究》一文中研究指出作为网络通信的安全保障,安全协议是整个信息系统架构的安全基础。为了保证安全协议的正确性,研究人员提出了一系列基于形式化方法的自动化验证算法来对安全协议进行分析验证,并已经成功地发现很多安全协议中存在的漏洞和攻击,但这些算法只能指出协议中的漏洞和攻击,不能自动生成改进协议,而且这些算法还存在验证效率低、使用难度大的问题。鉴于此,本文以串空间模型和认证测试方法为理论基础,对以上问题进行深入研究,研究内容主要包括以下几个方面：首先,在深入研究形式化方法的基础上,详细分析了几种应用较为广泛的自动化验证算法,并针对现有算法的不足,提出了IVAP算法(Intelligent Validator for Authentication Protocols)。IVAP算法不仅能自动地完成协议的验证,而且还能根据不安全属性逆向搜索主体串树,自动生成改进协议并继续完成改进协议的验证。然后,详细设计并开发了基于IVAP算法的安全协议自动化验证原型系统,原型系统采用B/S架构,由安全协议图形转换接口模块、安全协议形式化描述接口模块、安全协议验证模块和改进协议生成模块四个功能模块组成。最后,用原型系统对一系列经典认证协议进行了实验验证,分析了在协议验证过程中所需的时间复杂度和空间复杂度,并把实验数据与其它同类算法作了详尽的比较分析。通过实验结果表明了IVAP算法的有效性和高效性。本文的创新工作有以下两点：1.提出了基于串空间的IVAP算法,在协议验证过程中,若发现协议有安全漏洞,则自动生成改进协议,在理论的应用上具有创新性；2.开发了基于IVAP算法的安全协议自动化验证原型系统,通过实验分析结果表明,跟其它同类系统相比效率更高,在理论的应用上具有创新性。(本文来源于《湖南大学》期刊2010-05-10）
吴燕[5]（2006）在《基于术语猜测及Hash伪造的安全协议自动化验证》一文中研究指出安全协议为网络信息交换提供安全服务,是保证网络安全的基础。但攻击者可利用安全协议自身的缺陷来实施各种各样的攻击,因此安全协议的安全性成为网络安全的关键。早期人工证明的协议分析方式极易出错,其检测的范围也过于狭窄。由于安全协议目标的微妙性、协议运行环境的复杂性、攻击的多样性以及协议运行的高并发性,迫切需要研究和设计更可靠的安全协议形式化分析方法。本文提出一种新的安全协议的形式化验证逻辑,在协议分析的两个重要方面——协议的形式化和攻击模型的设计都作出了改进。该形式化方法有效克服了基于信仰的逻辑证明方法的不足,不仅可找到攻击,也可证明协议的安全性。本文还提出一种扩充的入侵模型,模型中应用了术语猜测和Hash碰撞理论。其中术语猜测是近年来协议分析的研究新热点。Hash碰撞是密码学方面的最新重大突破,据此本文首次提出Hash伪造攻击。基于这种扩充,本文的方法找到了更多新的协议攻击。在此基础上,本文针对如何有效避免这些新型攻击给出协议修改建议。同时本文分析了两种重要协议——电子商务协议和安全套接层协议的安全性。最后本文实现了基于本文验证逻辑和入侵模型的协议自动化分析系统,设计了用于实现自动化分析的协议说明语言,首次提出将协议说明语言分层实现的设计思想。与已有的自动化分析工具相比,该系统可分析的协议类型更广泛,得出的攻击更全面,并且对协议安全性的证明更可信。根据作者检索结果,目前尚无其他自动化工具发现Woo-LamΠ4的猜测攻击和MS-CHAPv2的Hash伪造攻击。本文的研究对安全协议的验证和设计乃至电子商务、军事、无线通信等网络安全研究具有一定参考价值。(本文来源于《南京航空航天大学》期刊2006-12-01）
安全协议自动化验证论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
随着网络技术和信息技术的迅速发展,计算机网络在诸多领域内的应用日益普及,然而由于其运行环境具有开放性,使得计算机网络在给人们带来巨大便利的同时,也产生一系列的安全问题,因此如何确保网络中信息的安全性成为亟待解决的问题。安全协议又称密码协议,是以密码学技术为基础,在不安全的公共网络和分布式系统中提供各种安全服务的一种通信协议。由于安全协议的安全性是评价网络好坏的一个重要指标,所以在安全协议投入使用之前,对其安全性分析就显得尤为重要。至今,安全协议的形式化分析和自动化检测己成为分析和研究安全协议领域的两个重要方向,而研制可靠实用的安全协议自动化分析工具也逐渐成为主流趋势。本文以串空间理论为基础,通过对当前存在的一些安全协议形式化方法和自动化技术进行比较分析,深入地研究了安全协议的自动化分析方法。主要内容包括：1)深入研究了安全协议的安全性质,针对当前运用比较广泛的形式化分析方法——串空间模型,通过研究构造方法,重点介绍了NSL协议的分析过程；同时,以SSM协议为例,探讨了如何使用认证测试验证协议的过程及设计原理。2)给出了一种基于串空间模型的安全协议自动化验证方法。在该方法中,针对参与方不检测某些消息的来源,只是将其作为消息的子项参与协议的运行的问题,通过构造和合法串结构相同的攻击者串的方式,给出了一种自动化验证方法；它不仅能够分析具有加密类型的攻击缺陷的协议,还将可信方引入到协议的参与方,使之能够分析具有重放类型攻击缺陷的协议,整个过程无需人工干预,直观和高效。在文章的最后借助两个实例,详细说明了该系统的验证过程,结果表明系统具有良好的性能。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
安全协议自动化验证论文参考文献
[1].陈伟.基于计算模型自动化验证安全协议Java代码认证性[D].中南民族大学.2014
[2].刘燕玲.基于串空间模型的安全协议自动化验证方法研究[D].郑州大学.2011
[3].张孝红,李谢华.基于串空间的安全协议自动化验证算法[J].计算机工程.2011
[4].张孝红.基于形式化方法的安全协议自动化验证算法的研究[D].湖南大学.2010
[5].吴燕.基于术语猜测及Hash伪造的安全协议自动化验证[D].南京航空航天大学.2006