A correctness proof of the DSR protocol

The correctness of a routing protocol consists of two kinds of properties: safety and liveness. Safety properties specify that every route found by the protocol is well formed, while liveness properties specify that useful routes will eventually be found and data messages be eventually delivered to recipients. Many safety properties for routing protocols have been verified; however, the verification of liveness properties was overlooked. This paper stresses the importance of liveness properties of routing protocol and presents a formal verification of the DSR (Dynamic Source Routing) protocol dealing with both safety and liveness properties. The results are checked with Isabelle/HOL/Isar.