网络安全协议的高效分析系统

南昌大学硕士学位论文网络安全协议的高效分析系统姓名：吴昌申请学位级别：硕士专业：计算机软件与理论指导教师：肖美华20081225网络安全协议的高效分析系统作者：吴昌学位授予单位：南昌大学相似文献(10条)1.学位论文张爱新网络安全协议的分析与设计2002网络作为信息的一个重要载体,其安全性是整个信息基础架构的安全基础,而网络的安全性离不开安全的网络协议.因此,网络安全协议本身是否安全是信息安全的一个重要因素.作为信息安全的一项重要研究内容,网络安全协议的分析与设计具有极为重要的理论意义和实际价值.该文以网络安全协议的分析与设计为核心,就以下领域进行了研究:(1)网络安全协议的非形式化分析;(2)网络安全协议的形式化分析;(3)形式化方法在网络安全协议设计上的应用;(4)对复杂协议(如IKE、3GAKA)的分析与设计;(5)网络安全协议自动化分析与设计技术.2.会议论文肖美华.薛锦云基于模型检测技术的网络安全协议形式化分析研究2004形式化方法是提高软件系统，特别是safety-critical系统的安全性与可靠性的重要手段。模型检测是一种针对并发系统的自动分析与验证技术，以其简洁明了和自动化程度高而引人注目。密码协议目前已广泛应用于计算机网络与并发分布式系统中，但当密码协议并发执行时，其安全可靠性的论证仍是当前软件安全可靠性研究领域的一个世界难题。90年代以来，密码协议的形式化分析验证成为国际上的研究热点。本文提出了一种通用的安全协议模型及网络协议验证方法，出发点是将密码协议形式化，模型通用化，运用静态分析及惰性计算二种策略以解决状态爆炸问题。以TMN协议为例，通过SPIN/Promela具体在同一个模型下找出了针对其的五种攻击序列，并直观地通过信息序列图(Message　Sequence　Charts)具体地描述出其攻击轨迹。实验证明了此方法的有效性及通用性，可方便地用于其它网络安全协议验证。3.学位论文卓继亮网络安全协议安全性评测系统的研究与应用2004网络安全协议(或称密码协议)是网络安全体系中的关键环节,然而安全协议的设计却极易出错,攻击者常常可以绕开密码系统而通过安全协议来对系统发起攻击.随着网络应用的普及,对安全协议进行安全性评测已成为保障网络安全的一项重要任务.安全协议的安全性评测是指对协议的安全性进行分析、测试和评估,试图找出其中的安全缺陷,并做出相应的安全性评价结论.由于安全协议的缺陷往往非常隐蔽,一般分析方法通常难以发现;现在普遍认为,形式化方法是分析安全协议的最为可靠和有效的方法.以形式化方法为基础建立安全协议的自动分析工具(评测系统)成为当前的一个研究热点.该文以最近提出的一种原创性安全协议形式化分析理论——CPA理论为基础,成功研制了一个安全协议分析工具,并应用于安全协议的安全性评测中.该文主要贡献包括:1.设计并实现了一个安全协议评测系统——安全协议分析器SPA(SecurityProtocolAnalyzer),一方面验证了CPA理论,另一方面为实际安全协议评测提供了一个有效的辅助工具.2.将SPA系统应用于具体安全协议的安全性评测中,分析了一些常见安全协议的安全性,并发现一个未见公开的对BAN-Yahalom协议的攻击方法.这项工作加深了我们对安全协议缺陷和攻击的认识,并为设计新协议提供了许多借鉴.3.针对实用网络安全协议的特点和形式化分析方法(工具)的局限性,从安全协议攻击分类的角度对安全协议评测方法进行研究,给出一种基于攻击者能力和攻击后果的二维攻击分类方法,并在此基础上提出一种面向实用网络安全协议的分级评测思想.4.期刊论文冯珺珺.李光耀.江耘.FENGJun-jun.LIGuang-yao.JIANGYun基于迹语义的网络安全协议形式化分析-计算机与现代化2007,(2)形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段.本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约.运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证.5.学位论文丁一强认证协议的形式化分析方法研究1999该论文中,作者使用模型检查(modelchecking)方法来形式化地分析安全协议中认证协议的性质,目的是帮助协议设计和分析人员发现认证协议中隐藏的漏洞.6.期刊论文肖美华.熊昊.XIAOMei-hua.XIONGHao模型检测中反例最小化分析-南昌大学学报（工科版）2008,30(4)介绍了Gastin.P最小反例的算法思想,然后结合著名的Needham-Schroeder公钥身份认证协议进行了非形式化分析,实例分析的结果表明,算法用于分析网络安全协议的有效性.针对Gastin.P算法中存在对已遍历的状态重复遍历的缺点,结合语法重定序策略提出了一种新的算法框架,有效地解决了这个问题.因此,新的算法框架用于网络安全协议的分析具有高效性.7.学位论文肖美华网络安全协议形式化分析及支撑工具研究2007保护通信系统信息安全的核心技术包括密码系统和密码协议(也称安全协议)。系统的安全性不仅依赖于所采用的密码算法强度，而且与算法所使用的环境(安全协议)密切相关。密码系统相对比较成熟，攻击的代价是相当大的。相对密码系统而言，密码协议是比较脆弱的，很容易受到攻击。安全协议是通讯和网络安全体系、分布式系统和电子商务的关键组成部分，是安全系统的主要保障手段和工具。由于安全协议运行在复杂的分布式网络环境中，设计出的安全协议难免会存在安全漏洞，许多安全协议在使用多年后都被发现存在很严重的安全漏洞，例如著名的Needham-Schroeder公开密钥协议在公开17年后，它存在的入侵者攻击漏洞才被Lowe发现。如果使用存在漏洞的安全协议，势必会形成严重的安全威胁。因此，网络安全协议的研究具有很强的理论价值和现实应用背景。@@形式化方法是提高软件系统，特别是safety-critical系统的安全性与可靠性的重要手段。多年来人们采用的安全协议分析与验证方法主要是形式化方法，形式化方法主要有模型检测和定理证明。模型检测是一种重要的形式化自动验证技术，以其简洁明了和自动化程度高而倍受注目，模型检测使用状态空间搜索的办法自动地验证系统是否满足其设计规约，此技术的成功应用归功于有效验证工具的开发和支持。SPIN是一种著名的分析验证并发系统逻辑一致性的模型检测工具，2002年被ACM授予最具声望的“系统软件奖”(SystemSoftwareAward)。@@本文使用模型检测方法，基于算法知识逻辑形式化分析安全协议，在分析和比较常用安全协议形式化分析方法及对应支撑工具优劣的基础上，设计网络安全协议验证模型生成系统，目的是发现安全协议中隐藏的漏洞并对协议加以改进。研究成果表现为：@@1.形式化描述了安全协议的组成要素，包括消息、动作(迹)、消息状态及修改、协议运行及消息构造规则等，设计了协议描述语言PDL(ProtocolDescriptionLanguage)，PDL中初步体现了协议安全构建块(SecurityBuildingBlocks)抽象建模机制。@@2.提出了基于算法知识逻辑的网络安全协议模型检测分析方法，用于显式地刻画入侵者模型能力，从理论上分析了其知识完备性。@@3.开发了网络安全协议验证模型生成系统，能将安全协议的PDL描述自动转换为对应协议的Promela语言描述，调用SPIN模型检测器，自动找出攻击漏洞，当协议不满足安全性质时，可以用消息序列图MSC直观地列出攻击序列。@@4.在网络安全协议验证模型生成系统中采用了多项优化策略(包括偏序归约、语法重定序以及静态分析等)解决安全协议模型检测过程中状态爆炸问题(StateExplosion)，实验结果证实了系统采用这些优化策略的有效性及效率。@@5.认证协议的实例分析(Needham-Schroeder协议、TMN协议、BAN-Yahalom协议、Helsinki协议、密钥交换协议IKEv2等)，发现了这些协议已公布的安全漏洞。@@关键词：安全协议；形式化分析；模型检测；算法知识逻辑；偏序归约8.学位论文王芷玲网络安全协议形式化分析技术研究2006安全协议的安全性是网络安全的重要基础，运用形式化方法分析安全协议已成为目前研究的主要热点。本文主要研究运用形式化方法分析安全协议的理论与技术，对基于模型检测技术的运行模式分析法进行深入的研究，并把其扩展到公平交换协议的分析与设计中去。主要的研究成果如下：(1)介绍安全协议的背景及基本概念、研究进展和发展趋势，概述了安全协议的分类和安全协议的形式化分析方法的三种思路；(2)介绍两方和三方安全协议的运行模式分析法，设计并提出了两方乐观公平交换协议运行模式分析法；(3)使用运行模式分析法成功分析了几个电子商务协议，如SET协议、Micali的电子合同协议ECS1、FPH电子邮件协议，得到了较好的结论；(4)根据公平交换协议的特点，提出了公平交换协议的设计原则，并设计了一个安全的电子合同签署协议；9.期刊论文武智广.吕银华.翁惠玉.WUZhi-guang.LUYin-hua.WENGHui-yu基于环境敏感互模拟的Kerberos协议形式化分析-计算机仿真2007,24(2)进程演算通常用来研究交互式反应系统,其中的互模拟方法是用来形式化验证系统属性的重要途径.首先扩展了进程演算中的Spi演算,并将其应用于形式化描述网络安全协议--Kerberos协议的安全属性.为了验证该协议所声称的安全属性,引入了Spi演算中环境敏感互模拟的方法,即两个系统与环境发生交互过程中是否互模拟.通过采用该互模拟关系对Kerberos协议两个安全属性--可认证性和保密性--的证明,发现其可认证性是可靠的,而保密性存在一个可能的漏洞.最后,指出了基于互模拟的安全协议形式化验证方法今后值得进一步研究的方向.10.学位论文莫燕网络安全协议模型检测技术研究与应用2005安全协议的安全性是网络安全的重要基础,运用形式化方法分析安全协议的安全性已成为目前研究的主要热点.本文主要研究运用形式化技术分析安全协议的理论与技术,对基于模型检测技术的运行模式分析法进行深入的研究,并把其应用到实用安全协议的分析与设计中去.主要的研究成果如下:(1)对安全协议的背景及基本概念、安全协议的形式化分析方法的三种思路进行了系统的介绍;(2)介绍两方安全协议的运行模式分析法,对只包括一个可信第三方服务器的协议的运行模式分析法进行归纳,提出多于一个可信第三方服务器协议的运行模式分析法;(3)计算运行模式的数量上界,并给出有效的约束条件,构造与具体模型检测工具相独立的运行模式组合集,进一步提出了多方安全协议的运行模式分析法;(4)使用运行模式分析法成功分析了实用的安全协议,如SSL3.0、TMN、Kerberos等协议,得到了较好的结论;(5)根据协议的安全缺陷提出了安全协议的设计原则,并设计了一个安全的密钥建立协议;(6)总结模型检测法,并与其他经典形式化分析方法进行了详细的比较.本文链接：授权使用：上海海事大学(wflshyxy)，授权号：fb56b6c1-a4e2-4347-9d59-9e0800e742eb下载时间：2010年10月7日