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

TL;DR

This paper introduces a formal framework for specifying and proving the correctness of secure routing protocols in MANETs, enabling rigorous analysis of their properties.

Contribution

It provides a formal specification method and correctness proof approach for secure routing protocols, demonstrated on two existing protocols.

Findings

Formal definitions of protocol properties and adversary models

Successful formal analysis of two literature protocols

Enhanced understanding of protocol correctness and security guarantees

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 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.