公平非否认协议可以防止通信主体对通信事件的抵赖行为并保证通信各方始终处于公平地位,是安全电子商务协议的基础。由于公平非否认协议的重要性,对它的各项安全性质进行分析是近十年来安全领域的研究热点。目前,国内外已提出了一些适用于分析公平非否认协议的形式化方法,这些方法主要分为三类:基于知识与信念的逻辑证明方法;基于模型化技术的状态搜索方法;基于定理证明的方法。这些分析方法或工具往往能分析公平非否认协议是否满足某个或某些性质,但目前还没有一种可以同时分析公平非否认协议非否认性、公平性及时限性的方法。鉴于安全协议各个安全性质的微妙相关性,单独分析某个或某些性质是不科学的。而在公平非否认协议中,非否认性、公平性和时限性是三个紧密相关和互相影响的性质,分析公平非否认协议性能时,忽略对任何一个性质的考虑,都可能使分析结果变得毫无意义。本文针对上述问题,通过深入研究公平非否认协议的相关安全性质的本质,在总结现有分析方法优缺点的基础上,提出了一种可同时分析公平非否认协议非否认性、公平性和时限性的方法。主要工作如下:1.深入研究了公平非否认协议的非否认性、公平性与时限性三个安全性质的本质。分析了目前应用于公平非否认协议分析的若干主要方法的原理、优缺点和应用范围。2.提出了一种基于可证性逻辑的,能同时分析非否认性、公平性与时限性的形式化分析方法。新方法对主体引入限时能力概念,使用“逐步断开,其余主体继续”的分析方案,并假设了一个攻击者能力集合,能全面地分析非否认性、公平性和时限性。使用新方法分析了若干典型的公平非否认协议,找到了一些已知的和未知的漏洞,验证了新方法的有效性。3.使用新方法验证了SET协议中的购买流程协议,有效地分析了该协议的非否认性、公平性和时限性。