Butler Lampson
Microsoft
There are lots of protocols for establishing connections (or equivalently, doing at-most-once message delivery) across a network that can delay, reorder, duplicate and lose packets. Most of the popular ones are based on three-way handshake, but some use clocks or extra stable storage operations to reduce the number of messages required. It’s hard to understand why the protocols work, and there are almost no correctness proofs; even careful specifications are rare.
I will give a specification for at-most-once message delivery, an informal account of the main problems an implementation must solve and the common features that most implementations share, and outlines of proofs for three implementations. The specifications and proofs based on Lamport’s methods for using abstraction functions to understand concurrent systems, and I will say something about how his methods can be applied to many other problems of practical interest.
Word, Acrobat, HTML.
A paper with many more details is here.