一种基于BAN类逻辑的安全协议分析方法及其自动化实现

来源 :浙江大学 | 被引量 : 0次 | 上传用户:dqqwa
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
安全协议是实现安全的分布式系统的基础,所以保证其正确地工作至关重要。不幸的是,安全协议的设计存在一些非常微妙的细节,很难保证在设计过程中就能发现可能存在的漏洞。为此,在过去的20年间,研究人员提出了许多严格的形式化分析方法用于协议的安全性分析。其中,一种名为“BAN逻辑”的基于逻辑推理的分析方法,因其以通俗的概念来侦测协议中存在的漏洞和冗余,而获得了广泛的应用和好评。GNY是BAN的众多后继者中的一员,它扩展了BAN逻辑中的许多内容使得便于利用GNY开发自动化验证系统。基于形式逻辑的思想,一种名为“信任多集”的形式化分析方法被提出来,它明确指明了保证密码协议足够安全的充分必要条件,同时对于存在安全性缺失的密码协议,能够有限度地给出构造攻击的结构。本文将阐述,信任多集在经过改进和完善后,不仅可用于手工分析也便于开发自动验证系统。BMF Package就是基于“信任多集”所开发出的一套自动化验证系统。它由Prolog语言编写的分析器BMF Analyzer和可视化建模工具Visual BMF组成。它借鉴了南非开普敦大学基于GNY逻辑所开发的Spear2系统。本文的结构如下:第2章主要介绍安全协议,安全协议的漏洞以及可能的攻击;第3,4章进入正题开始介绍安全协议的形式化分析;第5,6章是信任多集的改进及其自动化实现,这也是我的主要工作。
其他文献
随着现代信息技术的飞速发展,人们对存储系统的容量、性能提高要求的同时,也越来越注重容错能力。作为存储系统管理核心层次的分布式文件系统,也毋庸置疑需要具有较高的容错
轨迹数据是一种常见的序列化上下文数据,其从空间和时间维度描述了用户移动轨迹信息。而对轨迹数据全面的获取、准确的挖掘与利用,是当前面向位置计算所需解决的主要问题。通过
作为蓬勃发展的新技术之一,物联网技术逐渐被应用到各个领域,特别是在医疗健康领域。作为人们身边的医疗服务,社区医疗与人们的生活息息相关,因此也被人们寄予了更高的要求。面对
CAD模型检索是实现设计模型重用的基础,对于缩短产品开发周期,降低产品开发成本具有重要作用。相对于零件模型检索而言,装配模型检索的研究还比较初步,现有的装配模型检索方
大规模网络服务系统环境中,短时的大规模用户合法行为聚集会造成系统行为异常,使得系统可用性受到极大的损害。如何感知系统出现异常并采取相应的措施提高系统的可用性,是目前大
随着无线通信、嵌入式计算机和传感器等技术的快速发展,具有感知能力、计算能力和无线通信能力的微型传感器以及由其构成的无线传感器网络引起了人们极大的关注。目标跟踪实质
目前,计算机网络安全领域正面临着严重的挑战,木马、病毒、蠕虫等各种网络攻击行为正严重威胁着广大用户的数据和信息的安全。其中,木马攻击技术不断变化,已经造成了严重危害
学位
随着网络技术的迅速发展和网络需求的日益扩大,一个可信、安全、稳定的网络管理系统己经成为网络正常运行的关键。如何发现完整的网络拓扑结构并建立有效的网络拓扑模型,对现
现有网络管理方案面临的一个问题是缺乏统一的管理流程,包括功能流程和业务流程。另一个问题是基于SNMP的网络管理系统通常采用集中式网络管理模型,不适合应用于较大规模的网络