Formal Verification of the Pastry Protocol Using

As a consequence of the rise of cloud computing, the reliability of network protocols is gaining increasing attention. However, formal methods have revealed inconsistencies in some of these protocols, e.g., Chord, where all published versions of the protocol have been discovered to be incorrect. Pastry is a protocol similar to Chord. Using

$$\mathrm{{TLA}}^{+}$$

, a formal specification language, we show that LuPastry, a formal model of Pastry with some improvements, provides correct delivery service. This is the first formal proof of Pastry where concurrent joins and lookups are simultaneously allowed. In particular, this article relaxes the assumption from previous publication to allow arbitrary concurrent joins of nodes, which reveals new insights into Pastry through a final formal model in

$$\mathrm{{TLA}}^{+}$$

,

LuPastry

. Besides, this article also illustrates the methodology for the discovery and proof of its invariant. The proof in

$$\mathrm{{TLA}}^{+}$$

is mechanically verified using the interactive theorem prover TLAPS.