基于反例的安全协议漏洞挖掘
发布时间：2020-12-26 05:19
如今中国已经进入了一个互联网+的时代,各行各业都搭上了互联网的快车。安全协议作为一个关系到互联网流通的信息安全的重要因素,变得举足轻重。目前分析协议的方法多种多样,模型检测作为一种形式化方法受到广泛关注和认可。本文在前人建模、验证的基础上,扩展出反例分析阶段。试图从反例角度出发,从反例中提取有效信息,通过分析反例来定位漏洞位置。模型检测方法具有两个主要的优点:第一,模型检测具有高度的自动化,可以使研究者从繁杂的搜索任务中解脱出来。第二,当系统或者协议不满足约定的性质时,模型检测工具可以返回一个源码级别的事件序列,既反例。但是随着功能的增加和完善,现有的系统和协议变得越来越复杂,与之对应的反例数量越来越多,内容也越来越复杂,因此对反例的分析也变得越来越困难。本文提出了消除众多相似反例的方法。在使用模型检测器对协议进行验证时候,我们发现会有大量的相似反例,他们体现了同一个安全漏洞,但我们仅仅需要一个此类的反例,过多的反例只会增加系统负担,给分析反例的过程带来干扰。本文通过引入节点权重方法来在反例生成时消除相似反例。为了保证去重效果又增加了反例生成后的消除过程。以此来保证反例集合中没有相似反...
【文章来源】：电子科技大学四川省 211工程院校 985工程院校 教育部直属院校
【文章页数】：88 页
【学位级别】：硕士
【部分图文】：
转换过程
图2-1 转换过程2.1.2 CTL分支时序逻辑图2-2 常用CTL运算符CTL（Computation Tree Logic）分支时序逻辑是CTL*计算树逻辑的一个子集，该子集受到一些限制：其中每个时序运算符X、F、G、U和R必须由一个路径量词
第二章 安全协议分析相关理论领。在很大程度上说，CTL是CTL*由以下路径公式语法规则来代替CTL*中则而得到的子集：如果f和g是状态公式，那么Xf、Ff、Gf、fUg和fRg是路径公图2-2描述来了四种基本的CTL运算符：M，0 EF g、M，0 AF g、 MEG g、 M，0 AG g。1.3 LTL线性时态逻辑线性时态逻辑[22-23]（LTL，Linear Temporal Logic）包括具有形为Af的公式中f是路径公式，它的状态子公式只允许为原子命题。如下图2-4表示了LTL运。更准确的说，LTL路径公式为以下两种：（1）如果p ∈ AP'，则p为路径公式。（2）如果F和g是路径公式，则 f、f∨g、f∧g、X f、F f、G f、f U G和f 路径公式。
本文编号：2939112
【文章来源】：电子科技大学四川省 211工程院校 985工程院校 教育部直属院校
【文章页数】：88 页
【学位级别】：硕士
【部分图文】：
转换过程
图2-1 转换过程2.1.2 CTL分支时序逻辑图2-2 常用CTL运算符CTL（Computation Tree Logic）分支时序逻辑是CTL*计算树逻辑的一个子集，该子集受到一些限制：其中每个时序运算符X、F、G、U和R必须由一个路径量词
第二章 安全协议分析相关理论领。在很大程度上说，CTL是CTL*由以下路径公式语法规则来代替CTL*中则而得到的子集：如果f和g是状态公式，那么Xf、Ff、Gf、fUg和fRg是路径公图2-2描述来了四种基本的CTL运算符：M，0 EF g、M，0 AF g、 MEG g、 M，0 AG g。1.3 LTL线性时态逻辑线性时态逻辑[22-23]（LTL，Linear Temporal Logic）包括具有形为Af的公式中f是路径公式，它的状态子公式只允许为原子命题。如下图2-4表示了LTL运。更准确的说，LTL路径公式为以下两种：（1）如果p ∈ AP'，则p为路径公式。（2）如果F和g是路径公式，则 f、f∨g、f∧g、X f、F f、G f、f U G和f 路径公式。
本文编号：2939112
本文链接：https://www.wllwen.com/kejilunwen/sousuoyinqinglunwen/2939112.html
