公平不可否认协议设计及其形式化分析

论文摘要

公平不可否认协议可以保证通信双方对各自的行为不能进行抵赖,并保证双方的公平性。它使通信双方要么都收到消息及证据,要么都收不到消息及证据。该类协议是电子商务协议的基础。由于公平不可否认协议的重要性,对其设计及安全性分析是近十年来安全领域的一个研究热点。目前,国内外已有不少形式化方法分析该类协议。本文主要利用基于推理的逻辑方法来形式化分析非否认协议。前向安全是安全领域中又一个重要概念,它的提出主要是基于用户的签名私钥暴露,其他实体就会得到以前的签名或伪造新的签名,从而导致非否认问题。因此构造一个满足前向安全性的公平非否认协议也具有很大的实用价值。本文最后重点探讨了此类协议。论文主要工作如下:①简要介绍公平非否认协议及安全协议形式化分析方法的发展历史及现状。②主要介绍公平非否认协议形式化分析中的一些基础问题,包括用到的密码技术,非否认协议的概念及分类,基本假设及安全性质和设计思路与设计原则。另外还介绍和分析了协议的常见攻击及前向安全性质。③对著名的CMP1（Certified electronic mail 1）[1]协议进行分析,发现其存在一些安全缺陷,如只满足弱可追究性以及不满足公平性等,针对这些安全缺陷,文章引入了随机数的概念对原协议进行了改进。分析表明改进后的协议吸收了多种协议设计的优势而又有效的避免了各自缺陷,使其能够有效的满足不可否认性、公平性、保密性和高效性等安全服务。④对已有的双重加密密钥非否认协议（double-encrypted key non-repudiation protocol,简称DKNRP）[2]主要从攻击角度对其进行分析,发现其存在重放攻击。然后文中为解决这一缺陷提出了一个新的面向电子邮件的公平非否认协议。最后用SVO逻辑推理规则对新协议进行了形式化分析。分析表明,该协议满足非否认性以及公平性安全性质。⑤本章利用已有的签名机制,设计了一个与时间有关的安全电子邮件协议。该协议能够防止签名者私钥泄露后,其他实体伪造签名或得到过去时段的签名。另外,签名验证者不需要查找CA吊销列表,就能验证签名的有效性,极大的提高了验证签名效率。

论文目录

• 摘要
• ABSTRACT
• 1 绪论
• 1.1 公平非否认协议的研究背景
• 1.2 公平非否认协议研究现状
• 1.3 安全协议形式化方法的发展过程概述
• 1.3.1 基于推理的结构化方法
• 1.3.2 基于攻击的结构化方法
• 1.3.3 基于证明的结构化方法
• 1.4 论文主要工作
• 2 公平不可否认协议形式化分析的基础问题
• 2.1 相关的密码技术和密码机制
• 2.2 公平不可否认协议概念及分类
• 2.3 安全协议分析的基本假设及若干安全性质
• 2.4 公平不可否认协议常见攻击
• 2.5 前向安全性质
• 2.6 不可否认协议的设计思路与设计原则
• 3 SVO 逻辑方法
• 3.1 SVO 逻辑符号定义
• 3.2 SVO 逻辑方法原理
• 3.2.1 SVO 逻辑语言
• 3.2.2 SVO 逻辑系统
• 3.2.3 SVO 逻辑分析方法和步骤
• 3.2.4 SVO 逻辑分析目标
• 4 一种新型的面向电子邮件的非否认协议
• 4.1 面向电子邮件的非否认协议研究现状
• 4.2 基本标识符描述
• 4.3 改进前的CMP1 协议安全缺陷分析
• 4.4 改进后的面向电子邮件的公平非否认协议CMP1＇
• 4.5 改进后协议CMP1＇的分析
• 4.5.1 争端解决
• 4.5.2 公平性
• 4.5.3 保密性
• 4.5.4 高效性
• 4.6 改进后协议CMP1＇优点
• 4.7 本章小结
• 5 一种面向电子邮件的非否认协议及形式化分析
• 5.1 面向电子邮件的非否认协议一般安全缺陷
• 5.2 改进前DKNRP(（double-encrypted key non-repudiation protocol）描述及安全缺陷分析
• 5.3 一种面向电子邮件的公平不可否认协议
• 5.4 改进后协议的形式化分析
• 5.4.1 协议的预期目标
• 5.4.2 SVO 逻辑的推理规则及公理
• 5.4.3 协议的信任假设
• 5.4.4 协议目标形式化证明
• 5.5 本章小结
• 6 与时间相关的安全电子邮件协议
• 6.1 现有协议存在的缺陷
• 6.2 与时间相关的安全电子邮件协议
• 6.2.1 前向安全技术与单向hash 链
• 6.2.2 基本标识符
• 6.2.3 与时间相关的协议描述
• 6.2.4 协议安全性质分析
• 6.3 本章小结
• 7 总结与展望
• 总结
• 进一步工作展望
• 致谢
• 参考文献
• 附录