Skip to main content

Formal Reasoning About a Specification-Based Intrusion Detection for Dynamic Auto-configuration Protocols in Ad Hoc Networks

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 3866))

Abstract

As mobile ad hoc networks (MANETs) are increasingly deployed in critical environments, security becomes a paramount issue. The dynamic and decentralized nature of MANETs makes their protocols very vulnerable to attacks, for example, by malicious insiders, who can cause packets to be misrouted or cause other nodes to have improper configuration. This paper addresses security issues of auto-configuration protocols in ad hoc networks. Auto-configuration protocols enable nodes to obtain configuration information (e.g., an IP address) so that they can communicate with other nodes in the network. We describe a formal approach to modeling and reasoning about auto-configuration protocols to support the detection of malicious insider nodes. With respect to this family of protocols, our approach defines a global security requirement for a network that characterizes the "good" behavior of individual nodes to assure the global property. This behavior becomes local detection rules that define a distributed specification-based intrusion detection system aimed at detecting malicious insider nodes. We formally prove that the local detection rules (identifying activity that is monitored) together with “assumptions” that identify system properties which are not monitored imply the global security requirement. This approach, novel to the field of intrusion detection, can, in principle, yield an intrusion detection system that detects any attack, even unknown attacks, that can imperil the global security requirement.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anderson, J.P.: Computer security threat monitoring and surveilance, Technical report, James P. Anderson Co., Fort Washington, PA (April 1980)

    Google Scholar 

  2. Bishop, M.A.: Computer Security: Art and Science. Addison Wesley Longman, Amsterdam (2002)

    Google Scholar 

  3. Budkowski, S., Dembinski, P.: An Introduction to Estelle: A specification language for distributed systems. Computer Networks and ISDN Systems 14(1), 3–24 (1991)

    Article  Google Scholar 

  4. Brock, B., Kaufmann, M., Moore, J.: ACL2 Theorems about Commercial Microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 275–293. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  5. Boyer, R.S., Moore, J.S.: A computational logic. Academic Press, New York (1979)

    MATH  Google Scholar 

  6. Huang, Y., Lee, W.: Attack Analysis and Detection for Ad Hoc Routing Protocols. In: Jonsson, E., Valdes, A., Almgren, M. (eds.) RAID 2004. LNCS, vol. 3224, pp. 125–145. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Ilgun, K., Kemmerer, R., Porras, P.: State Transition Analysis: A Rule-based Intrusion Detection Approach. IEEE Transactions of Software Engineering 13, 181–199 (1995)

    Article  Google Scholar 

  8. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)

    Google Scholar 

  9. Ko, C., Brutch, P., Rowe, J., Tsafnat, G., Levitt, K.N.: System Health and Intrusion Monitoring Using a Hierarchy of Constraints. In: Lee, W., Mé, L., Wespi, A. (eds.) RAID 2001. LNCS, vol. 2212, p. 190. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. Ko, C., Ruschitzka, M., Levitt, K.: Execution Monitoring of Security-Critical Programs in Distributed Systems: A Specification-based Approach. In: Proceedings of the 1997 IEEE Symposium on Security and Privacy (May 1997)

    Google Scholar 

  11. McAuley, A.J., Manousakis, K.: Self-Configuring Networks. In: IEEE Milcom 2000, Los Angeles (October 2000)

    Google Scholar 

  12. Moore, J.: Proving Theorems about Java-like Byte Code. In: Correct System Design - Issues, Methods and Perspectives (1999)

    Google Scholar 

  13. Roesch, M.: Snort: Lightweight Intrusion Detection for Networks. In: Proc. Of USENIX LISA 1999, Seattle, Washington, November, pp. 229–238 (1999)

    Google Scholar 

  14. Song, T., Alves-Foss, J., Ko, C., Zhang, C., Levitt, K.: Using ACL2 to Verify Security Properties of Specification-based Intrusion Detection Systems. In: Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (2003)

    Google Scholar 

  15. Sterne, D., Balasubramanyam, P., Carman, D., Wilson, B., Talpade, R., Ko, C., Balupari, R., Tseng, C.-Y., Bowen, T., Levitt, K., Rowe, J.: A General Cooperative Intrusion Detection Architecture for MANETs. In: Proceedings of the 3rd IEEE International Workshop on Information Assurance (March 2005)

    Google Scholar 

  16. Song, T., Ko, C., Alves-Foss, J., Zhang, C., Levitt, K.: Formal Reasoning about Intrusion Detection Systems. In: Jonsson, E., Valdes, A., Almgren, M. (eds.) RAID 2004. LNCS, vol. 3224, pp. 278–295. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Subhadrabandhu, D., Sarkar, S., Anjum, F.: Efficacy of Misuse Detection in Adhoc Networks. In: proceeding of IEEE Communications Society Conference on Sensor and Ad Hoc Communications and Networks (2004)

    Google Scholar 

  18. Tseng, C.Y., Balasubramanyam, P., Ko, C., Limprasittiporn, R., Rowe, J., Levitt, K.: A Specification-Based Instrusion Detection system for AODV. In: 2003 ACM Workshop on security of Ad Hoc and Sensor Networks (SASN 2003), (October 21, 2003)

    Google Scholar 

  19. Tseng, C.H., Song, T., Balasubramanyam, P., Ko, C., Levitt, K.: A Specification-based Intrusion Detection Model for OLSR. In: Valdes, A., Zamboni, D. (eds.) RAID 2005. LNCS, vol. 3858, pp. 330–350. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Vaidyanathan, R., Kant, L., McAuley, A., Bereschinsky, M.: Performance Modeling and Simulation of Dynamic and Rapid Auto-configuration Protocols for Ad-hoc Wireless Networks. In: proceeding of Annual Simulation Symposium 2003 (2003)

    Google Scholar 

  21. Zhou, L., Haas, Z.J.: Securing ad hoc networks. IEEE Network Magazine 13(6) (November,December 1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Song, T., Ko, C., Tseng, C.H., Balasubramanyam, P., Chaudhary, A., Levitt, K.N. (2006). Formal Reasoning About a Specification-Based Intrusion Detection for Dynamic Auto-configuration Protocols in Ad Hoc Networks. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds) Formal Aspects in Security and Trust. FAST 2005. Lecture Notes in Computer Science, vol 3866. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11679219_3

Download citation

  • DOI: https://doi.org/10.1007/11679219_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-32628-1

  • Online ISBN: 978-3-540-32629-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics