A new proof of the GHS minimum spanning tree algorithm

This paper provides a proof of correctness for the celebrated Minimum Spanning Tree protocol of Gallager, Humblet and Spira [GHS83]. Both the protocol and the quest for a natural correctness proof have had considerable impact on the literature concerning network protocols and verification. We present an invariance proof that is based on a new intermediate-level abstraction of the protocol. A central role of the intermediate-level configurations in the proof is to facilitate the statement of invariants and other properties of the executions of GHS at the low level. This provides a powerful tool for both the statement and the proof of properties of the algorithm. The result is the first proof that follows the spirit of the informal arguments made in the original paper.