逻辑化方法的改进及若干密码协议安全性分析

论文摘要

论文在李逻辑的基础上提出一种新的BAN类逻辑系统,引进了新的符号、公式,添加了消息源公理,改进了消息生成公理、身份认证公理、消息接收公理,将系统加以扩展,并且列出若干常用定理。系统更好地刻划公钥密码体制在身份认证和密钥分发中起的作用,解决了如何对只使用公钥密码体制的密码协议证明数据的双向可追溯性,使系统更加完善,适用于更多密码协议,如NSL协议。进一步在新的认证逻辑系统上,对NSL协议和3G认证与密钥分发协议安全性进行了逻辑化分析。证明了NSL协议是一个强安全的身份认证协议,证明了NSL中临时值N_A和N_B的机密性和双向可追溯性。分析了3G认证与密钥分发协议的安全性,并针对协议的安全漏洞,提出了改进的协议方案,解决了用户的身份泄露和MS对VLR的认证的问题,MS通过产生的随机数,参与了密钥的分配,增强了协议的安全性,并对改进的协议安全性进行了逻辑化分析。

论文目录

• 摘要
• ABSTRACT
• 第一章 前言
• 第二章 基础知识
• 2.1 命题逻辑系统
• 2.2 谓词逻辑系统
• 第三章 逻辑化方法研究
• 3.1 若干基本概念和记号
• 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.1 NSL协议
• 3.1.1 NSL协议过程
• 3.1.2 NSL协议的安全性分析
• 3.2 3G认证与密钥分发协议
• 3.2.1 3G认证与密钥分发协议过程
• 3.2.2 3G认证与密钥分发协议安全性分析
• 3.2.3 3G认证与密钥分发协议的改进方案
• 结束语
• 致谢
• 参考文献