学位论文 > 优秀研究生学位论文题录展示

安全协议形式化模型刻画与代数属性研究

作　者: 陈晨
导　师: 陈卫红
学　校: 解放军信息工程大学
专　业: 密码学
关键词: 安全协议形式化分析多集重写项重写代数属性终止性
分类号: TP274
类　型: 硕士论文
年　份: 2010年
下　载: 17次
引　用: 0次
阅　读: 论文下载

内容摘要

形式化分析是构建安全协议自动化检测平台的基础。本文主要围绕安全协议形式化分析中存在的模型刻画与代数属性问题展开研究,提出模型扩展类型和自动化实现算法,并分析相关基础理论及应用,主要内容包括:首先,扩展以多集重写理论为基础的分析模型。通过增添密钥类型和转换规则,完善模型对类型攻击的检测;在增加发送、接收谓词和证据函数的基础上,进一步扩展模型对非否认性与公平性的分析能力,并分别选取Yahalom协议和Fair-ZG协议进行实例验证。其次,分析因代数属性引起的攻击者推演问题,提出一个自动化的实现算法。针对目前已有的理论成果和工具无法处理多数类型的代数等式问题,研究了基于项重写理论的形式化分析方法,给出一个解决等价理论下攻击者推演问题的统一算法。该算法基于区分等价理论和选取代表元两个思想,能够处理多数已发现的针对代数属性问题的中间人攻击,并以BAP协议为例进行自动化检测。再次,研究项重写理论的终止性证明及其在信息安全领域中的应用。针对多项式序、字典路径序等存在难以实现自动化、规则调用次数过多等缺点,给出一个基于标准化和向量化思想的向量序。该序不仅能够检测项重写系统的终止性,而且具有易于自动化运算,规则调用次数较少的优点。基于向量序的构建思想,提出一个解决异或操作等价合一问题的算法,该算法分析合一的所有条件,并在合一运算成功时输出合一解。最后,探讨项重写理论在安全电子交易领域中的应用。针对安全电子交易模型包含大量的程序语言和文字性描述,难以展开形式化研究等缺点,构建一个基于项重写理论的分析模型,该模型体现了交易双方能够互相检验身份的安全机制,不但满足完整性和一致性的模型性质,而且具有认证性和非否认性的安全属性。

全文目录

摘要  7-8
ABSTRACT  8-9
第一章绪论  9-14
  1.1 论文背景  9
  1.2 安全协议形式化研究现状  9-12
    1.2.1 基于逻辑推理的形式化分析方法  10
    1.2.2 基于定理证明的形式化分析方法  10-11
    1.2.3 基于模型检测的形式化分析方法  11-12
  1.3 论文工作  12-13
  1.4 论文结构安排  13-14
第二章模型刻画问题研究  14-22
  2.1 MSR模型简介  14-16
    2.1.1 基本概念  14-15
    2.1.2 重写模型  15-16
    2.1.3 执行模型  16
  2.2 MSR模型扩展  16-21
    2.2.1 类型扩展  16-18
    2.2.2 安全属性检测  18-21
  2.3 本章小结  21-22
第三章代数属性问题研究  22-35
  3.1 项重写理论简介  23-26
    3.1.1 基本概念  23-25
    3.1.2 项重写系统  25-26
  3.2 攻击者推演问题分析  26-30
    3.2.1 基于TRS的形式化描述  26-27
    3.2.2 等价理论划分  27-28
    3.2.3 代表元选取  28-30
  3.3 算法实现  30-34
    3.3.1 算法设计  30-32
    3.3.2 复杂度分析  32
    3.3.3 算法实例研究  32-34
  3.4 本章小结  34-35
第四章项重写理论终止性分析  35-48
  4.1 终止性证明  35-37
    4.1.1 不可判定性  35
    4.1.2 约简序简述  35-36
    4.1.3 多项式序  36-37
    4.1.4 字典路径序  37
  4.2 向量序的构建与分析  37-42
    4.2.1 向量序构建  38-40
    4.2.2 序的对比  40-42
  4.3 向量序的工程应用  42-46
    4.3.1 等价合一问题分析  42-43
    4.3.2 算法实现  43-44
    4.3.3 算法实例分析  44-46
  4.4 本章小结  46-48
第五章项重写理论在安全电子交易中的应用  48-54
  5.1 安全电子交易简述  48-49
  5.2 形式化建模  49-52
    5.2.1 模型基础  49-50
    5.2.2 电子交易过程形式化分析  50-52
  5.3 模型性质与安全属性研究  52-53
    5.3.1 完整性与一致性分析  52
    5.3.2 安全属性分析  52-53
  5.4 本章小结  53-54
结束语  54-56
参考文献  56-59
作者简历攻读硕士学位期间完成的主要工作  59-60
致谢  60

安全协议形式化模型刻画与代数属性研究

内容摘要

全文目录

相似论文