基于模型检测工具SPIN的安全协议分析和验证

兰州大学硕士学位论文基于模型检测工具SPIN的安全协议分析和验证姓名：孙守卿申请学位级别：硕士专业：计算机软件与理论指导教师：李廉20060601基于模型检测工具SPIN的安全协议分析和验证作者：孙守卿学位授予单位：兰州大学相似文献(10条)1.学位论文任侠形式化方法在安全协议验证领域内的应用研究2003该文中,我们探讨了形式化方法在安全协议验证领域内的相关应用问题.其中,我们工作的重点将集中在Strand空间方法上.首先,我们介绍了安全协议描述方法发展的三个阶段,由此引出形式化方法应用于安全协议验证领域内的初衷.随后,我们分三条线索:Dolev-Yao模型及其影响、BAN逻辑与其后续工作,以及形式化方法的自动化技术,对形式化方法在安全协议验证领域内的发展动态进行了全面而客观的评述.第二,我们概述了该领域内三个最具影响力的形式化方法的应用过程,它们分别是Dolev-Yao模型、BAN逻辑,与Strand空间.为了进一步说明这些方法的实用性,我们还给出了相应的实例分析.第三,我们对近来颇受关注的Strand空间展开了一系列研究.这部分工作基于五个目标:其一、细化理想结构的描述方式;基二、形式化表述安全密钥的概念;其三、揭示安全密钥与协议秘密属性之间的关系;其四、给出安全密钥的相关性质;其五、提出一个证明安全协议的新思路.为实现这些目标,我们引入新的记号以表示理想的内部结构;利用理想的概念给出了安全密钥的形式化描述;在特定条件下,通过对比安全密钥与秘密属性各自的理想表达,证明了他们之间的等价关系;借助入侵者密钥的定义与入侵者行为对应的消息序列,证明了安全密钥特有的性质;最后,基于以上工作,我们提出一个基于安全密钥概念的协议证明思路.第四,我们基于Strand空间提出了一个新的针对安全协议缺陷的分类法.这个分类法将协议缺陷分为以下八类:当前性缺失缺陷、方向性缺失缺陷、类型缺失缺陷、独立性缺失缺陷、轮数标识缺失缺陷、认证过程缺失缺陷、认证测试形式相同缺陷,与认证测试部分形式相同缺陷.并且,对于前四类协议缺陷,我们利用认证测试方法完成了相应的协议分析工作.最后,我们介绍了形式化方法在安全协议设计领域内的应用现状,并且讨论了这个领域内今后的研究方向.2.期刊论文周世健.蒋睿.杨晓辉.ZhouShi-jian.JiangRui.YangXiao-hui安全协议DoS攻击的形式化分析方法研究-中国电子科学研究院学报2008,3(6)针对形式化方法对安全协议DoS攻击分析的不足之处,提出了一种基于串空间模型的扩展形式化方法.利用扩展后的形式化方法.对IEEE802.11i四步握手协议进行了DoS攻击分析,发现其的确存在DoS攻击漏洞.通过分析,提出一种可以改善DoS攻击的方法,并通过了扩展形式化方法对于判断安全协议DoS攻击分析的测试规则.最后,根据扩展形式化方法对改进后的四步握手协议进行证明,得出改进后协议可以通过两类DoS测试规则运行至结束.3.学位论文卓继亮网络安全协议安全性评测系统的研究与应用2004网络安全协议(或称密码协议)是网络安全体系中的关键环节,然而安全协议的设计却极易出错,攻击者常常可以绕开密码系统而通过安全协议来对系统发起攻击.随着网络应用的普及,对安全协议进行安全性评测已成为保障网络安全的一项重要任务.安全协议的安全性评测是指对协议的安全性进行分析、测试和评估,试图找出其中的安全缺陷,并做出相应的安全性评价结论.由于安全协议的缺陷往往非常隐蔽,一般分析方法通常难以发现;现在普遍认为,形式化方法是分析安全协议的最为可靠和有效的方法.以形式化方法为基础建立安全协议的自动分析工具(评测系统)成为当前的一个研究热点.该文以最近提出的一种原创性安全协议形式化分析理论——CPA理论为基础,成功研制了一个安全协议分析工具,并应用于安全协议的安全性评测中.该文主要贡献包括:1.设计并实现了一个安全协议评测系统——安全协议分析器SPA(SecurityProtocolAnalyzer),一方面验证了CPA理论,另一方面为实际安全协议评测提供了一个有效的辅助工具.2.将SPA系统应用于具体安全协议的安全性评测中,分析了一些常见安全协议的安全性,并发现一个未见公开的对BAN-Yahalom协议的攻击方法.这项工作加深了我们对安全协议缺陷和攻击的认识,并为设计新协议提供了许多借鉴.3.针对实用网络安全协议的特点和形式化分析方法(工具)的局限性,从安全协议攻击分类的角度对安全协议评测方法进行研究,给出一种基于攻击者能力和攻击后果的二维攻击分类方法,并在此基础上提出一种面向实用网络安全协议的分级评测思想.4.期刊论文常亮.古天龙.CHANGLiang.GUTian-long安全协议及其形式化分析研究-桂林电子工业学院学报2006,26(4)安全协议是网络安全的重要基础,形式化分析是保证安全协议具备相应安全性质的有效途径.通过对安全协议进行分类,阐述了各类协议所应具备的安全性质;并基于安全协议进行形式化分析时所作的各种假设,综述和分析了三类典型的安全协议形式化方法,给出了安全协议形式化分析研究的发展趋势.5.学位论文刘学锋安全协议形式化分析及其应用2004协议是在计算机网络和分布系统中两个或多个主体(Principals)为相互交换信息而规定的一组信息交换规则和约定.安全协议也称作密码协议,是在协议中应用加密解密的手段隐藏或获取信息,以达到安全性的各种目的.对于安全协议的形式化研究始于20世纪70年代末,现在,安全协议的形式化研究成为一个热点领域,有众多的形式化和逻辑的研究方法涌现出来.串空间(strandspace)模型是出现在上世纪末的一种新型的安全协议的形式化方法,它是一种能结合定理证明和模型检测的混合形式化方法.事实证明,串空间模型是分析安全协议的一种实用、直观和严格的形式化方法.基于此模型开发的自动验证工具ATHENA已经实现了对协议的认证性特性验证,但未能克服模型检测方法所造成的状态空间严重爆炸的问题,对秘密性协议的证明也是不完善的.我们结合使用定理证明和模型检测技术,开发了安全协议验证工具AVSP,其中核心算法AVSP首次使用了理想的概念来定义协议的秘密性,并对秘密性安全属性进行验证.我们还提出一些剪枝规则对状态搜索空间进行剪枝,在我们试验中得到的对于Needham-Schroeder安全协议的弱一致性认证属性验证过程中充分说明这些状态搜索空间剪枝规则的应用,该结果清楚地表明所有的空间剪枝规则可有效缩小状态搜索空间,防止状态空间爆炸.实验结果分析表明AVSP是正确的和高效的.6.期刊论文吴立军.苏开乐安全协议认证的形式化方法研究-计算机工程与应用2004,40(17)安全协议认证是网络安全领域中重大课题之一.形式化方法多种多样.该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向.7.学位论文华东明安全协议的形式化方法及其应用的研究2005网络可以使人们在任意地点和任意时间、以任意方式访问共享网络资源，同时随着网络的迅猛发展和应用领域的不断扩大，网络面临着越来越多的安全威胁，为了保证网络的安全运行和资源的有效利用，作为网络安全服务基础的安全协议越来越受到重视，但由于安全协议本身的复杂性、相关理论和工程技术的不成熟以及人们认识能力的局限性，使得在现有安全协议中不可避免地存在着安全缺陷。为了设计出更可靠的安全协议，形式化方法成为描述、设计和分析安全协议的有效工具，并得到相当深入的研究、并获到比较广泛和成功的运用。目前，在无线局域网的安全协议中不同程度地存在着安全缺陷，其中在802.11中的安全机制存在着致命的安全漏洞。近几年来，为了基于可信平台特性建立未来具有高安全性的计算机系统，可信计算组提出了在计算机的硬件平台上引入安全芯片架构和通过提供硬件的安全特性来提高系统安全性的安全体系结构。本论文深入研究了安全协议面向主体的形式描述、设计和分析，并运用本论文中提出的安全协议面向主体的形式描述、设计和分析方法，分别研究了无线局域网中WAPI的认证和密钥协商协议以及可信计算中的OIAP协议。本论文的贡献表现在：(1)在安全协议面向主体的逻辑描述语言的研究中，将主体遵从安全协议相互通信的过程看成主体通过通信行为传递拥有、知识和信念以及主体的拥有、知识和信念随时序单调增加的过程；基于拥有、知识、信念、发送、接收和时序建立了描述安全协议的形式语言；给出它的Kripke语义模型和真值语义解释；在安全协议元素的形式化描述中，运用面向主体的方法描述了参与安全协议运行的主体的特性及其角色，比较清晰、准确和全面地描述了安全协议中消息的可辨认性和新鲜性、密钥的特性以及认证与密钥分发的目的，根据提供的不同安全服务，将安全协议中的密码机制抽象为不同信道：运用该形式语言以面向主体的方法对Needham-Schroeder对称密钥协议进行了形式化描述；将该语言与CKT5对安全协议逻辑描述的表达能力进行了比较。(2)在安全协议面向主体的设计逻辑的研究中，创建了基于面向主体以及知识和信念逻辑的安全协议设计逻辑，给出了关于知识和信念、安全主体、权威主体、发送、接收、拥有、消息的可辨认性、消息的新鲜性、消息源和主体身份认证、密钥验证和密钥协商的公理，给出了三段论推理规则；根据提供的不同安全服务，将安全协议中的密码机制抽象为不同信道，形式化地描述了细化规则、合成规则、转发规则、规范消息规则、关联规则、全信息规则和优化消息规则7个安全协议设计规则；将安全协议的设计分为安全协议目的的确定、分析主体的角色及其特性、密码机制的确定、安全协议目的的细化、分析安全协议设计的初始假设、运用规范消息、关联和全信息规则设计单个消息、根据优化消息优化安全协议7个步骤；根据给出的设计逻辑、设计规则和设计步骤形式化和系统化地设计了一个基于对称密钥机制的安全协议和一个基于挑战／响应机制进行相互身份认证和Diffie-Itellman密钥协商机制的安全协议；将该设计逻辑与BSW逻辑进行了比较。(3)在安全协议面向主体的分析逻辑的研究中，构建了面向主体的安全协议分析逻辑，将拥有、信念和知识融合起来更真实地模拟主体在协议运行中的状态，给出基于秘密和公开密钥密码系统的公理集，给出了三段论、必然律和理性推理规则；由主体的拥有集、信念集、知识集和通信行为构造安全协议的计算模型，给出该分析逻辑中形式语言的真值语义解释，证明了该分析逻辑的可靠性；给出安全协议的分析步骤，通过对Needll锄-Schroeder协议的分析检验了新的分析逻辑的推理能力，并与BAN和GNY逻辑对该协议的分析结论进行了比较，得出本逻辑比它们有着更强的推理能力的结论。(4)在国家标准．无线局域网认证和保密基础设施(WAPI)的研究中，描述了WLAN中安全协议的特性，分析了它们中存在的安全缺陷，对WAPI和802.11i进行了比较，运用本论文提出的安全协议分析逻辑对WAI协议进行了形式化分析和改进分析。(5)在可信计算的研究中，描述了可信平台的特性和OLAP的会话过程，运用本论文提出的安全协议分析逻辑对OIAP进行了形式化分析和改进分析。8.期刊论文韩进.蔡圣闻.王崇峻.赖海光.谢俊元一种基于πt演算的安全协议建模方法-计算机研究与发展2010,47(4)安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支