A User Model for Information Erasure

TL;DR

This paper formalizes the role of users in information erasure systems, defining requirements for user behavior to ensure combined system erasure, and proves that erasure-friendly users can be composed with erasing systems for joint erasure.

Contribution

It introduces a formal user model and erasure friendliness requirements, strengthening previous work by ensuring user-system composition guarantees erasure.

Findings

Formal user model and erasure friendliness defined

Proved composition of erasure-friendly user with erasing system yields joint erasure

Identified stronger user requirements for effective erasure

Abstract

Hunt and Sands (ESOP'08) studied a notion of information erasure for systems which receive secrets intended for limited-time use. Erasure demands that once a secret has fulfilled its purpose the subsequent behaviour of the system should reveal no information about the erased data. In this paper we address a shortcoming in that work: for erasure to be possible the user who provides data must also play his part, but previously that role was only specified informally. Here we provide a formal model of the user and a collection of requirements called erasure friendliness. We prove that an erasure-friendly user can be composed with an erasing system (in the sense of Hunt and Sands) to obtain a combined system which is jointly erasing in an appropriate sense. In doing so we identify stronger requirements on the user than those informally described in the previous work.