基于CP-nets模型的安全协议形式化方法研究

发布时间：2021-11-12 12:41

　　随着计算机网络的迅速发展,信息通信的安全问题变得越来越突出,越来越复杂,解决安全问题对许多网络应用来说具有重要意义。目前,网络通信安全问题的解决方案中,安全协议是最有效的手段之一。由于网络本身的开放性,使得网络中存在着各种安全威胁,攻击者可以采用多种方式对安全协议进行攻击,破坏其安全属性。分析安全协议中可能存在的缺陷很难完全由人工来识别,因此,需要借助形式化的分析方法和工具来完成。安全协议的形式化分析过程包含安全协议系统建模、安全属性验证、以及攻击序列生成等。本文通过分析安全协议模型中攻击者的“任意”性行为和协议的多次并发会话问题,提出了一种改进的攻击者模型和多并发会话划分分析方法。针对安全属性验证和攻击序列生成问题,采用安全属性违背事件对不安全状态进行分类描述,提出基于安全属性违背事件生成攻击序列的两种方法：状态空间搜索法和on-the-fly生成方法。基于安全属性违背事件生成攻击序列的方法能够有效地控制搜索范围,提高搜索效率。最后通过分析安全协议中的数据特征,提取能够构成攻击的攻击策略,并依据攻击策略确定攻击目的,构建基于攻击目的的模型,选择生成攻击序列,有效地削减安全协议模型检测... 

【文章来源】：内蒙古大学内蒙古自治区 211工程院校

【文章页数】：122 页

【学位级别】：博士

【文章目录】：
摘要
ABSTRACT
縮略词
第一章 引言
    1.1 研究背景及意义
    1.2 论文的贡献
    1.3 论文的组织
第二章 相关研究概述
    2.1 安全协议及其性质
        2.1.1 安全协议分类
        2.1.2 安全属性
    2.2 形式化建模方法
    2.3 安全协议形式化分析方法
        2.3.1 基于推理证明的模态逻辑方法
        2.3.2 定理证明方法
        2.3.3 基于类型检测的方法
        2.3.4 模型检测方法
    2.4 攻击者模型
        2.4.1 Dolev-Yao攻击者模型
        2.4.2 安全协议的攻击分类
    2.5 攻击序列生成方法
        2.5.1 基于定理证明的攻击序列生成方法
        2.5.2 基于模型检测的攻击序列生成方法
    2.6 基于CP-nets模型的形式化方法
        2.6.1 CP-nets模型形式化定义
        2.6.2 CP-nets的主要分析技术
        2.6.3 CP-nets应用现状
    2.7 本文研究的问题
    2.8 本章小结
第三章 安全协议的形式化建模
    3.1 方法概述
    3.2 安全协议建模约束
    3.3 Dolev-Yao攻击者模型的改进
        3.3.1 Dolev-Yao攻击者模型
        3.3.2 一种改进的攻击者模型
        3.3.3 应用实例：NS协议
    3.4 多并发会话划分分析方法
    3.5 并发行为控制
    3.6 实例系统：TMN协议
        3.6.1 建模约束条件
        3.6.2 TMN协议的数据建模
        3.6.3 TMN协议的CP-nets建模
        3.6.4 TMN协议的CP-nets模型安全属性验证分析
    3.7 小结
第四章 基于CP-nets的安全协议模型验证与攻击序列生成
    4.1 方法概述
    4.2 ATG-CPN模型形式化定义
    4.3 安全属性描述
        4.3.1 保密性属性形式化定义
        4.3.2 认证性属性形式化定义
    4.4 基于安全属性违背事件的攻击序列生成算法—状态空间搜索法
        4.4.1 安全属性违背事件
        4.4.2 算法的形式描述
        4.4.3 NS协议的攻击序列生成
    4.5 On-the-fly安全协议攻击序列生成
        4.5.1 ATG_X-CPN模型描述
        4.5.2 On-the-fly攻击序列生成方法
    4.6 实例分析：TMN协议系统
        4.6.1 TMN协议的ATG-CPN模型
        4.6.2 基于状态空间搜索方法的攻击序列生成与分析
    4.7 本章小结
第五章 基于攻击目的的攻击序列选择
    5.1 方法概述
    5.2 安全协议的主要攻击方式
        5.2.1 攻击者的攻击策略和攻击行为
        5.2.2 攻击策略的评判
    5.3 攻击目的AP-CPN形式化描述
    5.4 基于攻击目的的攻击序列选择方法
    5.5 实例分析：TMN协议系统
        5.5.1 TMN协议的攻击策略评判
        5.5.2 TMN协议的攻击策略建模
        5.5.3 TMN协议的攻击序列选择生成
    5.6 本章小结
第六章 结论及进一步工作
    6.1 论文的主要结论
    6.2 进一步的研究工作
参考文献
致谢
攻读博士学位期间发表论文
攻读博士学位期间主持和参加的科研项目


【参考文献】：
期刊论文
[1]安全协议:信息安全保障的灵魂——安全协议分析研究现状与发展趋势[J]. 薛锐,雷新锋.  中国科学院院刊. 2011(03)
[2]基于面向对象时间Petri网的密码协议分析[J]. 刘雪艳,吴慧欣,张强,王彩芬.  计算机工程. 2009(13)
[3]安全协议的形式化分析技术与方法[J]. 薛锐,冯登国.  计算机学报. 2006(01)
[4]串空间代数缺陷到实际攻击的转换[J]. 沈海峰,黄河燕,陈肇雄.  计算机科学. 2005(07)
[5]基于进程代数安全协议验证的研究综述[J]. 李梦君,李舟军,陈火旺.  计算机研究与发展. 2004(07)
[6]安全协议形式化分析理论与方法研究综述[J]. 冯登国,范红.  中国科学院研究生院学报. 2003(04)
[7]一种通信协议测试序列生成的新方法[J]. 孙宇霖,屈玉贵,赵保华.  通信学报. 2001(06)
[8]随机Petri网的分解和压缩技术[J]. 林闯.  软件学报. 1997(07)

硕士论文
[1]安全协议攻击序列重构技术研究[D]. 张超.解放军信息工程大学 2008



本文编号：3490934