无线网络路由协议的可证安全设计与自动化安全分析方法研究

本项目主要以无线通信网络路由协议为研究对象，融合计算复杂性理论与符号操作理论的安全协议设计与分析方法, 针对无线网络安全路由协议设计和分析方法面临的问题，建立了实际有效的无线网络路由协议安全评价体系并验证了安全评价体系对无线网络安全路由协议设计和分析的指导性。在该安全评价体系中，主要研究了以下内容：(1)建立了无线网络拓扑特征的形式化描述方法，分析了路由发现阶段和数据转发阶段存在的攻击类型，基于Dolev-Yao模型和安全多方计算理论，提出了路由安全层次化威胁模型和预防路由完整性攻击的多个密码学安全机制；(2)引入通用可复合UC安全框架模型，建立了路由协议的形式化安全定义，提出了基于UC安全模型的可证明安全路由协议的新方法，应用于无线通信网络路由协议的安全设计和分析；(3)基于协议复合逻辑PCL证明系统，简化了路由协议安全性的推理规则，建立了路由安全分析的符号操作模型，设计了基于PCL的安全协议自动化验证方法。融合路由协议可证明安全设计方法与符号操作的协议分析方法，证明了符号分析方法能够解释路由协议基于复杂性理论的分析方法。