Proving properties of the Chord protocol using the ASM formalism.

This paper describes the overlay protocol Chord using the formalism of Abstract State Machines. The formalization concerns Chord actions that maintain ring topology and manipulate distributed keys. We define a minimal set of deterministic constraints and prove that they guarantee the stability of the topological structure of the network and the consistency of data handling.