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