The specifications of electronic money protocols usually presented in the literature consist of informal descriptions of message flows. Therefore, it seems essential to develop a formalism to specify and verify such protocols. To this end, we start by sketching an enrichment of the spi-calculus encompassing the notion of state. Using this formalism, we specify an electronic money protocol. In order to show that this protocol is secure against e-coin replication in the presence of private and authenticated channels, we first introduce a notion of equivalence between agents and explore its main properties. Indeed, the protocol is shown to be secure by proving that it is equivalent to an ideal perfect protocol. Finally, we also show how to emulate private and authenticated channels using public channels and cryptography.