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

发布时间：2023-02-05 15:31

　　安全协议是实现安全的分布式系统的基础,所以保证其正确地工作至关重要。不幸的是,安全协议的设计存在一些非常微妙的细节,很难保证在设计过程中就能发现可能存在的漏洞。为此,在过去的20年间,研究人员提出了许多严格的形式化分析方法用于协议的安全性分析。其中,一种名为“BAN逻辑”的基于逻辑推理的分析方法,因其以通俗的概念来侦测协议中存在的漏洞和冗余,而获得了广泛的应用和好评。GNY是BAN的众多后继者中的一员,它扩展了BAN逻辑中的许多内容使得便于利用GNY开发自动化验证系统。 基于形式逻辑的思想,一种名为“信任多集”的形式化分析方法被提出来,它明确指明了保证密码协议足够安全的充分必要条件,同时对于存在安全性缺失的密码协议,能够有限度地给出构造攻击的结构。本文将阐述,信任多集在经过改进和完善后,不仅可用于手工分析也便于开发自动验证系统。 BMF Package就是基于“信任多集”所开发出的一套自动化验证系统。它由Prolog语言编写的分析器BMF Analyzer和可视化建模工具Visual BMF组成。它借鉴了南非开普敦大学基于GNY逻辑所开发的Spear2系统。 本文的结构如下：第2章主要...

【文章页数】：95 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
目录
图目录
表目录
第一章 绪论
    1.1 背景及其意义
    1.2 我的工作
    1.3 论文的组织结构
第二章 安全协议的介绍
    2.1 安全协议形式化
    2.2 安全协议的安全性质
    2.3 安全协议的分类
    2.4 安全协议的漏洞以及可能攻击
    2.5 本章小结
第三章 安全协议形式化分析的研究与进展
    3.1 形式逻辑分析方法
    3.2 模型检测方法
    3.3 定理证明方法
    3.4 本章小结
第四章 BAN逻辑的介绍
    4.1 BAN逻辑的前提假设和适用范围
    4.2 基本概念和符号
    4.3 基本推导规则
    4.4 安全协议的理想化
    4.5 BAN逻辑的推导过程
    4.6 BAN逻辑中的认证协议的目标
    4.7 使用BAN逻辑进行协议分析
    4.8 BAN逻辑的缺陷
第五章 信任多集形式化分析方法的改进
    5.1 一些引论
    5.2 拥有和关联
    5.3 基本概念和符号
    5.4 基本推导规则
    5.5 安全协议的形式化
    5.6 信任多集中的初始化假设
    5.7 信任多集的计算模型
    5.8 信任多集的推导过程
    5.9 信任多集中的安全协议目标
    5.10 使用信任多集进行协议分析
    5.11 本章小结
第六章 信任多集自动化分析的实现
    6.1 Spear2的简单介绍
    6.2 Prolog的简单介绍
    6.3 信任多集的Prolog表示
    6.4 一些预备知识
    6.5 前向链推导引擎的实现
    6.6 ^*(M)集合的实现
    6.7 推导规则的实现
    6.8 使用Prolog输出推导过程
    6.9 可视化定制环境-Visual BMF
    6.10 使用BMF Package对Otway-Rees协议进行分析
    6.11 本章小结
第七章 结束语
    7.1 总结
    7.2 展望
参考文献
致谢



本文编号：3735226