dc.contributor.author Daggitt, Matthew Lucian dc.date.accessioned 2019-04-29T12:08:55Z dc.date.available 2019-04-29T12:08:55Z dc.date.issued 2019-07-31 dc.date.submitted 2018-12-18 dc.identifier.uri https://www.repository.cam.ac.uk/handle/1810/292067 dc.description.abstract 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(n^2)$. 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. dc.description.sponsorship EPSRC Doctoral Training grant dc.format Needs Agda 2.6.0 and Agda Standard Library 1.0 dc.language.iso en dc.rights Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0) dc.rights.uri https://creativecommons.org/licenses/by-nc-sa/4.0/ dc.subject Routing protocols dc.subject Agda dc.subject Asynchronous iterations dc.subject Parallel algorithms dc.subject Formal verification dc.subject Algebra dc.subject Convergence dc.subject Vector-based routing dc.subject Path-vector dc.subject Distance-vector dc.subject Routing dc.subject BGP dc.subject RIP dc.title An algebraic perspective on the convergence of vector-based routing protocols dc.type Thesis dc.type.qualificationlevel Doctoral dc.type.qualificationname Doctor of Philosophy (PhD) dc.publisher.institution University of Cambridge dc.publisher.department Department of Computer Science and Technology, University of Cambridge dc.date.updated 2019-04-29T05:53:59Z dc.identifier.doi 10.17863/CAM.39222 dc.contributor.orcid Daggitt, Matthew Lucian [0000-0002-2552-3671] dc.publisher.college Jesus dc.type.qualificationtitle PhD in Computer Science cam.supervisor Griffin, Timothy cam.thesis.funding true
﻿

### This item appears in the following Collection(s)

Except where otherwise noted, this item's licence is described as Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)