Formal analysis of pure-join model of chord using alloy

Chord is a popular structured peer-to-peer protocol. In this protocol a hash function is used to identify Nodes ID and data Keys. Therefore, it is possible that different nodes have the same ID; examining the features of this protocol under the condition in which different nodes may have the same ID is important. In this paper, using Alloy, we formally examine two features of Pure-Join model of Chord in such a condition: “Join preserves validity or not” and “The state of Allcycle can be reached with stabilize operation or not”. Our study shows that with high probability, Join preserves validity, and Chord cannot reach “Allcycle” state with stabilize operation in some cases.