Abstract
Evaluation techniques to analyze security properties in ad hoc routing protocols generally rely on manual, non-exhaustive approaches. Non-exhaustive analysis techniques may conclude a protocol is secure, while in reality the protocol may contain an unapparent or subtle flaw. Using formalized exhaustive evaluation techniques to analyze security properties increases protocol confidence. In this paper, we offer an automated evaluation process to analyze security properties in the route discovery phase for on-demand source routing protocols. Using our automated security evaluation process, we are able to produce and analyze all topologies for a given network size. The individual network topologies are fed into the SPIN model checker to exhaustively evaluate protocol abstractions against an attacker attempting to corrupt the route discovery process.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Royer, E.M., Toh, C.-K.: A review of current routing protocols for ad hoc mobile wireless networks. IEEE Personal Communications 6, 46–55 (1999)
Hu, Y.C., Perrig, A.: A survey of secure wireless ad hoc routing. IEEE Security & Privacy 2, 28–39 (2004)
Argyroudis, P.G., O’Mahony, D.: Secure routing for mobile ad hoc networks. IEEE Communications Surveys & Tutorials 7, 2–21 (2005)
Djenouri, D., Khelladi, L., Badache, A.N.: A survey of security issues in mobile ad hoc and sensor networks. IEEE Communications Surveys & Tutorials 7, 2–28 (2005)
Andel, T.R., Yasinsac, A.: Surveying Security Analysis Techniques in MANET Routing Protocols. IEEE Communications Surveys & Tutorials 9, 70–84 (2007)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23, 279–295 (1997)
De Renesse, F., Aghvami, A.H.: Formal verification of ad-hoc routing protocols using SPIN model checker. In: 12th IEEE Mediterranean Electrotechnical Conference, vol. 3, pp. 1177–1182 (2004)
Wibling, O., Parrow, J., Pears, A.: Automatized Verification of Ad Hoc Routing Protocols. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 343–358. Springer, Heidelberg (2004)
Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. Journal of the ACM 49, 538–576 (2002)
Andel, T.R., Yasinsac, A.: Automated Security Analysis of Ad Hoc Routing Protocols Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA 2007), Wroclaw, Poland, pp. 9–26 (2007)
Hu, Y.-C., Perrig, A., Johnson, D.B.: Ariadne: A Secure On-Demand Routing Protocol for Ad Hoc Networks. Wireless Networks 11, 21–38 (2005)
Ács, G., Buttyán, L., Vajda, I.: Provably secure on-demand source routing in mobile ad hoc networks. IEEE Transactions on Mobile Computing 5, 1533–1546 (2006)
Ryan, P., Schneider, S.: Modelling and Analysis of Security Protocols. Addison-Wesley, Harlow (2001)
Burmester, M., Van Le, T.: Secure multipath communication in mobile ad hoc networks. In: International Conference on Information Technology: Coding and Computing (ITCC 2004), vol. 2, pp. 405–409 (2004)
Kotzanikolaou, P., Mavropodi, R., Douligeris, C.: Secure Multipath Routing for Mobile Ad Hoc Networks. In: Second Annual Conference on Wireless On-demand Network Systems and Services (WONS 2005), pp. 89–96 (2005)
Awerbuch, B., Holmer, D., Nita-Rotaru, C., Rubens, H.: An on-demand secure routing protocol resilient to byzantine failures. In: 3rd ACM Workshop on Wireless Security, pp. 21–30. ACM Press, Atlanta (2002)
Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Computing Surveys 28, 626–643 (1996)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Meadows, C.: The NRL Protocol Analyzer: An Overview. The Journal of Logic Programming 26, 113–131 (1996)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Song, D., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9, 47–74 (2001)
Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theoretical Computer Science 367, 203–227 (2006)
Yang, S., Baras, J.S.: Modeling vulnerabilities of ad hoc routing protocols. In: 1st ACM Workshop on Security of Ad hoc and Sensor Networks, pp. 12–20 (2003)
Maggi, P., Sisto, R.: Using SPIN to Verify Security Properties of Cryptographic Protocols. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 187–204. Springer, Heidelberg (2002)
Ruys, T.C.: Towards effective model checking. Department of Computer Science. University of Twente, Deventer, The Netherlands (2001)
Andel, T.R., Yasinsac, A.: The Invisible Node Attack Revisited, pp. 686–691. IEEE SoutheastCon, Richmond (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andel, T.R., Yasinsac, A. (2008). Automated Evaluation of Secure Route Discovery in MANET Protocols. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)