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

基于进程演算的公钥密码体制自动化安全性证明方法研究

作　者: 陈楠
导　师: 祝跃飞
学　校: 解放军信息工程大学
专　业: 密码学
关键词: 公钥密码体制可证明安全自动化游戏转换进程演算观察等价 ElGamal加密体制
分类号: TN918.1
类　型: 硕士论文
年　份: 2010年
下　载: 28次
引　用: 0次
阅　读: 论文下载

内容摘要

可证明安全是当前密码体制安全性评估的重要依据。但手工证明的难度较大且正确性难以保证。利用计算机技术实现可证明安全性的自动化分析是解决这一问题的有效途径。本文对公钥密码体制自动化安全性证明方法进行深入分析和研究,在理论建模的基础上,开发一套可证安全自动化分析系统,可以实现对公钥密码体制的自动化安全性证明。本文主要工作如下:(1)提出基于“游戏转换”的安全性“规约”的具体实施方法。本文采用“游戏转换”的方式来实现密码体制和数学难题之间的“规约”证明,使用“游戏序列”来组织安全性证明过程。从初始攻击游戏出发,通过语法转换和依据密码原语安全性质或安全假设的转换这两种主要转换方式来获取游戏序列。(2)构建一个密码体制形式化描述模型。通过对符号化模型和计算模型这两种分析协议安全性的主流模型进行比较,选取抽象程度较低,模型更接近于实际的计算模型作为安全性证明的基础模型。针对计算模型证明过程繁琐,难以自动化实现的缺点,引入进程演算对其进行符号化改造,构建一个适用于公钥密码体制自动化安全性证明的形式化模型,这是可证安全自动化分析的前提。(3)定义一种提供给用户的高级描述语言。该语言是在形式化模型的基础上定义的,用以描述需要进行安全性证明的密码体制和期望达到的安全目标等,形成可证安全自动化分析系统的输入文件。输入文件经解析器解析后,形成计算机可识别的初始攻击游戏,可以进行进一步的转换证明。(4)引入观察等价理论和观察等价式的概念,给出观察等价式的构造方式和概率计算方法。观察等价为构建游戏序列提供了非常有用的理论依据,而观察等价式可以形式化描述密码原语的安全性质或算法假设,基于观察等价式的转换使自动化获取游戏序列成为可能。(5)提取基于循环群相关特性的代数恒等式和观察等价式,实现对ElGamal加密体制及其hash版本的自动化安全性证明。由于反映密码原语的安全性质或算法假设的观察等价式可以重用,所以基于循环群的相关代数性质所提取出的恒等式和观察等价式实际上也充实了自动化证明工具的转换规则库,这对其他具有相似密码性质的密码协议的自动化安全性证明具有借鉴意义。最后,对全文工作进行总结,并指出进一步研究方向。

全文目录

摘要  9-10
ABSTRACT  10-12
第一章绪论  12-18
  1.1 课题背景及意义  12-13
  1.2 国内外发展趋势及现状  13-15
    1.2.1 安全性证明模型  13-14
    1.2.2 自动化安全性证明的发展  14-15
  1.3 研究内容及难点  15-17
  1.4 论文结构安排  17-18
第二章预备知识  18-27
  2.1 可计算理论  18-21
  2.2 公钥加密体制  21-24
    2.2.1 公钥加密体制的安全性定义  21-24
    2.2.2 安全性间的关系  24
  2.3 签名体制  24-26
  2.4 数学难题  26
  2.5 小结  26-27
第三章自动化安全性证明方法研究  27-41
  3.1 计算模型  27-29
  3.2 基于游戏转换的可证明安全性  29-32
    3.2.1 可证明安全性  29-30
    3.2.2 基于游戏转换的安全性证明  30-32
  3.3 进程演算  32-37
    3.3.1 项代数的相关概念  32-33
    3.3.2 符号说明  33
    3.3.3 进程演算的语法  33-36
    3.3.4 类型系统  36
    3.3.5 两类密码原语及其安全性的形式化描述  36-37
  3.4 基于进程演算的密码体制安全性自动化证明方法  37-40
    3.4.1 游戏序列生成  38-40
    3.4.2 可证明安全性的判别条件  40
  3.5 小结  40-41
第四章可证安全自动化分析系统  41-50
  4.1 可证安全自动化分析系统概述  41-42
  4.2 输入文件结构  42-45
  4.3 基于观察等价式的游戏转换  45-47
  4.4 游戏的语法转换和化简  47-48
    4.4.1 游戏的语法转换  47-48
    4.4.2 游戏的化简  48
  4.5 转换策略和证明路径搜索  48-49
  4.6 小结  49-50
第五章 ElGamal加密体制的自动化安全性证明  50-64
  5.1 数学架构  50-52
    5.1.1 概率  50-51
    5.1.2 循环群  51
    5.1.3 循环群的概率性质  51-52
  5.2 形式安全  52-55
    5.2.1 DDH假设  52-53
    5.2.2 熵平滑  53
    5.2.3 语义安全  53-54
    5.2.4 适应性选择密文攻击下密文不可区分（IND-CCA2）  54
    5.2.5 加密体制的正确性  54-55
  5.3 ElGamal加密体制的安全性证明  55-57
    5.3.1 算法描述  55
    5.3.2 ElGamal加密体制的初始输入(IND-CPA)  55-57
    5.3.3 证明结果  57
  5.4 带hash的ElGamal加密体制的安全性证明  57-60
    5.4.1 算法描述  57-58
    5.4.2 带hash的ElGamal加密体制的初始输入(IND-CPA)  58-60
    5.4.3 证明结果  60
  5.5 证明失败案例  60-62
    5.5.1 ElGamal加密体制的初始输入（IND-CCA2）  60-62
    5.5.2 证明结果  62
  5.6 小结  62-64
结束语  64-66
参考文献  66-69
附录带hash的ElGamal加密体制自动化安全性证明过程（IND-CPA）  69-72
作者简历作者攻读硕士学位期间完成的主要工作  72-73
致谢  73

基于进程演算的公钥密码体制自动化安全性证明方法研究

内容摘要

全文目录

相似论文