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

安全路由协议的基础理论探索和相关的安全设计和分析方法是可信网络研究领域的重要内容之一。本项目以无线通信网络路由协议为研究对象，融合可证明安全设计方法与符号操作的协议分析方法, 针对安全路由协议问题定义基于复杂性理论的语义，提出一种实际有效的无线网络路由协议自动化安全分析方法。主要研究无线路由协议的安全标准；利用Dolev-Yao 模型和安全多方计算理论确定路由协议的自适应威胁模型；引入通用可复合UC模型的密码协议安全定义框架，建立路由协议的形式化安全定义及可证明安全设计方法；利用计算PCL理论证明系统简化路由协议安全性的推理规则，开发一个自动化的拓扑发生器，分析检查给定网络规模N的所有可能的网络拓扑，设计基于PCL的安全协议自动化验证工具。通过研究，我们希望在安全路由协议的形式化理论和方法上有一定的突破，为高效、可靠和可证安全的路由协议设计和安全分析提供比较完整和系统的理论支持和技术支撑。

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