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

论文摘要

长期以来,密码模块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形式化模型进行验证,不仅能验证已知的攻击,而且还发现了新的攻击,并且验证时效性优势明显。

论文目录

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