Skip to main content
SpringerLink
Log in

Formal Model for (k)-Neighborhood Discovery Protocols

  • Chapter
  • First Online:
Advances in Network Analysis and its Applications

Part of the book series: Mathematics in Industry ((MATHINDUSTRY,volume 18))

  • 1720 Accesses

Abstract

Neighborhood discovery is a critical part of wireless sensor networks, yet little work has been done on formal verification of the protocols in presence of both intruder nodes and mobility. We present a formal trace-based model to verify protocols doing neighborhood discovery, and we provide a formal definition of (1)-neighborhood and (k)-neighborhood. We also analyze a protocol from the literature, and show some conditions needed for its correctness. Finally, we present the groundwork for a protocol which discovers (k)-neighborhood based on (1)-neighborhood data under some assumptions, and prove that it remains secure even if an intruder interferes.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Institutional subscriptions

Notes

  1. 1.

    We remark that is not the case for the authentication which is a property based on exchanged messages.

References

  1. Ross J. Anderson. Security Engineering: A Guide to Building Dependable Distributed Systems. John Wiley & Sons, Inc., New York, NY, USA, 2001.

    Google Scholar 

  2. Gildas Avoine, Muhammed Ali Bingöl, Süleyman Kardaş, Cédric Lauradoux, and Benjamin Martin. A framework for analyzing rfid distance bounding protocols. J. Comput. Secur., 19:289–317, April 2011.

    Google Scholar 

  3. David Basin, Cas Cremers, and Catherine Meadows. Model Checking Security Protocols, chapter 24. Springer, 2011. To appear.

    Google Scholar 

  4. Prosenjit Bose, Pat Morin, Ivan Stojmenovi, and Jorge Urrutia. Routing with guaranteed delivery in ad hoc wireless networks. Wireless Networks, 7:609–616, 2001. 10.1023/A:1012319418150.

    Google Scholar 

  5. S. Brands and D. Chaum. Distance-bounding protocols. In Advances in Cryptology (EUROCRYPT’93), pages 344–359. Springer, 1994.

    Google Scholar 

  6. Srdjan Capkun and Jean-Pierre Hubaux. Secure positioning of wireless devices with application to sensor networks. In IEEE INFOCOM. IEEE Journal on Selected Areas in Communications: Special Issue on Security in Wireless Ad Hoc Networks, 2005.

    Google Scholar 

  7. Cas Cremers, Kasper Bonne Rasmussen, and Srdjan Capkun. Distance hijacking attacks on distance bounding protocols. Cryptology ePrint Archive, Report 2011/129, 2011. http://eprint.iacr.org/.

  8. B. Das and V. Bharghavan. Routing in ad-hoc networks using minimum connected dominating sets. In Communications, 1997. ICC 97 Montreal, ’Towards the Knowledge Millennium’. 1997 IEEE International Conference on, volume 1, pages 376 –380 vol.1, jun 1997.

    Google Scholar 

  9. D. Dolev and A. Yao. On the security of public key protocols. Information Theory, IEEE Transactions on, 29(2):198–208, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  10. D. Dolev and A.C. Yao. On the security of public key protocols. In Proc. of the 22nd Symp. on Foundations of ComputerScience, pages 350–357. IEEE Computer Society Press, 1981.

    Google Scholar 

  11. J. Du, E. Kranakis, O. Morales Ponce, and S. Rajsbaum. Neighbor discovery in a sensor network with directional antennae. In Algosensors, Saarbruecken, Germany, September 2011.

    Google Scholar 

  12. G.P. Hancke and M.G. Kuhn. An rfid distance bounding protocol. In Security and Privacy for Emerging Areas in Communications Networks, 2005. SecureComm 2005. First International Conference on, pages 67–73. IEEE, 2005.

    Google Scholar 

  13. C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

    Google Scholar 

  14. Y. C. Hu, A. Perrig, and D. B. Johnson. Packet leashes: a defense against wormhole attacks in wireless networks. In INFOCOM 2003. Twenty-Second Annual Joint Conference of the IEEE Computer and Communications Societies. IEEE, volume 3, pages 1976–1986 vol.3, 2003.

    Google Scholar 

  15. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055, pages 147–166. Springer-Verlag, Berlin Germany, march 1996. Also in Software Concepts and Tools, 17:93–102, 1996.

    Google Scholar 

  16. G. Lowe. Casper: A compiler for the analysis of security protocols. In Proc. of 10th Computer Security Foundations Workshop (CSFW’97). IEEE Computer Society Press, 1997. Also in Journal of Computer Security, Volume 6, pages 53–84, 1998.

    Google Scholar 

  17. Catherine Meadows, Radha Poovendran, Dusko Pavlovic, LiWu Chang, and Paul Syverson. Distance bounding protocols: Authentication logic analysis and collusion attacks. In Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks, edited volume, Springer, Nov. 2006, Nov 2006.

    Google Scholar 

  18. R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communication of the ACM, 21(12):993–999, 1978.

    Article  MATH  Google Scholar 

  19. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

    Google Scholar 

  20. Panagiotis (Panos) Papadimitratos, Marcin Poturalski, Patrick Schaller, Pascal Lafourcade, David Basin, Srdjan Capkun, and Jean-Pierre Hubaux. Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking. IEEE Communications Magazine, 46(2), 2008.

    Google Scholar 

  21. L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of computer security, 6(1–2):85–128, 1998.

    Google Scholar 

  22. Adrian Perrig, Ran Canetti, J. D. Tygar, and Dawn Song. The tesla broadcast authentication protocol. RSA CryptoBytes, 5, 2002.

    Google Scholar 

  23. M. Poturalski, P. Papadimitratos, and J.P. Hubaux. Secure neighbor discovery in wireless networks: formal investigation of possibility. In Proceedings of the 2008 ACM symposium on Information, computer and communications security, pages 189–200. ACM, 2008.

    Google Scholar 

  24. Marcin Poturalski, Panos Papadimitratos, and Jean-Pierre Hubaux. Secure Neighbor Discovery in Wireless Networks: Formal Investigation of Possiblity. Technical report, EPFL, 2007.

    Google Scholar 

  25. Marcin Poturalski, Panos Papadimitratos, and Jean-Pierre Hubaux. Towards Provable Secure Neighbor Discovery in Wireless Networks. In The 6th ACM Workshop on Formal Methods in Security Engineering, pages 31–42, Alexandria, VA, 2008. ACM.

    Google Scholar 

  26. P.Y.A. Ryan, S.A. Schneider, M.H. Goldsmith, G. Lowe, and A.W. Roscoe. The modelling and analysis of security protocols: the CSP approach. Addison-Wesley, 2000.

    Google Scholar 

  27. Patrick Schaller, Benedikt Schmidt, David Basin, and Srdjan Capkun. Modeling and verifying physical properties of security protocols for wireless networks. In Proceedings of the IEEE Computer Security Foundations Symposium (CSF), pages 109–123. IEEE, 2009.

    Google Scholar 

  28. S.A. Schneider. Security properties and CSP. In Proc. of the Symposium on Security and Privacy, pages 174–187. IEEE Computer Society Press, 1996.

    Google Scholar 

  29. R. Shokri, M. Poturalski, G. Ravot, P. Papadimitratos, and J.P. Hubaux. A practical secure neighbor verification protocol for wireless sensor networks. In Proceedings of the second ACM conference on Wireless network security, pages 193–200. ACM, 2009.

    Google Scholar 

  30. F. Javier Thayer, Vipin Swarup, and Joshua D. Guttman. Metric strand spaces for locale authentication protocols. In Masakatsu Nishigaki, Audun Jøsang, Yuko Murayama, and Stephen Marsh, editors, Trust Management IV - 4th IFIP WG 11.11 International Conference, IFIPTM 2010, Morioka, Japan, June 16–18, 2010. Proceedings, volume 321 of IFIP Conference Proceedings, pages 79–94. Springer, 2010.

    Google Scholar 

  31. S. Vasudevan, J. Kurose, and D. Towsley. On neighbor discovery in wireless networks with directional antennas. In INFOCOM 2005. 24th Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings IEEE, volume 4, pages 2502–2512. IEEE, 2005.

    Google Scholar 

  32. J. Wilson, V. Bhargava, A. Redfern, and P. Wright. A wireless sensor network and incident command interface for urban firefighting. In Mobile and Ubiquitous Systems: Networking & Services, 2007. MobiQuitous 2007. Fourth Annual International Conference on, pages 1–7. IEEE, 2007.

    Google Scholar 

  33. Jie Wu and Hailan Li. On calculating connected dominating set for efficient routing in ad hoc wireless networks. In Proceedings of the 3rd international workshop on Discrete algorithms and methods for mobile computing and communications, DIALM ’99, pages 7–14, New York, NY, USA, 1999. ACM.

    Google Scholar 

Download references

Acknowledgements

This work was supported by Projects TERRA and ARESA2.

Author information

Authors and Affiliations

  1. Université Grenoble 1, CNRS, Verimag, Grenoble, France

    Raphaël Jamet & Pascal Lafourcade

Authors
  1. Raphaël Jamet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pascal Lafourcade
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Raphaël Jamet .

Editor information

Editors and Affiliations

  1. , School of Computer Science, Carleton University, Colonel By Drive 1125, Ottawa, K1S 5B6, Ontario, Canada

    Evangelos Kranakis

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Jamet, R., Lafourcade, P. (2012). Formal Model for (k)-Neighborhood Discovery Protocols. In: Kranakis, E. (eds) Advances in Network Analysis and its Applications. Mathematics in Industry, vol 18. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30904-5_8

Download citation

Publish with us

Policies and ethics

Search

Navigation