Secure memory erasure in the presence of man-in-the-middle attackers. (March 2021)

• Record Type: Journal Article
• Authors: Trujillo-Rasua, Rolando
• Is Part Of: Journal of information security and applications. Volume 57(2021)
• Publication Date: 2021-03
• Subjects: Memory erasure -- Security protocols -- Formal verification -- Distance bounding; Computer security -- Periodicals; Information technology -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.jisa.2020.102730
• Languages: English
• ISSNs: 2214-2126

Abstract

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.