This thesis studies the properties of vector-based routing protocols whose underlying algebras are strictly increasing. Strict increasingness has previously been shown to be both a sufficient and a necessary condition for the convergence of path-vector protocols.

One of the key contributions of this thesis is to link vector-based routing to a much larger family of asynchronous iterative algorithms. This unlocks a significant body of existing theory, and allows asynchronous protocols to be proved correct by purely synchronous reasoning. As well as applying it to routing protocols, this thesis advances the asynchronous theory in two ways. Firstly it shows that the existing conditions required for convergence may be relaxed. Secondly it proposes the first model for ``dynamic'' asynchronous processes in which both the problem being solved and the set of participants change over time.

The thesis' attention then turns to models of routing problems, and presents a new algebraic structure that is simpler and more expressive than the state of the art. In particular this structure is capable of modelling routing problems that underlie both distance-vector and path-vector protocols. Consequently these two families of vector-based protocols may be unified for the first time. The new structure is also capable of modelling protocols that use path-dependent conditional policy.

Next the work above is used to construct a model of an abstract vector-based protocol. This is then used in the first proof of correctness for strictly increasing distance-vector protocols and a new proof of correctness for strictly increasing path-vector protocols. The latter is an improvement over previous results as it i) proves that convergence is deterministic ii) does not assume reliable communication between nodes and iii) applies to path-vector protocols with path-dependent conditional policy. The long standing question of the worst-case rate of convergence for a strictly increasing path-vector protocol is then answered by lowering the previous upper bound of $O(n!)$ to a new tight bound of~$\Theta (n2)$.

Finally all of the work has been formalised in the proof assistant Agda. Not only does this significantly increase users' confidence in the validity of the results, the resulting Agda library may also be used to verify the correctness of protocol implementations. To illustrate this, a formal proof of correctness is described for a path-vector protocol which contains many of the features of the Border Gateway Protocol including: local preferences, communities, an expressive conditional policy language and path inflation.