摘要
提出了Ad-hoc网络虚假路由攻击的形式化验证和分析方法,主要是在参数化Ad-hoc路由协议串空间模型的基础上采用改进的Athena状态表示法来描述问题域,并采用相应的证明搜索过程来完成目标验证。最后设计实现了虚假路由自动验证系统FRpoofor,用它验证和分析了Ariadne安全路由协议运行环境下某些虚假路由的建立过程,以此说明方法的有效性。
It is a general threaten for MANET routing protocol to create the false routes,so analysis of this threaten is an important goal of routing security research.We proposed an approach to formal verification for the false route in MANET.It allows us to represent the basic objective to be proven with the state representation based on our parameterized strand space model of the Ad-hoc routing protocol,and to apply the adapted proof search procedure to automatically verify the basic objective.At last we completed the automatic verification program,called FRpoofor.As a example,we executed FRpoofor to verify and analyze some false route in secure routing protocol Ariadne.
出处
《计算机科学》
CSCD
北大核心
2012年第2期118-121,共4页
Computer Science
