移动自组网Manet(Mobilead-hocnetworks)是由若干带有无线收发器的移动节点所组成的无基站的自治网络，广泛应用于军事、民用、商业等各个领域。在商业领域中，诸如电子商务、网上银行的网络应用对安全性的要求极高，为此人们提出了公平非抵赖协议。　　 非抵赖协议是指为保证交易双方对交易行为无法抵赖，在交易结束后，交易双方都必须得到相应的证据，在出现争议时，仲裁方便能依据双方提供的证据进行仲裁。当交易双方使用非抵赖协议进行交易后，双方都不能否认参与此次信息交换。而一个公平的非抵赖协议则是指，当非抵赖协议结束之后，交易双方都得到相应的证据，或交易双方都没得到相应的证据，即不会出现交易双方中只有一方得到证据的情况。对于一个无法保证公平性的非抵赖协议，其结果可能会使仲裁有失公正，因此一个有效的非抵赖协议必须保证公平性。　　 现有的非抵赖协议分为两种，一种为无可信第三方TTP(TrustedThirdParty)参与的非抵赖协议，另一种为有可信第三方参与的协议。无可信第三方参与的非抵赖协议中，绝大多数情况下无法保证其公平性，而能保证公平性的非抵赖协议要求又极为苛刻，例如要求发送方和接收方的计算能力相同。基于可信第三方的非抵赖协议需要选择一个权威、中立、可信任的第三方节点或组织作为TTP来实现证据交换，才能保证公平性。但是固定的可信第三方存在不少缺点。第一，由于移动自组网Manet具有无中心节点和所有节点不可信任的特性，无法采用集中提供服务的TTP;第二，可信第三方也难以保证绝对的安全，一旦可信第三方崩溃或被攻破，都会带来难以预估的损失，同时由于每次协议的运行都需要交易双方与可信第三方通信，易造成传输的瓶颈，最后，固定的可信第三方维护代价也较大。　　 为此，本文对移动自组网下的公平非抵赖协议进行研究，研究内容如下：　　 首先，在可信平台模块TPM(TrustedPlatformModule)的安全体系结构基础上提出了一种适用于移动自组网、无需可信第三方的可信公平非抵赖协议。协议使用动态第三方取代固定的可信第三方，同时使用TPM完整性度量技术和DAA(DirectAnonymousAttestation)远程认证技术，保证动态第三方的可信。针对移动自组网Manet的无中心节点和所有节点不可信任的特点，新协议使用随机选取的动态第三方，同时使用可信计算技术保证动态第三方的可信，使其代替传统的固定可信第三方完成信息交换。　　 然后，使用形式化工具EventB对提出协议的公平性和证据的有效性进行分析证明。公平非抵赖协议对安全性的要求极高，因此必须对其进行安全性进行分析。本文使用形式化方法对新协议进行形式化建模并在模型中添加其安全需求，然后对其自动生成的证明义务进行证明，以保证新协议的安全性。