移动自组网中无需可信第三方的可信认证协议研究

Mobile Ad Hoc Networks (MANET) is a non-central network with mobile nodes of non-trustworthy. As traditional security authentication scheme required Trusted Third Party (TTP) as authentication server, it is not sufficient to guarentee efficiency and safety in MANET. This subject is based on Trusted Platform Module (TPM) security architecture, and is to study the trusted authentication protocols without TTP. We also study the formal modeling, proof, verification, asssessment techiniques to ensure the trustworthiness. That is, we study the formal modeling and proof techniques of trusted authentication protocols based on Event B, the formal verification of the protocols based on Pi calculus, the dynamic assessment techniques based on association rules, and finally the trusted authentication procotols based on TELSA broadcasting for verifying safety of the previous formal techniques. The purpose of this subject is to build the trusted authentication protocols without TTP for avoiding the TTP efficiency bottlenecks, and formal methods to ensure the safety of trusted protocols in MANET, to further promote the research and development of Trusted Computing in China.

由于移动自组网(MANET)是一个无中心的网络且不存在任何一个值得信任的移动节点，传统的安全认证方案因需要一个可信第三方(TTP)来提供认证服务而不足以保证MANET的高效性和安全性。本课题拟在可信平台模块(TPM)安全体系结构基础上提出一个无需TTP的可信认证协议，并研究该协议的形式化建模、证明、验证、评估技术以保证其可信性。即研究基于Event B的的可信认证协议形式化建模与证明技术；研究基于Pi演算的可信认证协议形式化验证技术；研究基于关联规则的可信认证协议动态评估技术；研究基于TELSA广播的可信认证协议以验证其安全性。本课题的目的就是为MANET提供一个无需TTP的可信认证协议，避免TTP带来的效率瓶颈问题，保证协议高效运行，并通过形式化方法完善协议软件，确保可信认证协议安全运行，为MANET中各种应用软件提供可信保障，进一步推动我国可信计算的研究和发展。

由于移动自组网(MANET)是一个无中心的网络且不存在任何一个值得信任的移动节点，传统的安全认证方案因需要一个可信第三方(TTP)来提供认证服务而不足以保证MANET的高效性和安全性。本课题在可信平台模块(TPM)安全体系结构基础上提出一个无需TTP的可信认证协议，并研究该协议的形式化建模、证明、验证、评估技术以保证其可信性。即研究基于Event B的的可信认证协议形式化建模与证明技术；研究基于Pi演算的可信认证协议形式化验证技术；研究基于关联规则的可信认证协议动态评估技术；研究基于TELSA广播的可信认证协议以验证其安全性。本课题的目的就是为MANET提供一个无需TTP的可信认证协议，避免TTP带来的效率瓶颈问题，保证协议高效运行，并通过形式化方法完善协议软件，确保可信认证协议安全运行，为MANET中各种应用软件提供可信保障，进一步推动我国可信计算的研究和发展。我们的进展如下：.1）基于信誉模型的移动无线网络密钥管理方案.我们设计基于信誉模型的密钥管理方案。在该方案中，密钥的建立和更新是建立在信任基础上自组织式的，不仅提高了密钥的安全性，而且有效抵制了内部节点的恶意行为，从而提高了网络的抗毁性。支持密钥的动态管理使新节点的加入操作变得相对简单，不仅使方案具有良好的分布性和可扩展性，更节约了计算时间和资源，提高了方案的可行性。.2）基于模糊数学的MANET恶意节点识别.我们主要针对MANET中从路由层发起攻击的内部恶意节点，分析节点通信行为，确定内部恶意节点的属性，并建立由多个属性组成的属性向量，采用模糊数学理论进行恶意节点识别。分析节点通信行为，提取节点的包转发延迟、转发率和丢包率3个属性，在对属性建模的基础上，通过最大隶属度原则识别恶意节点。.3）针对基于TPM的安全协议的细粒度分析.可信赖平台模块(TPM)可以提供平台完整性检查和为远程实体进行完整性认证，但是现在并没有针对基于TPM的安全协议的形式化框架。我们针对Event-B语言的IDE生成的约束进行了证明。基于此，我们可以使用Event-B语言对基于TPM的安全协议做更细粒度的分析。.基于本项目已发表文章17篇，其中SCI期刊8篇，国际会议6篇，CCF A类论文3篇，B类论文3篇，申请发明专利6项，完成预期研究计划。