5个研究背景和意义示例,教你写计算机形式化分析论文

今天分享的是关于形式化分析的5篇计算机毕业论文范文, 如果你的论文涉及到形式化分析等主题,本文能够帮助到你

基于串空间模型的安全协议自动化验证方法研究

这是一篇关于安全协议,形式化分析,串空间模型,认证测试的论文, 主要内容为随着网络技术和信息技术的迅速发展,计算机网络在诸多领域内的应用日益普及,然而由于其运行环境具有开放性,使得计算机网络在给人们带来巨大便利的同时,也产生一系列的安全问题,因此如何确保网络中信息的安全性成为亟待解决的问题。安全协议又称密码协议,是以密码学技术为基础,在不安全的公共网络和分布式系统中提供各种安全服务的一种通信协议。由于安全协议的安全性是评价网络好坏的一个重要指标,所以在安全协议投入使用之前,对其安全性分析就显得尤为重要。至今,安全协议的形式化分析和自动化检测己成为分析和研究安全协议领域的两个重要方向,而研制可靠实用的安全协议自动化分析工具也逐渐成为主流趋势。本文以串空间理论为基础,通过对当前存在的一些安全协议形式化方法和自动化技术进行比较分析,深入地研究了安全协议的自动化分析方法。主要内容包括： 1)深入研究了安全协议的安全性质,针对当前运用比较广泛的形式化分析方法——串空间模型,通过研究构造方法,重点介绍了NSL协议的分析过程；同时,以SSM协议为例,探讨了如何使用认证测试验证协议的过程及设计原理。 2)给出了一种基于串空间模型的安全协议自动化验证方法。在该方法中,针对参与方不检测某些消息的来源,只是将其作为消息的子项参与协议的运行的问题,通过构造和合法串结构相同的攻击者串的方式,给出了一种自动化验证方法；它不仅能够分析具有加密类型的攻击缺陷的协议,还将可信方引入到协议的参与方,使之能够分析具有重放类型攻击缺陷的协议,整个过程无需人工干预,直观和高效。在文章的最后借助两个实例,详细说明了该系统的验证过程,结果表明系统具有良好的性能。

基于串空间模型的认证协议分析方法研究

这是一篇关于串空间模型,形式化分析,认证协议,重复认证协议的论文, 主要内容为计算机网络的高速发展和网络新应用的不断涌现给网络安全带来了很大的冲击,网络安全成为新的信息安全的热点;安全协议作为计算机网络安全体系的重要组成部分,也就变得越来越重要。然而,由于安全协议的复杂性,设计一个完美的安全协议是十分困难的,许多公开发表的安全协议中后来被发现它们存在各种各样的安全漏洞。因此,以确保安全协议正确性为目的的安全协议分析成为一项重要的研究课题。安全协议分析方法可分为形式化分析方法和非形式化分析方法,其中,形式化分析方法是安全协议理论研究的热点之一。常见的形式化分析方法有BAN逻辑,Kailar逻辑,SPI演算,CSP方法,串空间模型等。串空间模型理论是安全协议分析领域最新的研究成果,它是在1998年由Thayer, Herzog和Guttman提出的,具有高效、直观、实用等特点,不仅可以用于证明安全协议的正确性,还可以用于构造攻击,揭示安全协议的内在缺陷。该方法已经成功地分析了Needham-Schroeder-Lowe协议,Otway-Rees协议,Yahalom协议等诸多协议,被公认为是一种先进的高效的协议分析方法。本文简要介绍了串空间模型的符号系统及其基本概念和理论,分析了基于串空间模型的极小元、理想与诚实、认证测试方法这三个分支的原理和应用场合,并体现了串空间模型的特点及优势。首先,本文以在无线局域网中广泛使用的IEEE 802.11i认证协议为例,用串空间模型中的相关符号和丛图对协议进行建模,并在此基础上用理想与诚实方法去证明协议的保密性和认证性。其次,对运用串空间模型理论分析重复认证协议进行研究,发现以往的运用串空间模型理论分析重复认证协议,都是把重复认证协议的不同子协议看成是独立的。为了解决这个问题,本文扩展串空间模型理论。在不同的子协议之间引入了一种新的因果关系,并重新定义了串空间与丛的定义,提出重复认证协议的两个属性,即重复认证一致性与重复认证保密性。最后,以Kao Chow重复认证协议为例。应用扩展后的串空间模型,对Kao Chow协议进行建模,并在此基础上用理想和诚实方法去证明协议的保密性和认证性。

基于串空间模型的协议分析方法研究

这是一篇关于串空间,认证协议,不可否认协议,形式化分析的论文, 主要内容为计算机网络的高速发展和网络新应用的不断涌现给网络安全带来了很大的冲击,网络安全成为新的信息安全的热点;安全协议作为计算机网络安全体系的重要组成部分,也就变得越来越重要。然而,由于安全协议的复杂性,设计一个完美的安全协议是十分困难的,许多公开发表的安全协议中后来被发现它们存在各种各样的安全漏洞。因此,以确保安全协议正确性为目的的安全协议分析成为一项重要的研究课题。安全协议分析可分为形式化分析和非形式化分析,其中,形式化分析方法是安全协议理论研究的热点之一。常见的形式化分析方法有BAN逻辑,Kailar逻辑,SPI演算,CSP方法,串空间模型等。串空间模型理论是安全协议分析领域最新的研究成果,它是在1998年由Thayer, Herzog和Guttman提出的,具有高效、直观、实用等特点,不仅可以用于证明安全协议的正确性,还可以用于构造攻击,揭示安全协议的内在缺陷。该方法已经成功地分析了Needham-Schroeder-Lowe协议,Otway-Rees协议,Yahalom协议等诸多协议,被公认为是一种先进的高效的协议分析方法。本文以串空间理论作为研究基础,主要进行了以下研究: (1)深入研究串空间模型的基础理论,应用串空间模型分析了Natalia Miloslavskaya等人提出的一个双向认证协议,发现该协议在认证方面存在缺陷,并对该协议进行了改进。 (2)对运用串空间理论分析不可否认协议进行研究,发现了以往运用串空间理论分析协议公平性的两个问题,并给出了解决方法。随后对不可否认协议中弹性信道、同步消息等特定假设条件,采用串空间理论的方式进行形式化描述及推理,从而为串空间理论分析不可否认协议扫除了障碍。然后以一个实例来说明如何运用串空间理论证明不可否认协议的公平性,其中,关键之处是如何构造正确的命题。 (3)分析TEENP不可否认协议,发现它的安全缺陷,在此基础上提出了一个新的不可否认协议。同时,对另外两个不可否认协议进行分析,发现以往文献中未提及的新的漏洞。 (4)此外,还对不可否认协议中的公平性,异常数据处理等问题提出了自己的一些想法。

基于着色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项评估规则为例,得出依据该评估规则的协议安全性分析结果,通过与现有文献中的安全性分析结果相比,表明了本文所设计的系统具有较强的可行性和有效性。