Formal verification of routing protocols for wireless ad hoc networks