3rd International ICST Conference on Broadband Communications, Networks, and Systems

Research Article

How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET

  • @INPROCEEDINGS{10.1109/BROADNETS.2006.4374344,
        author={Panagiotis  Papadimitratos and Zygmunt J. Haas and Jean-Pierre Hubaux},
        title={How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET},
        proceedings={3rd International ICST Conference on Broadband Communications, Networks, and Systems},
        publisher={IEEE},
        proceedings_a={BROADNETS},
        year={2012},
        month={6},
        keywords={},
        doi={10.1109/BROADNETS.2006.4374344}
    }
    
  • Panagiotis Papadimitratos
    Zygmunt J. Haas
    Jean-Pierre Hubaux
    Year: 2012
    How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET
    BROADNETS
    IEEE
    DOI: 10.1109/BROADNETS.2006.4374344
Panagiotis Papadimitratos1,*, Zygmunt J. Haas2,*, Jean-Pierre Hubaux1,*
  • 1: EPFL Lausanne, Switzerland
  • 2: Cornell University, Ithaca, NY, USA
*Contact email: papos.papadimitratos@epfl.ch, haas@ece.cornell.edu, jean-pierre.hubaux@epfl.ch

Abstract

Secure routing protocols for mobile ad hoc networks have been developed recently, yet, it has been unclear what are the properties they achieve, as a formal analysis of these protocols is mostly lacking. In this paper, we are concerned with this problem, how to specify and how to prove the correctness of a secure routing protocol. We provide a definition of what a protocol is expected to achieve independently of its functionality, as well as a communication and adversary models. This way, we enable formal reasoning on the correctness of secure routing protocols. We demonstrate this by analyzing two protocols from the literature.