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

密码模块API形式化验证技术研究

作　者: 吴晖
导　师: 马自堂
学　校: 解放军信息工程大学
专　业: 计算机应用技术
关键词: 密码模块API PKCS#11 API攻击形式化模型形式化验证合模式
分类号: TN918.2
类　型: 硕士论文
年　份: 2008年
下　载: 32次
引　用: 0次
阅　读: 论文下载

内容摘要

长期以来,密码模块API的安全性没有得到人们的充分重视和研究。直到2000年以后,随着API攻击在大多数的密码模块中不断发现,密码模块API的安全性才逐渐引起了人们的广泛注意和研究。随着研究的深入,使用形式化方法对密码模块API安全性进行分析与验证正在成为该领域的研究热点。本文以一个广泛应用的密码模块API—PKCS#11为例,对密码模块API形式化验证技术进行了深入研究。本文所做的工作主要包括以下几点:介绍了密码模块API和当前密码模块API形式化分析与验证领域的研究成果,分析了该领域的研究热点和不足。研究了一个典型的密码模块API—PKCS#11;分析了PKCS#11的安全机制;研究了已知的针对PKCS#11的API攻击,并使用协议描述方式进行了形式化描述;总结了PKCS#11存在的设计缺陷。研究了基于一阶逻辑和基于HLPSL的PKCS#11模型及其验证方法;并指出这两种PKCS#11形式化模型都只能表示单调的系统状态,没有正确建模密码模块API输入输出的非单调易变全局状态。提出了一套适用于描述PKCS#11的语法和形式化语义,建立了PKCS#11密码操作函数核心部分的形式化模型,该模型可对非单调易变全局状态做出合理解释;并通过引入“模式”的概念,建立了合模式规则,证明了合模式推导的存在性和在合模式化条件下模型安全属性的可判定性。即对于一个有限的名称集,使用有限的新鲜数,可以对模型的秘密属性做出可判定性结论。通过这个结论,可以限制模型的搜索空间。设计了PKCS#11形式化模型所采用的验证方法和策略:使用模型检测工具NuSMV对不同的PKCS#11安全配置方案进行了验证性实验;讨论了PKCS#11的安全配置;并比较了本文的验证方法与已有验证方法的实验结果。结果证明使用本文提出的形式化验证方法对改进的PKCS#11形式化模型进行验证,不仅能验证已知的攻击,而且还发现了新的攻击,并且验证时效性优势明显。

全文目录

摘要  6-7
Abstract  7-8
第一章绪论  8-19
  1.1 研究背景及意义  8-10
    1.1.1 课题背景  8-9
    1.1.2 课题意义  9-10
  1.2 相关研究现状  10-17
    1.2.1 密码模块API  10-14
    1.2.2 密码模块API安全性分析  14-15
    1.2.3 密码模块API形式化验证  15-17
  1.3 研究内容与组织结构  17-19
第二章 PKCS#11及其安全性分析  19-33
  2.1 PKCS#11概述  19-26
    2.1.1 PKCS#11结构模型  19-20
    2.1.2 对象  20-21
    2.1.3 会话  21-22
    2.1.4 函数  22-26
  2.2 PKCS#11的安全机制  26-27
  2.3 PKCS#11的API攻击  27-31
    2.3.1 通用API攻击  27
    2.3.2 密钥绑定攻击(Key Binding Attack)  27-28
    2.3.3 密钥分离攻击(Key Separation Attack)  28-29
    2.3.4 弱密钥/算法攻击(Weaker Key/Algorithms Attack)  29
    2.3.5 并行搜索攻击(Parallel Search Attack)  29-30
    2.3.6 相关密钥攻击(Related Key Attack)  30
    2.3.7 木马公钥攻击(Trojan Public Key Attack)  30-31
    2.3.8 加密的木马密钥攻击(Trojan Wrapped Key Attack)  31
  2.4 PKCS#11的设计缺陷  31-32
  2.5 本章小结  32-33
第三章 PKCS#11形式化模型研究  33-41
  3.1 基于一阶逻辑的PKCS#11形式化模型  33-36
    3.1.1 基本的一阶逻辑定义  33
    3.1.2 PKCS#11部分指令描述  33-34
    3.1.3 攻击者能力描述  34
    3.1.4 安全目标描述  34
    3.1.5 初始状态描述  34-35
    3.1.6 验证方法分析  35-36
  3.2 基于HLPSL的PKCS#11形式化模型  36-40
    3.2.1 AVISPA和HLPSL语言  36-38
    3.2.2 PKCS#11建模描述  38-39
    3.2.3 验证方法分析  39-40
  3.3 本章小节  40-41
第四章改进的PKCS#11形式化模型  41-52
  4.1 基本假设  41
  4.2 形式化模型  41-46
    4.2.1 语法和形式化语义  41-43
    4.2.2 密码模块API描述  43-44
    4.2.3 安全属性描述  44-45
    4.2.4 攻击的模型表示  45-46
  4.3 模型的理论证明  46-51
    4.3.1 合模式规则  46-47
    4.3.2 合模式推导的存在性证明  47-51
    4.3.3 可判定性结论  51
  4.4 本章小节  51-52
第五章 PKCS#11安全性验证  52-62
  5.1 验证工具介绍  52-53
    5.1.1 NuSMV  52-53
    5.1.2 基于OBDD的符号模型检测  53
  5.2 验证方案设计  53-57
  5.3 验证实验与结论  57-61
  5.4 本章小结  61-62
第六章结束语  62-64
  6.1 论文工作总结  62-63
  6.2 下一步工作展望  63-64
参考文献  64-68
附录 PKCS#11密码操作函数部分NuSMV语言脚本  68-77
作者简历攻读硕士学位期间完成的主要工作  77-78
致谢  78

密码模块API形式化验证技术研究

内容摘要

全文目录

相似论文