Specifying and Analyzing the Kademlia Protocol in Maude

Kademlia is the most popular peer-to-peer distributed hash table DHT currently in use. It offers a number of desirable features that result from the use of a notion of distance between objects based on the bitwise exclusive or of n-bit quantities that represent both nodes and files. Nodes keep information about files close or near to them in the key space and the search algorithm is based on looking for the closest node to the file key. The structure of the routing table defined in each peer guarantees that the lookup algorithm takes no longer than Ologn steps, where n is the number of nodes in the network. This paper presents a formal specification of a P2P network that uses the Kademlia DHT in the Maude language. We use sockets to connect different Maude instances and create a P2P network where the Kademlia protocol can be used, hence providing an implementation of the protocol which is correct by design. Then, we show how to abstract this system in order to analyze it by using Real-Time Maude. The model is fully parameterized regarding the time taken by the different actions to facilitate the analysis of various scenarios. Finally, we use time-bounded model-checking and exhaustive search to prove properties of the protocol over different scenarios.