Secure Memory Erasure in the Presence of Man-in-the-Middle Attackers

Memory erasure protocols serve to clean up a device's memory before the installation of new software. Although this task can be accomplished by direct hardware manipulation, remote software-based memory erasure protocols have emerged as a more efficient and cost-effective alternative. Existing remote memory erasure protocols, however, still rely on non-standard adversarial models to operate correctly, thereby requiring additional hardware to restrict the adversary's capabilities. In this work, we provide a formal definition of secure memory erasure within a symbolic security model that utilizes the standard Dolev-Yao adversary. Our main result consists of a restriction on the Dolev-Yao adversary that we prove necessary and sufficient to solve the problem of finding a protocol that satisfies secure memory erasure. We also provide a description of the resulting protocol using standard cryptographic notation, which we use to analyze the security and communication complexity trade-off commonly present in this type of protocols.