不可否认协议可以为网络上实体间的交互行为提供不可抵赖的证据。近年来，电子商务等Intemet应用的发展极大地推动了不可否认协议的研究。尽管如此，在不可否认协议研究领域还是存在很多问题。目前还没有出现比较完善实用的协议，相关的标准化工作更是滞后。 时限性和对可信第三方TTP(TrustedThirdParty)的依赖是不可否认协议的两个重要性质，它们都会对协议的安全性和性能产生影响。目前还没有对它们进行足够的研究。另外，不可否认协议和一般密码协议相同，也需要形式化的协议分析方法的验证以保证其安全性。目前对不可否认协议的形式化分析仅着重于协议目标(证据的有效性)和公平性的分析，而对如何描述和分析影响公平性的其他性质(如时限性)缺乏足够的研究。这导致一些有缺陷的协议在分析中被认为是安全的。 本论文的目标就是研究协议设计中如何既实现协议的时限性又保证协议对TTP的低依赖性，并研究如何使用形式化分析方法描述和分析不可否认协议特有的性质以保证其安全性。 研究协议时限性的关键是解决同步方法会带来额外的开销和异步方法对TTP依赖性的增强之间的矛盾。本论文提出了一种基于时间段概念的不可否认协议的时限性实现技术。它在满足时限性要求的同时，不需要实体间的时钟同步机制，提高协议效率，并有效降低协议对TTP的依赖。在对TTP依赖性的研究中，论文明确证明了各种不可否认协议对TTP产生的最低依赖并提出了降低协议对TTP依赖性的办法。作为上述研究的成果，论文设计并实现了一个安全高效的不可否认协议。通过本论文中各种形式化分析方法的验证和它在电子邮件系统中的应用表明该协议是公平高效的。 在不可否认协议形式化分析方法的研究方面，论文首先研究了SVO逻辑的性质及其在不可否认协议形式化中的应用。对SVO逻辑进行了扩展后将其应用于对不可否认协议的分析验证。由于逻辑方法本身难以克服的缺陷，论文又研究了不可否认协议的Petri网分析方法，首次提出了使用Petri网分析不可否认协议的完整步骤和方法。最后，综合逻辑方法和Petri网方法，论文提出了一种不可否认协议Petri网建模方法。该建模方法参考SVO逻辑的协议描述方法和语义模型，设计了一种简单直观的不可否认协议描述语言NDL。然后提出了从不可否认协议的NDL语言描述到有色Petri网模型的转换规则。最后实现了一个基于这些转换规则的编译程序，它能从不可否认协议的NDL语言描述文件生成其有色Petri网模型，供CPNTools进行自动化分析。对多个不可否认协议的形式化分析结果证明了上述形式化分析方法的正确和有效。 本论文的研究表明不可否认协议特殊性质需要特殊的设计技术，不可否认协议的形式化分析也需要特殊的方法。本论从不可否认协议的TTP依赖性和时限性的实现与形式化分析进行了研究。希望这些研究能为不可否认协议的发展尽一点绵薄之力。