密码协议符号分析方法的计算可靠性研究

论文摘要

密码协议形式化分析方法分为符号方法与计算方法两类。符号方法假设密码算法是完美的,但没有论证该假设的正确性。计算方法考虑了攻击者对密码算法的分析能力,接近协议的实际运行。目前,人们致力于在计算方法框架下论证完美假设的正确性,以建立符号方法的计算可靠性。Micciancio-Warinschi模型是该领域的经典模型,它给出了在主动攻击下建立符号方法计算可靠性的一般方法,但仅针对公钥加密原语和协议的认证性进行研究,且没有体现完美算法的随机性,不能分析包含{{m}k}k,类型消息的协议。鉴于此,本文给出了具有计算可靠性的扩展Micciancio-Warinschi符号方法,以扩展Micciancio-Warinschi模型的应用范围。本文所做的工作主要包括以下几点:1.基于Micciancio-Warinschi方法提出了扩展Micciancio-Warinschi方法,在该扩展方法内建立了使用数字签名、对称加密以及公钥加密等密码原语的扩展标记符号模型与扩展计算模型,并论证了扩展标记符号模型的计算可靠性。这是本文工作的重点与难点。2.用扩展Micciancio-Warinschi方法对NS公钥协议和NSL公钥协议进行了手工推导,得到的结果与理论一致,证明了扩展Micciancio-Warinschi方法的正确性。3.为使扩展标记符号模型便于机器分析与处理,给出了扩展标记符号模型的随机变换,并证明了随机变换的正确性。4.给出了扩展标记符号模型计算可靠性验证的原理、结构及工作流程,并利用现有验证工具实现了该模型的计算可靠性验证。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景及意义
• 1.2 密码协议形式化分析方法
• 1.2.1 符号方法
• 1.2.2 计算方法
• 1.3 计算可靠性研究现状
• 1.3.1 逻辑方法与模拟方法
• 1.3.2 LMMS:概率多项式时间下进程演算方法
• 1.3.3 符号方法的密码学扩充
• 1.3.4 总结
• 1.4 论文主要内容
• 第二章 Micciancio-Warinschi方法的分析与研究
• 2.1 公钥加密方案的安全性
• 2.2 双方协议
• 2.2.1 协议语法
• 2.2.2 协议执行模型—符号模型与计算模型
• 2.3 符号模型的计算可靠性
• 2.4 本章小结
• 第三章 扩展 Micciancio-Warinschi方法
• 3.1 扩展协议语法
• 3.1.1 标记
• 3.1.2 标记消息
• 3.1.3 标记角色
• 3.2 扩展标记符号模型
• 3.2.1 消息项
• 3.2.2 攻击者模型
• 3.2.3 协议描述
• 3.2.4 符号安全性建模
• 3.3 扩展计算模型
• 3.3.1 密码方案的安全定义
• 3.3.2 计算语义
• 3.3.3 计算安全性建模
• 3.4 计算可靠性论证
• 3.4.1 联系计算迹与符号迹
• 3.4.2 联系符号安全性质与计算安全性质
• 3.5 实例分析
• 3.5.1 NS公钥协议实例分析
• 3.5.2 NSL公钥协议实例分析
• 3.5.3 结果分析
• 3.6 本章小结
• 第四章 扩展标记符号模型的随机变换
• 4.1 随机变换
• 4.1.1 协议规范建模
• 4.1.2 攻击者建模
• 4.1.3 安全性质建模
• 4.2 随机变换规则
• 4.3 随机变换的正确性证明
• 4.4 本章小结
• 第五章 扩展标记符号模型的计算可靠性验证
• 5.1 ProVerif
• 5.1.1 ProVerif的基本结构
• 5.1.2 Horn语句
• 5.2 CryptoVerif
• 5.2.1 语法
• 5.2.2 安全特性
• 5.2.3 CryptoVerif输入语法
• 5.3 计算可靠性验证的结构及工作流程
• 5.4 计算可靠性验证的实现
• 5.4.1 输入部分
• 5.4.2 核心处理部分
• 5.4.3 结果输出部分
• 5.5 实验结果与分析
• 5.6 本章小结
• 第六章 结束语
• 6.1 论文工作总结
• 6.2 工作展望
• 参考文献
• 作者简历 攻读硕士学位期间完成的主要工作
• 致谢