移动自组网无需可信第三方的可信公平非抵赖协议研究

由于移动自组网Manet中所有结点的不可信性，传统的信息安全机制和方法因需要一个集中提供非抵赖服务的可信第三方TTP而无法完全保证Manet的安全性和可靠性。本课题拟在可信平台模块TPM的安全体系结构基础上提出一个无需TTP的可信非抵赖协议，并研究该协议及软件的形式化建模、证明、评估、检测与验证技术以保证其可信性即研究基于Pi演算的可信公平非抵赖协议形式化建模和验证技术；研究基于高阶逻辑的可信公平非抵赖协议软件的形式化建模与证明技术；研究基于数据挖掘的可信公平非抵赖协议的动态评估技术；研究基于模型检测的可信公平非抵赖协议软件的形式化检测技术；研究Manet中无需可信第三方的可信公平非抵赖协议软件以验证其安全可靠性。本课题的目的就是为Manet提供一个无需TTP的可信公平非抵赖协议软件以便彻底抛弃TTP，克服现有无需TTP公平非抵赖协议的概率公平缺点，进一步推动国内可信移动计算的研究和发展。

移动自组网 Manet(Mobile Ad-hoc Networks)是由若干带有无线收发器的移动节点所组成的无基站的自治网络，广泛应用于军事、民用、商业等领域。为保证其安全性,在交易结束后,交易双方都应得到相应的证据,在出现争议时,仲裁方便能依据双方提供的证据进行仲裁,为此人们提出了公平非抵赖协议。.传统的公平非抵赖协议大多基于可信第三方TTP(Trusted Third Party),选择一个权威、中立、可信任的第三方节点或组织作为TTP 来实现证据交换。但是, 由于Manet的无中心性及拓扑的动态性, 传统TTP因采用集中服务会带来协议的效率瓶颈,同时TTP的崩溃将导致网络中所有节点都无法得到公平非抵赖服务。于是,无需TTP的公平非抵赖协议成为研究的重点。.我们的项目有以下贡献：.(1).提出针对TPM可信认证协议软件的形式化建模、精化与证明方法。由于TPM体系中，普遍认为TPM是可信的，这样我们需要假设TPM外的软件平台是不可信的。针对这个问题，我们对传统的敌方模型进行了修改，提出新的安全模型。在新的安全模型中，我们提出额外假设：未被TPM进行完整性验证平台是可能遭遇敌方的攻击的。进一步，我们使用Event-B精化语言，进行逐层精化；.(2).基于TPM及虚拟化技术的最小化可信基系统。由于部分程序涉及到用户的隐私、机密数据，需要保证这些安全敏感程序（Security-sensitive Application）代码和数据的安全。我们提出一个新的架构，使用较小的最小可信基(Trusted Computing Base, TCB)，实现安全敏感程序在不可信操作系统中的安全执行，并且安全敏感程序拥有和传统程序一样的操作系统服务。.(3).针对可信计算架构中遮蔽技术的形式化证明框架。为了保护安全敏感程序不受这些来自主机系统的威胁，通常会在主机系统之下增加遮蔽系统，对安全敏感程序进行保护。之前的针对遮蔽系统的形式化方法仅考虑了一个防护机制的作用在一个形式化工作中。基于这个动机，我们提出了一个综合性的形式化框架来分析遮蔽系统是否给安全敏感程序提供了足够的安全保证。.基于本项目已发表文章31篇，其中SCI期刊15篇，国际会议7篇，CCF A类论文3篇，B类论文3篇，申请发明专利8项，完成预期研究计划。