Abstract
Kad is the implementation by eMule and aMule of the Kademlia peer-to-peer distributed hash table protocol. Although it agrees with the basic behaviour of the protocol, there are some significant differences. 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. The routing tables present a dynamic behavior in the sense that they should be able to send messages to other peers and they should have a notion of time for raising events and detect no answered messages. Our main contribution is the integration of these dynamic aspects in the protocol specification.
Research supported by MEC Spanish project DESAFIOS10 (TIN2009-14599-C03-01) and Comunidad de Madrid program PROMETIDOS (S2009/TIC1465).
Chapter PDF
Similar content being viewed by others
References
Bakhshi, R., Gurov, D.: Verification of peer-to-peer algorithms: A case study. In: Combined Proceedings of the Second International Workshop on Coordination and Organization, CoOrg 2006, and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord 2006. Electronic Notes in Theoretical Computer Science, vol. 181, pp. 35–47. Elsevier (2007)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Lu, T., Merz, S., Weidenbach, C.: Towards Verification of the Pastry Protocol Using TLA + . In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE 2011. LNCS, vol. 6722, pp. 244–258. Springer, Heidelberg (2011)
Maymounkov, P., Mazières, D.: Kademlia: A peer-to-peer information system based on the XOR metric. In: Druschel, P., Kaashoek, M.F., Rowstron, A. (eds.) IPTPS 2002. LNCS, vol. 2429, pp. 53–65. Springer, Heidelberg (2002)
Mysicka, D.: Reverse Engineering of eMule. An analysis of the implementation of Kademlia in eMule. Semester thesis, Dept. of Computer Science, Distributed Computing group, ETH Zurich (2006)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20, 161–196 (2007)
Pita, I.: A formal specification of the Kademlia distributed hash table. In: Gulías, V.M., Silva, J., Villanueva, A. (eds.) Proceedings of the 10 Spanish Workshop on Programming Languages, PROLE 2010, pp. 223–234. Ibergarceta Publicaciones (2010), http://www.maude.sip.ucm.es/kademlia (Informal publication–Work in progress)
Pita, I., Fernández Camacho, M.I.: Formal Specification of the Kademlia Routing Table and the Kad Routing Table in Maude. Technical Report 1/2013. Dept. Sistemas Informáticos y Computación Universidad Complutense de Madrid (January 2013), http://www.maude.sip.ucm.es/kademlia
Pita, I., Riesco, A.: Specifying and Analyzing the Kademlia Protocol in Maude. In: 9th International Workshop on Rewriting Logic and its Applications, WRLA 2012 (2012)
Ratnasamy, S., Francis, P., Handley, M., Karp, R., Shenker, S.: A scalable content-addressable network. In: ACM SIGCOMM Computer Communication Review - Proceedings of the 2001 SIGCOMM Conference, vol. 31, pp. 161–172 (October 2001)
Rowstron, A., Druschel, P.: Pastry: Scalable, decentralized object location, and routing for large-scale peer-to-peer systems. In: Guerraoui, R. (ed.) Middleware 2001. LNCS, vol. 2218, pp. 329–350. Springer, Heidelberg (2001)
Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: A scalable peer-to-peer lookup service for internet applications. ACM SIGCOMM Computer Communication Review 31, 149–160 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Pita, I., Fernández-Camacho, MI. (2013). Formal Specification of the Kademlia and the Kad Routing Tables in Maude. In: Martí-Oliet, N., Palomino, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2012. Lecture Notes in Computer Science, vol 7841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37635-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-37635-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37634-4
Online ISBN: 978-3-642-37635-1
eBook Packages: Computer ScienceComputer Science (R0)