基于串空间模型的安全协议形式化分析方法研究

来源 :全国网络与信息安全技术研讨会2004 | 被引量 : 0次 | 上传用户:robert_xt
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
用于安全协议形式化分析的串空间(strand space)模型,是一种结合定理证明和协议迹的混合方法,可以有效地描述和证明安全协议的正确性.本文对串空间模型近年来在扩展性、与其它形式化方法的关系、安全协议自动检验技术以及串空间模型的应用等几个研究层面作了全面介绍.
其他文献
统计分析在海量数据库应用中占据很大比重.如何提高统计分析的效率是优化数据库应用性能面临的重要问题.语义缓存技术能够通过重用已有查询结果加快统计分析的速度,是一种非常有效的优化方法.本文以一个海量数据库系统为平台面向统计分析的需求对中间层语义缓存进行了研究,首先提出了一个语义缓存的体系结构,然后阐述了语义缓存的关键技术,最后通过试验验证了中间层语义缓存的有效性.
目前为止,网络入侵检测系统的研究主要集中在检测的有效性和检测效率等方面,网络入侵检测系统本身的一些安全问题,如可靠性和生存健壮性等问题并没有得到足够的重视和研究,本文针对网络入侵检测系统-snort,就入侵检测系统的自身安全问题进行了深入地研究,并利用分布式协同攻击技术对NIDS的可靠性和生存健壮性进行了测试.实验结果显示,当前的NIDS对分布式攻击来说是脆弱的.
基于BGP协议构造的域间路由系统是Internet的基础设施.域间路由系统面临多种恶意攻击的威胁且易受人为错误的影响.由于危害域间路由健康与安全的因素较多,单一防范方法难以奏效.本文在全面分析域间路由安全威胁的基础上,提出实现域间路由安全的系统化方法,从安全策略检测、路由协议增强、路由器健壮性设计、路由行为监测以及安全能力测试等多个角度来增强域间路由系统的安全能力,并建立域间路由系统的安全能力模型
计算网格能够提供了一个计算的基础设施,它能够提供多用户之间灵活、安全和协调的资源共享.本文首先提出了多个接受者的RSA可验证加密理论,并利用它建立网格计算中的可信自治域.提出了一个三方协议,建立了"计算发起方"与"计算协同方"之间的信任模型.
网络嗅探器是一种最常用的网络管理工具,更是一种必要的黑客工具,本文主要从共享网络环境中网络嗅探器存在的检测和网络嗅探的预防、交换环境下网络嗅探与预防和无线网络环境中的网络嗅探及预防三个方面对当前网络嗅探技术加以研究.
本文给出网络安全战略预警系统的组成,讨论现有的入侵检测技术,攻击检测系统的逻辑结构,并在监听、检测、反应、系统的设计等方面进行研究.网络环境下安全事件的分布式协同预警技术的基本原理是在一个分布式入侵检测系统(DIDS)基础上,统计入侵事件的特征和规律,从而预测将来一段时间内可能的入侵行为及其特征.分布式入侵检测系统的基本任务是从大规模网络中采集和分析网络信息,从中提取、过滤重要的安全信息,及时准确
本文通过网络传播的计算机病毒和蠕虫程序不仅破坏计算机系统而且对网络本身造成的破坏也变得越来越严重.自防御网络是指通过综合的安全手段,使得网络自身能从各个方面抵御有害的攻击.本文的研究将集中于自防御网络的实现手段的研究,提出一个基于网络自动重配置的自防御网络体系架构并研究其实现方式.
本文在分析了网络内容审计系统和互联网的现状,并在此基础上提出了一个网络内容审计系统下分布式的数据采集和分析模型,以此模型来作为网络审计系统的基础构件,适应当今的网络状况.该模型能灵活地为实际的网络审计系统提供其所需要的关于网络的多方面信息,在起到其作为网络审计系统基础件作用的同时,也使网络审计系统组件化.
应急响应是近年来人们为了应对各种突发网络事件而提出来的一种采用联动策略的综合防范措施.本文通过对网络安全事件的现状与特点的分析,给出了应急响应体系的关键属性,进而指出网络可生存性理论是应急响应的先进理论.文章进一步探讨了应急响应的总体架构和具体实施流程.最后从技术和实施进程两个角度对网络安全应急响应体系建设的实施方案进行了研究.
为了保障网络上信息的安全性,需要对网络中的邮件进行检测、封堵和拦截,在此过程中,会产生大量的残缺邮件,这样会导致后续工作的分析负担加重.为了准确地对残缺邮件进行识别,本文在对RFC规范中对邮件格式规范的分析的基础上,介绍了一种残缺邮件的识别方法,并进行了大量的实验,最后给出了实验结果及分析.