MANET安全路由协议自动化分析

doi:10.3969/j.issn.1001-2400.2016.06.010

西安电子科技大学学报

MANET安全路由协议自动化分析

毛立强1;黄影2

(1. 西安电子科技大学计算机学院，陕西西安 710071;
2. 西安文理学院数学与计算机工程学院，陕西西安 710068)

收稿日期:2014-09-28 出版日期:2016-12-20 发布日期:2017-01-19
作者简介:毛立强(1978-)，男，高级工程师，博士，E-mail: lqmao@xidian.edu.cn．
基金资助:
国家自然科学基金重点资助项目(U1135002)

Automated security analysis techniques in MANET routing protocols

MAO Liqiang1;HUANG Ying2

(1. School of Computer Science and Technology, Xidian Univ., Xi'an 710071, China;
2. School of Mathematics and Computer Engineering, Xi'an Univ. of Arts and Science, Xi'an 710068, China)

Received:2014-09-28 Online:2016-12-20 Published:2017-01-19

摘要/Abstract

摘要：

移动ad hoc网络安全路由协议已经成为一个热门的研究领域，其中协议的安全性分析方法及其自动化实现倍受关注．利用SPIN工具自动分析了SRP和Ariadne协议，首先通过网络拓扑建模和自动生成，可以全面分析在不同网络拓扑下协议的安全性．再通过节点丢弃攻击和协议建模，自动发现了针对协议的有效攻击，证明基于模型检测及SPIN工具自动分析安全路由协议的方法是有效的．

关键词: 路由协议, 形式化分析, SPIN, 模拟模型

Abstract:

Automated security analysis techniques in Mobile ad hoc network(MANET) routing protocols has become a hot research field. We have developed an automated evaluation process to analyze security properties of SRP and Ariadne. Using the automated security evaluation process, we can produce and analyze all topologies for a given network size. The NDA attackers and routing protocols are modeled in SPIN, and the route corruption attack is found automatically, which indicates the effectiveness of automated analysis of MANET route protocols using SPIN.

Key words: routing protocol, formal analysis, simple promela interpreter, simulatability model

毛立强;黄影. MANET安全路由协议自动化分析[J]. 西安电子科技大学学报, 2016, 43(6): 56-61.

MAO Liqiang;HUANG Ying. Automated security analysis techniques in MANET routing protocols[J]. Journal of Xidian University, 2016, 43(6): 56-61.

参考文献

［1］ SHARMA S B, CHAUHAN N. Security Issues and Their Solutions in MANET［C］//Proceedings of the 2015 1st International Conference on Futuristic Trends in Computational Analysis and Knowledge Management. Piscataway: IEEE, 2015: 289-294.
［2］ NANZ S, HANKIN C. A Framework for Security Analysis of Mobile Wireless Networks ［J］. Theoretical Computer Science, 2006, 367(1/2): 203-227.
［3］ THONG T V, BUTTYAN L. On Automating the Verification of Secure Ad-hoc Network Routing Protocols［J］. Telecommunication Systems, 2013, 52(4): 2611-2635.
［4］ PURA M L, BUCHS D. Model Checking ARAN Ad Hoc Secure Routing Protocol with Algebraic Petri Nets［C］//Proceedings of the 10th IEEE International Conference on Communications. Piscataway: IEEE, 2014: 1-4.
［5］ BENETTI D, MERRO M, VIGANO L. Model Checking Ad Hoc Network Routing Protocols: ARAN vs Endair A［C］//Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods. Piscataway: IEEE, 2010: 191-202.
［6］ PURA M L, PATRICIU V V, BICA I. Formal Verification of Secure Ad Hoc Routing Protocols Using AVISPA: ARAN Case Study［C］//Proceedings of the 4th Conference on European Computing Conference. Athens: World Scientific and Engineering Academy and Society, 2010: 200-206.
［7］ WIBLING O, PARROW J, PEARS A. Automatized Verification of Ad Hoc Routing Protocols［C］//Lecture Notes in Computer Science: 3235. Berlin: Springer Verlag, 2004: 343-358.
［8］ ZAIDI F, LALLALI M, MAAG S. A Component Based Testing Technique for a MANET Routing Protocol［C］//Proceedings of the ACS/IEEE International Conference on Computer Systems and Applications. Piscataway: IEEE Computer Society, 2010: 5587040.
［9］ ACS G, BUTTYAN L, VAJDA I. Provably Secure On-demand Source Routing in Mobile Ad Hoc Networks ［J］. IEEE Transactions on Mobile Computing, 2006, 5(11): 1533-1546.
［10］ CORTIER V, DEGRIECK J, DELAUNE S. Analysing Routing Protocols: Four Nodes Topologies Are Sufficient［C］//Lecture Notes in Computer Science: 7215. Berlin: Springer Verlag, 2012: 30-50.

[1]	底琳佳;戴显英;苗东铭;吴淑静;郝跃. 单轴应变锗带隙特性和电子有效质量计算[J]. 西安电子科技大学学报, 2018, 45(3): 24-29.
[2]	杨元原;马文平;刘维博;俞优;顾健. 带有异或运算安全协议的自动化检测[J]. J4, 2012, 39(4): 120-125+183.
[3]	李桢;陈健;阔永红. WSN中六边形集中式分簇多跳路由协议[J]. J4, 2012, 39(3): 20-26.
[4]	唐迪;杨小牛;李建东. 一种具有概率预测机制的无线传感器网络安全路由协议[J]. J4, 2011, 38(6): 1-7.
[5]	毛立强1;马建峰1;2. 可证明安全的MANET按需距离矢量路由协议分析 [J]. J4, 2008, 35(6): 1063-1068.
[6]	徐瑞;李伟华;陈华胜. 基于树的按需Ad Hoc组播路由协议性能比较和分析 [J]. J4, 2007, 34(4): 664-668.
[7]	慕建君. 一种形式化分析安全协议的新模型[J]. J4, 2006, 33(3): 381-385.
[8]	王炫;李建东;李峰. 增强型RIEMS协议及其在Ad Hoc网络中的性能[J]. J4, 2006, 33(2): 241-246.
[9]	张文柱;李建东;王炫. 多跳分布式无线网络中不同路由协议的性能[J]. J4, 2003, 30(4): 458-463.
[10]	杜欣军;葛建华;王莹. 一种增强AODV路由协议安全性的方案[J]. J4, 2002, 29(6): 819-822.

MANET安全路由协议自动化分析

Automated security analysis techniques in MANET routing protocols

PDF (PC)

赞

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 10

Metrics

本文评价

推荐阅读 10