认证和密钥分配协议的可证明安全研究

论文摘要

可证明安全是一种证明密码学方案安全性的形式化方法，它将密码学方案的安全性规约为公认的计算难题，并已成为现代密码学领域中理论工作的主线。本文主要研究密钥分配协议的可证明安全，这包括它们的各种形式化安全定义以及达到这些安全性定义的方案构造。并且研究这些模型在设计和分析现实中的一些密钥管理方案方面的具体应用。本文得到的主要结果如下：1.对当前主流的分析密钥分配协议的可证明安全的随机预言机模型方法进行分析总结，并讨论其在设计和证明密钥分配协议安全性方面的密码学用途。2.对中国无线局域网国家标准WAPI中用户身份鉴别和密钥管理方案进行分析，发现其存在的两个安全缺陷，改进后得到一个可证明安全的身份鉴别和密钥管理方案。=3.针对无线传感器网络存在的一系列安全问题，基于CK模型，形式化地提出一种快速、高效且适用于大规模传感器网络的密钥管理方案。4.填补SIP描述中缺乏具体安全机制的空白，提出一种基于挑战－应答的SIP安全机制，实现了消息的双向认证，并且利用可证明安全技术证明了方案的安全性，较其他同类方案具有密钥规模小、计算速度快等明显优势。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 协议的形式化分析方法
• 1.1.1 BAN 逻辑
• 1.1.2 状态系统探查
• 1.1.3 可证明安全技术
• 1.2 可证明安全方法
• 1.3 课题支持
• 1.4 论文的内容安排
• 第二章 安全模型
• 2.1 BR 模型
• 2.1.1 两方 BR 模型
• 2.1.2 三方 BR 模型
• 2.1.3 小结
• 2.2 BCK 模型
• 2.2.1 参与者行为的形式化模型
• 2.2.2 安全目标
• 2.2.3 实例研究
• 2.2.4 讨论
• 2.3 CK 模型
• 2.3.1 参与者行为的形式化模型
• 2.3.2 安全目标
• 2.3.3 实例研究
• 2.4 模型间的比较
• 2.5 本章小结
• 第三章 WAPI接入鉴别过程安全性分析及改进
• 3.1 WAPI 简介
• 3.2 WAPI 接入鉴别过程
• 3.2.1 相关术语和定义
• 3.2.2 WAPI 接入鉴别过程
• 3.2.3 WAI 协议的形式化描述
• 3.2.4 WAI 协议的安全性分析
• 3.3 WAI 协议的改进
• 3.4 WAI'协议的安全性分析
• 3.4.1 WAI'1 协议的安全性证明
• 3.4.2 WAI'2 的安全性证明
• 3.5 本章小结
• 第四章 无线传感器网络密钥分配协议设计
• 4.1 无线传感器网络概述
• 4.2 相关工作
• 4.3 传感器密钥分配协议
• 4.3.1 安全需求
• 4.3.2 系统假设
• 4.3.3 协议的整体步骤
• 4.4 安全性分析
• 4.5 性能分析
• 4.6 本章小结
• 第五章 SIP协议的认证和密钥交换机制设计
• 5.1 SIP 协议概述
• 5.1.1 SIP 协议概要介绍
• 5.1.2 SIP 协议的实现机制
• 5.2 SIP 协议的安全机制
• 5.2.1 SIP 协议的安全机制
• 5.2.2 SIP 认证过程
• 5.2.3 SIP 认证和密钥交换协议
• 5.3 本章小结
• 第六章 结束语
• 致谢
• 参考文献
• 研究成果