Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHTs protocols to scale to millions of nodes. Consequently, the correct operation of DHTs is essential for the proper functioning of many practical and P2P systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. To improve the current state of the art, in this paper we propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation to establish a number of DHT-derived properties and generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.