移动AdHoc网络(Mobile Ad Hoc Networks，MANETs)是一种无基础设施的多跳无线网络，网络节点既是主机又是路由器，只有依赖网络中所有可信节点协作，安全路由协议才能获得可信路径信息，而这种“依赖”需借助密码学安全协议实现。然而，在分析路由协议安全性时，与分析密码学安全协议安全性不同，必需考虑构成路径的网络中间节点行为。因此，用于密码学安全协议的形式化分析技术不能直接用于安全路由协议的安全分析，设计分析安全路由协议的新方法具有重要的理论和应用价值。　　 目前广泛使用的针对密码学安全协议的形式化分析模型可分为两大类：计算模型和符号模型。本论文针对移动AdHoc网络路由协议安全分析的特殊性，基于两种流行的密码学安全协议安全分析技术一通用可复合UC(Universally Composable)安全计算模型和协议复合逻辑PCL(Protocol Compisition Logic)符号模型，研究了以下几个方面的内容：　　 第一，路由安全威胁模型的研究。本论文分析了现有路由安全威胁模型active-n-m攻击模型、参数化威胁模型、自适应威胁模型等存在的问题，基于Dolev-Yao攻击模型并综合现有威胁模型的特点，提出了更加适合于建模路由安全威胁的层次化威胁模型。　　 第二，基于UC安全理论的路由安全分析技术研究。针对多路径距离矢量路由安全分析问题，基于层次化威胁模型和攻陷网络拓扑模型，提出了多路径距离矢量路由协议安全需求.可信系统状态概念，并给出了多路径距离矢量路由协议理想函数及安全定义，对基于UC安全理论的路由安全分析模型UC-RP(UC for Routing Protocol)模型作了进一步的补充和完善。　　 第三，基于PCL的路由安全分析技术研究。PCL是一种用于分析密码学安全协议，如认证协议、密钥协商协议等的符号模型。本论文引入线程位置和线程位置相邻概念，扩展PCL提出了建模移动AdHoc网络和分析路由协议安全性的符号模型PCL-RP(PCL for Routing Protocol)模型。PCL-RP模型把移动AdHoc网络模型化为不同逻辑位置上运行的线程复合，用线程邻居集及邻居集的变化描述多跳无线网络的动态拓扑关系，用广播规则模型化多跳无线网络广播通信特征，用符号迹概念模型化路由协议执行过程，提出网络迹概念模型化符号迹上事件导致的网络进化过程，在网络迹上定义了PCL-RP模型中谓词公式和模态公式的语义，提出了路由协议安全分析的新方法。　　 第四，路由协议通用可复合符号分析技术研究。PCL-RP模型协议符号分析比UC-RP模型协议分析简单、直观并且易于实现自动化分析。然而，PCL-RP模型中的符号分析缺乏计算可靠性。借鉴密码学安全协议计算可靠性符号分析的最新研究成果，本论文融合UC-RP模型和PCL-RP模型，提出了路由协议通用可复合符号分析模型UCSA-RP(Universally Composable Symbol Analysis for Routing Protocol)模型，在UCSA-RP模型中说明了如何用PCL-RP模型的符号分析方法断言UC-RP模型中的协议安全性。　　 第五，多路径安全路由协议的设计与分析技术研究。AMR(Aggregate Multi-paths Routing)算法是计算节点不相交多路径路由的累积多路径路由机制，本论文整合AMR算法和单路径距离矢量路由协议AODV协议，引入密码学安全机制、错误检测机制和路径确认机制，设计了节点不相交多路径距离矢量安全路由协议SMDVR(Secure Multi-paths Distance Vector Routing)，并在UC-RP模型中分析了SMDVR协议的安全性，SMDVR协议的可证明安全性能够归约为签名机制的安全性。另外，对SMDVR协议与相关协议方案的效率作了比较分析。　　 第六，编码感知安全路由协议的设计与分析技术研究。本论文研究了全局网络编码系统DCAR(Distributed Code-Aware Routing)存在的问题，提出了适合于编码感知安全路由协议的安全目标，基于DCAR，设计了编码感知安全路由协议DCASR(Distributed Code-Aware Secure Routing)，并在PCL-RP模型中建模并分析了DCASR协议的安全属性，证明新协议能够满足本论文提出的安全目标。在UCSA-RP模型中证明PCL-RP模型中DCASR协议的符号安全准则蕴含UC-RP模型中的计算安全定义，说明了DCASR协议的计算可靠性。