摘要： 分析了网络编码系统DCAR“编码+路由”发现过程存在的安全问题，提出了适用于编码感知安全路由协议的安全目标，设计了基于DCAR的编码感知安全路由协议DCASR，DCASR协议利用密码学机制保证可信路由建立和正确编码机会发现。为建模多跳无线网络特征和分析路由协议安全性，引入线程位置和线程位置相邻概念，扩展安全系统逻辑LS2，提出了分析路由协议安全性的逻辑LS2-RP。LS2-RP用线程邻居集及邻居集的变化描述多跳无线网络的动态拓扑关系，用广播规则模型化多跳无线网络广播通信特征。最后，用LS2-RP协议编程语言描述了DCASR协议，用LS2-RP的谓词公式和模态公式描述DCASR协议的安全属性，用LS2-RP逻辑证明系统分析了DCASR协议的安全性，证明DCASR协议能够满足安全目标。