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

## TL;DR

This paper formalizes secure remote memory erasure against standard Dolev-Yao adversaries, providing necessary and sufficient conditions for protocol security and analyzing the associated cryptographic trade-offs.

## Contribution

It introduces a formal definition of secure memory erasure under standard adversarial models and characterizes the exact adversary restrictions needed for protocol security.

## Key findings

- Necessary and sufficient adversary restrictions identified
- A protocol description using standard cryptographic notation provided
- Security and communication complexity trade-offs analyzed

## Abstract

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.