Using Process Algebra to Design Better Protocols

Protocol design, development and standardisation still follow the lines of rough consensus and running code. This approach yields fast and impressive results in a sense that protocols are actually implemented and shipped, but comes at a price: protocol specifications, which are mainly written in natural languages without presenting a formal specification, are (excessively) long, ambiguous, underspecified and erroneous. These shortcomings are neither new nor surprising, and well documented. It is the purpose of this paper to provide further evidence that formal methods in general and process algebras in particular can overcome these problems. They provide powerful tools that help to analyse and evaluate protocols, already during the design phase. To illustrate this claim, I report how a combination of pen-and-paper analysis, model checking and interactive theorem proving has helped to perform a formal analysis of the Ad hoc On-Demand Vector (AODV) routing protocol.