基于串空间模型的安全协议验证及算法研究
这是一篇关于安全协议,串空间模型,理想,认证测试,状态空间简化的论文, 主要内容为伴随着计算机网络的普及和电子商务新政务的发展，信息安全问题变得越来越关键。要保证信息的安全性，仅仅依赖良好的加密算法是不够的，在实际应用中，还需要有可信的机制为各个独立的通信实体分发密钥，并且在通信实体间进行身份认证，这就使人们研究出各种安全协议。 安全协议，是使用了密码学方法的网络通信协议，其目的就是为了在复杂的、不安全的网络环境中提供各种安全服务。安全协议的目的是保证信息的安全，但是如果安全协议本身存在漏洞，攻击者就会利用这些漏洞，对合法通信者造成危害。因此需要对安全协议进行分析和验证，来验证安全协议是否能够达到其预期的安全目标。 Strand Space模型是由Fábrega，Herzog和Guttman三人提出的一种形式化方法，该模型的提出为解决安全协议设计与分析的困难提供了一种可能，它是现有的安全协议形式化分析方法中最为直观、简洁、严格和有效的方法。本文在深入研究串空间理论的基础上，做了以下几个方面的工作： 1)深入了解了安全协议的安全性质，尤其是机密性与认证性，熟悉串空间理论模型及其协议验证方法； 2)运用串空间模型分析了MY-Helsinki协议，证明了其在机密性与认证性方面的正确性，并分析了该协议在改进前存在缺陷的原因； 3)分析研究了理想和认证测试在安全协议分析中的应用，分别运用理想和认证测试方法对Weakened-Yahalom协议的认证性进行了分析，并对二者进行了比较； 4)分析并修改了动态串空间模型算法，总结了已有的状态空间简化规则，在认证测试理论基础上提出一个新的剪枝定理，修改了其结点绑定算法并增加了丛扩展规则。将剪枝定理应用于协议认证性质分析中，减少了协议分析的工作量，提高了协议分析效率；丛扩展规则的增加使得算法能够适用于包括发起者、响应者和服务器的三方协议。最后通过两个实例分别说明算法修改的有效性。
基于串空间模型的安全协议自动化验证方法研究
这是一篇关于安全协议,形式化分析,串空间模型,认证测试的论文, 主要内容为随着网络技术和信息技术的迅速发展,计算机网络在诸多领域内的应用日益普及,然而由于其运行环境具有开放性,使得计算机网络在给人们带来巨大便利的同时,也产生一系列的安全问题,因此如何确保网络中信息的安全性成为亟待解决的问题。安全协议又称密码协议,是以密码学技术为基础,在不安全的公共网络和分布式系统中提供各种安全服务的一种通信协议。由于安全协议的安全性是评价网络好坏的一个重要指标,所以在安全协议投入使用之前,对其安全性分析就显得尤为重要。至今,安全协议的形式化分析和自动化检测己成为分析和研究安全协议领域的两个重要方向,而研制可靠实用的安全协议自动化分析工具也逐渐成为主流趋势。 本文以串空间理论为基础,通过对当前存在的一些安全协议形式化方法和自动化技术进行比较分析,深入地研究了安全协议的自动化分析方法。主要内容包括： 1)深入研究了安全协议的安全性质,针对当前运用比较广泛的形式化分析方法——串空间模型,通过研究构造方法,重点介绍了NSL协议的分析过程；同时,以SSM协议为例,探讨了如何使用认证测试验证协议的过程及设计原理。 2)给出了一种基于串空间模型的安全协议自动化验证方法。在该方法中,针对参与方不检测某些消息的来源,只是将其作为消息的子项参与协议的运行的问题,通过构造和合法串结构相同的攻击者串的方式,给出了一种自动化验证方法；它不仅能够分析具有加密类型的攻击缺陷的协议,还将可信方引入到协议的参与方,使之能够分析具有重放类型攻击缺陷的协议,整个过程无需人工干预,直观和高效。在文章的最后借助两个实例,详细说明了该系统的验证过程,结果表明系统具有良好的性能。
微服务框架下数据共享技术研究和实现
这是一篇关于微服务,数据共享,安全协议,Spring Cloud的论文, 主要内容为近年来,信息数字化呈现出不可避免的趋势,几何式爆发增长的数据中蕴含着巨大的价值,因此,数据的共享显得尤为重要。最初,为了加快信息化建设,开发者采用传统面向服务的单体架构完成海量数据交换共享,然而,随着业务的不断增加,数据规模的不断增大,单体架构在数据共享中的可扩展性和性能稳定性明显不足,同时,现有数据共享平台的数据滥用和隐私泄露问题,导致数据共享缺乏必要的安全保障。针对上述问题,本文选用Spring Cloud技术框架,运用其分而治之的思想以及扩展灵活、耦合度低的优势,设计并实现了保障分布式隐私安全的基于微服务的数据共享框架。该框架针对数据共享痛点,在数据共享统一性、灵活性和安全性方面做出尝试,旨在提高数据的开放性和综合利用率。论文的主要工作如下:(1)对数据共享特点以及现有的数据共享模式进行综合分析,找出其中影响更好发挥数据共享功能的因素,总结实现数据共享安全所面临的挑战,探究解决方案。(2)针对共享框架分布式特性,设计了保障数据共享安全的协议,协议结合了安全多方计算的思想,以分布的共享数据服务作为多方参与者,改进了秘密共享使用场景与方式,为其添加信任度机制并制定算法参数标准,实现参数动态更新,保证了数据隐私性和密钥私密性。(3)在需求分析的基础上,完成了数据共享框架的设计与实现。宏观上将框架分为认证系统、数据系统和加密系统,为其设计数据共享规范,简化了数据使用流程。此外,框架结合安全协议,构建了基于Elastic Search的搜索引擎微服务,为该服务开发了数据操作模块、数据限流模块、数据同步模块以及数据匿名模块,配合加入框架的共享数据服务,对数据进行集中管理。实际运行效果显示,共享框架在提高数据的共享效率的同时保障了框架数据共享的安全进行,充分挖掘了数据价值。
基于着色Petri网的安全协议自动化分析系统的设计与实现
这是一篇关于着色Petri网,安全协议,自动化建模,形式化分析的论文, 主要内容为安全协议也被称之为密码学协议,它的目标是通过应用密码学基件在不安全的网络环境中提供安全的通信服务。安全协议的海量、复杂、易错等特点,导致协议安全性自动化分析的需求与日俱增。CPN Tools(Colored Petri Net,CPN)是一种基于模型检测的协议自动化分析工具,作为模型检测的代表性方法之一,因具备并发分布式系统建模的能力且集成了大量强有力的自动化计算工具,在协议自动化分析领域具有很好的发展前景。但在安全协议分析领域,由于CPN Tools缺乏对敌手状态的有效建模,在利用CPN Tools进行安全协议分析时,针对不同安全协议需要手动构建敌手模型,这一过程会导致协议分析的自动化程度大幅下降,且极易引入安全风险。本文以CPN模型为基础、以协议安全性自动化分析为核心,构建了基于着色Petri网的安全协议自动化建模与分析系统,解决了已有方案需手动构建CPN敌手模型和协议模型的问题,极大提高了系统的自动化程度。该系统基于CPN建模规范自定义一套新的安全协议描述规范,并通过分析CPN模型的XML文件结构,设计了一种CPN基本对象的自动化生成工具,实现了在CPN Tools环境下安全协议分析模型的自动化生成模块和协议文本描述的自动化解析。在此基础上,系统提供一种基于ML语言的协议安全评估规则描述方法,该方法可以精确定位CPN模型状态空间衍生范围,并依据安全评估规则快速检索不安全状态节点,以提取安全协议攻击路径。综上,通过引入上述自动化工具,该系统精简了基于CPN模型的协议安全性分析流程,极大地降低了应用过程中的协议安全性分析门槛。最后,以经典的Andrew Secure RPC协议为实证应用,验证了本文设计的基于着色Petri网的安全协议自动化建模与分析系统的性能和可用性。首先,通过自定义协议描述规范对协议4条会话消息进行文本描述;然后,基于自动化建模工具生成协议安全性分析CPN模型,通过与手动建模在各项条目上的对比,验证了自动化建模工具的自动化性能;最后,通过分析协议需要满足的2项安全要求得出协议安全性分析的3项评估规则,以其中1项评估规则为例,得出依据该评估规则的协议安全性分析结果,通过与现有文献中的安全性分析结果相比,表明了本文所设计的系统具有较强的可行性和有效性。
基于串空间模型分析与验证密码安全协议
这是一篇关于安全协议,形式化方法,串空间模型,理想,秘密性:AVSP的论文, 主要内容为随着网络的普及以及电子商务和电子政务蓬勃兴起，安全协议变得越来越重要，确保安全协议的安全性已经成为一项重要的研究课题。安全协议分析是一个很难解决的问题，20年来为了应对这一挑战，科学家们投入了大量的精力。在已有的理论和方法中，形式化分析方法的成果比较突出，其发展前景被专家们普遍看好，本文第二章对此进行了综述。 串空间(STRAND SPACE)模型由F’abrega、Herzog和Guttman三人提出，它是分析安全协议的一种实用、直观和严格的形式化方法，它充分吸收了前人的研究成果，模型使用一种节点间存在因果关系的有向图来表示协议的运行。D.Song对串空间模型进行了扩展，并开发了安全协议自动验证工具ATHENA。 在深入研究串空间理论的基础上，本文从理论和算法两个方面对串空间模型进行了扩展和完善。在理论上，本文引入了理想的语义，并首次使用了理想的概念对安全协议的秘密性进行严格的定义，同时使用理想的命题逻辑公式表示安全协议的秘密性；另外，本文修正了F’abrega、Herzog和Guttman三人文献中的一个引理的证明，原有的证明是不完善的。在算法上，本文增设了一条状态删减规则，并进行了严格的证明；另外，对模型检测算法进行了修改，使得算法可以找出协议在限定搜索深度下所有攻击反例。我们使用JAVA语言对本文的模型检测算法进行了具体实现，开发了一个拥有自主知识产权的安全协议自动验证工具AVSP。对已经进行的实验结果分析表明，本文对串空间模型的扩展是正确的和有效的；另外，利用AVSP我们发现了Woo-Lam4认证协议的一个新的在现有的文献中没有公布的攻击。
本文内容包括但不限于文字、数据、图表及超链接等）均来源于该信息及资料的相关主题。发布者：代码驿站 ，原文地址：https://bishedaima.com/lunwen/48522.html
