When designing and verifying security protocols, a certain level of idealization is needed to provide manageable mathematical treatment. Accordingly, two views of cryptography have been developed over the years, by two mostly separate communities. In the first view, cryptographic protocols are expressed algebraically, within simple languages. This view is suitable for formal reasoning and automated tools, but also arguably too abstract. In the second view, cryptographic primitives are concrete algorithms that operate on bitstrings. This view involves probabilities and limits in computing power; it is harder to handle formally, especially when dealing with large protocols. Getting the best of both views is appealing, and is the subject of active research. In this work, we develop a first sound and complete implementation of a distributed process calculus. Our calculus provides secure primitives for messaging and authentication, but not explicit cryptography. It supports simple reasoning, based on labelled transitions and observational equivalence. We precisely describe its implementation in a computational setting, using abstract machines and standard cryptographic assumptions. We show that high level reasoning accounts for all low-level adversaries. We also discuss the resulting constraints on high-level language design. Joint work with Cédric Fournet.