可证明安全的MANET按需源路由协议分析.doc

·· 通信学报 第30卷
第1期 毛立强等：可证明安全的MANET按需源路由协议分析 ··

第30卷第1期 通信学报 Vol.30No.1
2009年1月 JournalonCommunications January2009

可证明安全的MANET按需源路由协议分析
毛立强1，马建峰1,2，李兴华1
（1.西安电子科技大学计算机学院，陕西西安710071；2.计算机网络与信息安全教育部重点实验室，陕西西安710071）
摘要：对MANET安全按需源路由协议的一种形式化分析模型进行了深入分析，指出其中存在的合并相邻敌手节点等不合理操作以及该模型下endairA协议安全性证明过程中的错误，并给出了一种针对endairA协议的隐蔽信道攻击，表明该协议即使在其安全分析模型下也不能满足其安全目标。
关键词：路由协议；可证明安全；形式化分析；模拟；隐蔽信道攻击
中图分类号：TP393.04文献标识码：A文章编号：1000-436X(2009)01-0038-07
Analysisofprovablysecureon-demandsourceroutinginMANET
MAOLi-qiang1,MAJian-feng1,2,LIXing-hua1
(1.SchoolofComputerScience&Technology,XidianUniversity,Xi’an710071,China;2.KeyLaboratoryofComputerNetworks&InformationSecurity,MinistryofEducation,Xi’an710071,China)
Abstract:Aformalmodeltailoredtothesecurityanalysisofon-demandsourceroutingprotocolsinMANETwasanalyzed,andtheimpropermanipulationssuchasmergenceoftheadjacentadversarialnodesinthemodelandtheflawintheproofforendairAwereindicated.AnewhiddenchannelattacktoendairAwaspresented,whichshowsthatendairAisnotprovablysecureevenintheirmodel.
Keywords:routingprotocol;provablesecurity;formalanalysis;simulationparadigm;hiddenchannelattack

1引言
收稿日期：2008-06-02；修回日期：2008-10-21
基金项目：国家高技术研究发展计划（“863”计划）基金资助项目（2007AA01Z429,2007AA01Z405）；国家自然科学基金重点资助项目（60633020）；国家自然科学基金资助项目（60573036,60702059,60503012,60803150）
FoundationItems:TheNationalHighTechnologyResearchandDevelopmentProgramofChina(863Program)(2007AA01Z429,2007AA01Z405);TheKeyProgramofNationalNaturalScienceFoundationofChina(60633020);TheNationalNaturalScienceFoundationofChina(60573036,60702059,60503012,60803150)

移动adhoc网络(MANET，mobileadhocnetworks)是一种不依赖于固定基础设施的自组织无线网络，其组网快捷、方便，不受时间和空间的限制，在救灾保障、作战指挥、会务通信、实施远距离或危险环境中的监控等场合具有广阔的应用前景。当前，移动adhoc网络已经成为一个热门的研究领域，与之相关的安全技术也得到了广泛关注，安全路由协议的设计与分析即是其中之一。目前，已经提出多种安全路由协议[1]，大多都是在原有路由协议上附加安全机制。其中，基于按需源路由协议DSR[2]的安全路由协议倍受关注。
目前大部分安全路由协议分析都是基于主观分析或者模拟仿真等非形式化方法，缺乏精确严格的分析过程，导致很多原来声称“安全”的路由协议后来都被发现存在安全漏洞。近年来有学者开始进行安全路由协议形式化分析方法的尝试。SRP的作者试图用BAN逻辑分析SRP的安全性[3]，但BAN逻辑假设参与协议的主体都是可信的，而路由源节点S和目标节点T依赖中间节点建立安