A peer-to-peer ( p2p ) system provides the networking substrate for the execution of distributed applications. It is made of peers that interact over an overlay network . Overlay networks are highly dynamic, as peers can join and leave at any time. Traditional process calculi, such as π -calculus, CCS and others, seem inadequate to capture these kinds of networks, their routing mechanisms, and to verify their properties. In order to model network architecture in a more explicit way, in [Ugo Montanari and Matteo Sammartino. Network conscious π -calculus: A concurrent semantics. ENTCS , 286:291–306, 2012; Matteo Sammartino. A Network-Aware Process Calculus for Global Computing and its Categorical Framework. PhD thesis, University of Pisa, 2013. available at http://www.di.unipi.it/~sammarti/publications/thesis.pdf ; Ugo Montanari and Matteo Sammartino. A network-conscious π -calculus and its coalgebraic semantics. Theor. Comput. Sci. , 546:188–224, 2014] we have introduced the Network Conscious π-calculus ( NCPi ), an extension of the π -calculus with names representing network nodes and links. In [Ugo Montanari and Matteo Sammartino. A network–conscious π -calculus and its coalgebraic semantics. Theor. Comput. Sci. , 546:188–224, 2014] (a simpler version of) NCPi has been equipped with a coalgebraic operational models, along the lines of Fiore-Turi presheaf-based approach [Marcelo P. Fiore and Daniele Turi. Semantics of name and value passing. In LICS 2001 , pages 93–104. IEEE Computer Society, 2001], and with an equivalent History Dependent Automaton [Ugo Montanari and Marco Pistore. Structured coalgebras and minimal hd-automata for the π -calculus. Theor. Comput. Sci. , 340(3):539–576, 2005], i.e., an (often) finite-state automaton suitable for verification. In this paper we first give a brief account of these results. Then, our contribution is the sketch of a NCPi representation of the p2p architecture Pastry . In particular, we give models of its overlay network and of a Distributed Hash Table built on top of it, and we give evidence of their correctness by proving convergence of routing mechanisms. [ABSTRACT FROM AUTHOR]