Kademlia is a peer-to-peer distributed hash table (DHT) currently used in the P2P eDonkey file sharing network. Kademlia offers a number of desirable features that result from the use of a notion of distance between objects based on the bitwise exclusive (XOR) of the n-bit quantities that represent both nodes and files. Nodes keep information about files close or near to them in the key space in their routing tables. The search algorithm is based on looking for the closest node (or almost closest node, if the information is replicated) to the file key. The structure of the routing tables defined in each peer guarantees that the lookup algorithm takes no longer than log n steps.
This paper explains the specification of the behaviour of a P2P network that uses the Kademlia DHT in the formal specification language Maude. We use the initial description of the Kademlia DHT and fill some open issues with the eMule real implementation. We allow peers to connect to the network and leave it by simulating time using the Real Time Maude facilities.
We present the distributed specification of the behavior of a P2P network that uses the Kademlia DHT in the formal specification language Maude. We use sockets to connect different Maude instances and create a P2P network where the Kademlia protocol may be used. This protocol is executed on top of a previously developed routing protocol that provides real-time by connecting Maude to an external Java server and allows peers to enter and leave the network dynamically. Then, we show how to represent this distributed system in one single term in order to simulate and analyze the system using the Real-Time Maude facilities.
This paper presents the specification of both the Kademlia and the Kad routing tables, using the specification language Maude. As far as we know, this is the first such a formal development. Using our two formal specifications, we can isolate some of those differences and detect some open issues on the original description, mainly related with message passing. In this context, our main contribution is the integration of the dynamic aspects of the routing table with the full protocol specification.
MultiClientTimer. It must be started before launching the Maude processes.
erewcommand must be used. It must receive a configuration containing a location, an EIGRP router, and a peer. We provide here 6
erewcommands, that must be executed in different Maude instances in any order. These commands assume that they are located in the same folder as the distributed configuration and thus they can load the appropriate modules and start the external rewrites. Note that tracing options are activated to show when the Kademlia rules are applied. Files: erew1, erew2, erew3, erew4, erew5, and erew6.