*[table]skip=-10pt,belowskip=-10pt *[figure]skip=5pt,belowskip=-10pt soft open fences

# Software-Based Memory Erasure with relaxed isolation requirements: Extended
Version111This is an extended version of [15]. Here we propose a third memory-
erasure protocol and show the proofs missing in the original article.

Sergiu Bursuc
University of Luxembourg
<EMAIL_ADDRESS>0000-0002-0409-5735 Reynaldo Gil-Pons
University of Luxembourg
<EMAIL_ADDRESS>Reynaldo Gil-Pons was supported by the Luxembourg
National Research Fund, Luxembourg, under the grant AFR-PhD-14565947.
0000-0003-1804-3319 Sjouke Mauw
University of Luxembourg
<EMAIL_ADDRESS>0000-0002-2818-4433 Rolando Trujillo-Rasua
Rovira i Virgili University
<EMAIL_ADDRESS>Rolando Trujillo-Rasua was funded by a Ramon y Cajal
grant from the Spanish Ministry of Science and Innovation and the European
Union (REF: RYC2020-028954-I). 0000-0002-8714-4626

###### Abstract

A Proof of Secure Erasure (PoSE) is a communication protocol where a verifier
seeks evidence that a prover has erased its memory within the time frame of
the protocol execution. Designers of PoSE protocols have long been aware that,
if a prover can outsource the computation of the memory erasure proof to
another device, then their protocols are trivially defeated. As a result, most
software-based PoSE protocols in the literature assume that provers are
isolated during the protocol execution, that is, provers cannot receive help
from a network adversary. Our main contribution is to show that this
assumption is not necessary. We introduce formal models for PoSE protocols
playing against provers aided by external conspirators and develop three PoSE
protocols that we prove secure in this context. We reduce the requirement of
isolation to the more realistic requirement that the communication with the
external conspirator is relatively slow. Software-based protocols with such
relaxed isolation assumptions are especially pertinent for low-end devices,
where it is too costly to deploy sophisticated protection methods.

##  1 Introduction

Internet of Things (IoT) devices are specially vulnerable to malware infection
due to their ubiquity, connectivity and limited computational resources [34].
Once infected, an IoT device becomes both a victim and a useful weapon to
launch further attacks on more advanced infrastructure and services. Detecting
whether an IoT device is infected with malware is thus essential to
maintaining a secure computer network. The challenge for the defender is
operating within the resource constraints of IoT devices, which make them ill-
suited for active security defences and health monitoring [33].

A pragmatic approach to ensure the absence of malware is secure erasure,
consisting of putting a device back into a clean state by wiping out its
memory. This approach was first introduced in [37] as a prerequisite for
secure software update. Although memory erasure can be achieved via direct
hardware manipulation, here we are interested in Secure Erasure protocols
(PoSE), whereby a verifier instructs a resource-constrained device, called the
prover, to erase its memory and to prove that it indeed has done so. Notice
that a PoSE protocol is not a data erasure tool [26], despite both being aimed
at erasing memory. The latter is meant to erase sensitive data from memory in
an irreversible manner, i.e., in a way that is unrecoverable by advanced
forensics techniques. The former is a lightweight communication protocol
whereby a verifier attests whether a (possibly) compromised prover has filled
its memory with random data.

Because provers are potentially infected with malware, PoSE protocols in
general cannot rely on cryptographic secrets stored in the prover. The
exception are protocols that rely on secure hardware [9], such as a Trusted
Platform Module. Not all devices are manufactured with secure hardware,
though. Examples are those designed for low price and low energy consumption.
Hence, in this article, we don’t assume secure hardware on provers and we seek
a software-based solution.

In the absence of cryptographic secrets, software-based PoSE protocols have
historically relied on the assumption that provers are isolated during the
protocol execution, that is, provers cannot receive external help. The
isolation assumption has been deemed necessary so far to prevent a malicious
prover from outsourcing the erasure proof to another device. Ensuring
isolation is cumbersome, though. It requires closing all communication
channels between provers and potential conspirators, for example, by jamming
or using a Faraday cage.

The goal of this work is to reduce the requirement of isolation to the more
realistic requirement that the external conspirator (which we call a _distant
attacker_) is further away from the verifier than the prover (see Figure 1 for
an illustration). That is, we do not restrict the communication capabilities
of the (possibly corrupt) prover with the external adversary, but their
position relative to each other. In practice, this can be accomplished relying
on round-trip-time measurements, to ensure that the responses received to a
sequence of challenges come from the device whose memory we aim to erase. Such
measurements are used in distance-bounding protocols, whose goal is to ensure
the authenticity of communication with a nearby device [25]. For ensuring our
distant-attacker assumption, we can therefore build upon the principles of
design in distance-bounding protocols, of which there exist already various
proof-of-concepts and real-life implementations. While the messages exchanged
in classic distance-bounding protocols typically consist of single bits [40],
recent progress in the communication infrastructure allows fast exchange of
longer messages. This was proved feasible in [14], assuming that attackers are
using only commercial off-the shelf hardware. Furthermore, the relay resistant
protection mechanism in the EMV protocol [23] and later improvements [39]
measure the round-trip-time of 32-bit packets in order to bound distance. In
the context of electric vehicle charging systems, [18] also considers a bigger
than binary alphabet for their messages. In our proposed protocols, we will
exploit this feature in order to challenge random blocks of the device’s
memory, rather than bits.

DeviceVerifier

DeviceVerifierAttacker

Figure 1:  The isolation assumption (on the left) assumes no interference in
the prover-verifier communication. The distant attacker assumption (on the
right) lets the attacker interfere from far away.

_Overview and contributions._ To demonstrate that secure memory erasure is
possible without assuming isolation, we introduce and formalize a class of
PoSE protocols that employs a distance-bounding mechanism, which we call PoSE-
DB, and put forward three protocols in this class together with formal
security proofs against a corrupt prover that communicates with an external
attacker. PoSE-DB protocols will have an interactive phase consisting of
several challenge-response rounds. For each round, they will measure the
round-trip-time between the challenge and response, and verify that the
response is correct, aiming for two security goals. First, the prover cannot
relay its communication with the verifier to the distant attacker without
failing the distance-bounding check, compelling the prover to compute the
responses locally. Second, if the prover locally computes the responses to the
verifier’s challenges, then it must have erased its memory even if aided by an
external attacker. The first contribution of this work is a formalization of
those security requirements (Section 3).

Our second contribution is the development of three PoSE-DB protocols with
formal security proofs. The first protocol (Section 5) is based on a
straightforward idea, already used in the first secure erasure protocol
proposed by Perito and Tsudik [37]: the verifier sends a random sequence of
bits to the prover, who should store it in its memory; then the verifier
queries random memory blocks to check that they are stored. We adapt this idea
into a PoSE-DB protocol, where we query one random block per round, checking
that the reply is correct and is received within the specified time bound. Our
main contribution in this case is a formal security proof without resorting to
the device isolation assumption. Although the protocol is simple, the proof is
not trivial, and we introduce general proof methods in Section 4 that help the
analysis by allowing to focus on a single challenge-response round.

Sending a sequence of bits as large as the prover’s memory may be undesirable
in some contexts, e.g. when the communication channels have limited capacity.
Instead, in our second protocol (Section 6), the verifier sends a small seed
to the prover, which uses it to compute the labelling of a suitably chosen
graph and store the labels of some nodes. In the interactive phase, we run
several fast rounds to verify that those labels are stored. We identify a
depth-robustness property for the graph that ensures the security of our
proposed protocol: we show that a cheating prover needs to spend significant
time to recompute any missing labels, so it will be caught by our time
measurement. Our third protocol (Section 8) is also based on graphs, but
trades-off security for performance.

Although graph-labelling techniques have been used in related works, e.g. for
memory hardness [5, 6], proofs of space [21, 11, 38], and classic secure
erasure [22, 28], none of them can directly be applied in our context. This is
because we want to erase the full memory of the device, and we consider a
stronger attacker model. In all the previous protocols, the gap between the
memory filled by the prover and the full memory of the device is too high,
either because they consider a different case study where this is not a
concern (e.g. for proofs of space), or because the class of graphs is not
strong enough (e.g. the proof in [28] can only erase $\frac{1}{32}$ of the
full memory because of this reason). Furthermore, the protocols that directly
target memory erasure, i.e. [22, 28], are also not adequate for our attacker
model; they either assume protected memory [22] or the device isolation
assumption [28]. Indeed, [22] assumes at least part of a secret key not to be
leaked, while in our model we allow full compromise of the memory content. In
the protocol from [28], the prover needs to compute the graph labelling on the
fly after being challenged to return a label, which is unsuitable for distance
bounding.

We therefore propose a new class of graphs that allows our protocol to proceed
in two phases, first compute and store the labels, and then reply to several
rounds of challenges, thus proving the labels are stored. We prove that the
resulting protocol can securely erase all but a small proportion of the
prover’s memory. Furthermore, our protocol provides its security guarantees in
the presence of a distant attacker, without resorting to device isolation or
protected memory assumptions. The undirected graph we propose (Section 7)
satisfies a classic property of depth-robustness and can be computed in-place,
i.e. by using only a constant memory overhead for the prover. This tightness
constraint for the graph is especially important if we want to erase the full
memory of the device. Our graph is tighter in this respect than other depth-
robust graphs used recently in the literature [28, 21, 5, 38], and we believe
this makes the graph of interest in other domains too, such as proof of space
and memory hardness.

##  2 Related Work

We review memory erasure and attestation protocols for resource-constrained
devices that don’t use secure hardware. See [31] for a review of protocols
that use it. We will see that the main limitation of current software-based
protocols, as highlighted in a recent survey [9], is the assumption that there
is a secure communication channel between verifier and prover, called the
_device isolation assumption_.

_Software-based memory isolation._ Some protocols use software-based memory
isolation techniques that continuously monitors the programs running on the
device. In this class, SPEED[8] and SIMPLE[7] perform memory erasure and
attestation, respectively. These protocols could, in theory, achieve our
security goals. In practice, they add a significant overhead to any program
running on the platform, as the software TPM continuously monitors the
platform to ensure memory isolation at all times. Since memory erasure can
start from any state of the device, we do not need to impose constraints on
programs running on it. SPEED uses distance-bounding to ensure that only a
nearby verifier can start the memory erasure procedure. We use distance-
bounding in the opposite direction, where the verifier is the challenger
aiming to ensure the prover is near.

_Time-optimal memory erasure routine._ SWATT is an attestation protocol [42]
based on computing a checksum function over the memory of the prover within a
prescribed amount of time. The idea is that, had the prover’s memory been
compromised, the prover would take noticeably longer to generate the correct
attestation proof. Several attacks on SWATT were shown in [16], the main
problem being that the checksum function and the timing constraints are rather
ad hoc. This problem was later treated in [10], which proposes a formal model
of software-based attestation and a generic protocol similar to SWATT, but,
this time with a formal security proof. The problem here is that, if the local
device is not isolated, the attacker could compute the response on a separate
device and return it in time. Another problem is that the global running time
of the erasure procedure is too high in order to detect small changes to the
memory. The attacker could use the available time to optimize procedures and
recompute the data that is missing. That is why [10] suggests the idea of a
multi-round protocol, requiring shorter computation time in each round. This
is an idea we develop further in this paper as part of a distance-bounding
mechanism.

The first protocol for secure memory erasure based on cryptographic techniques
is introduced in [37]. The paper proposes a protocol based on computing a
(time-optimal) MAC over randomly generated data that fills the memory of the
prover, along with an informal adversarial model and argument of security.
This protocol uses a high bandwidth to transmit the random data and cannot
prevent the computation to be delegated to an external attacker without
isolating the device, like in [42, 10].

_Graph pebbling games._ A recent series of papers use graph pebbling
techniques to achieve time-memory trade-offs, e.g. in proofs of secure erasure
[22, 28], proofs of space, or memory-hardness results. The works aiming for
memory erasure cannot be applied in our context, as discussed in the
introduction. We should mention, in addition, that [28] also proposes an
erasure protocol that is not based on graphs, but on hard-to-invert hash
functions. In addition to assuming device isolation, the security of this
protocol is proved assuming that, in the memory challenge phase, the adversary
cannot query a hash function. We are not aware how this could be enforced in
practice.

_Distance-bounding techniques._ A PoSE protocol that relies on distance
bounding in a spirit similar to ours was proposed in [43]. It uses a cyclic
tree automaton that occupies the full prover’s memory. To obtain the erasure
proof, the verifier asks the prover to transition into a new state of the
automaton, based on random input chosen by the verifier, and to transmit the
label of the new state. This round of exchanges is timed by the verifier to
bound its distance to the prover. However, we observe that the fact that the
response comes fast in each round is not sufficient to counter pre-computation
attacks or an adaptive attacker. For example, depending on previous
challenges, the adversary can get rid of states in the automaton that are
unreachable by future verifier’s challenges. This attack was overlooked
because the protocol was analysed within a symbolic model, rather than a
computational model as we do in this paper.

As summarized in Figure 2, there does not exist in the literature a software-
based memory erasure (or attestation) protocol whose security can be formally
proven without relying on the device isolation assumption. Section 5 and
Section 6 in this article introduce the first three protocols of this type.

Protocol | No Isol. | No Hw. | Comm.
---|---|---|---
[42] | ✗ | ✓ | $\mathcal{O}(1)$
[29] | ✓ | ✗ | $\mathcal{O}(1)$
[37] | ✗ | ✓ | $\mathcal{O}(n)$
[35] | ✓ | ✗ | $\mathcal{O}(1)$
[11] | ✗ | ✓ | $\mathcal{O}(1)$
[28] | ✗ | ✓ | $\mathcal{O}(1)$
[27] | ✗ | ✓ | $\mathcal{O}(n)$
5 | ✓ | ✓ | $\mathcal{O}(n)+\mathcal{O}(r)$
6 | ✓ | ✓ | $\mathcal{O}(1)+\mathcal{O}(r)$
Figure 2:  Comparison of erasure and attestation protocols in terms of their
communication complexity (Comm) and their capacity to _avoid_ the use of the
device isolation assumption (No Isol.) and specialised hardware (No Hw.). The
value of $n$ refers to the memory size and $r$ is a security parameter that
refers to the number of rounds during the fast phase (see Section 3).

_Formal security definitions._ We briefly review existing security definitions
related to our problem to motivate the need for a new definition in the
context of the distant attacker. The definition of memory attestation in [10]
considers an experiment where a computationally unbounded adversary
$\mathcal{A}$ produces a computationally bounded prover $\mathcal{P}$ which
represents the state of the device to be attested. The protocol is run between
a verifier $\mathcal{V}$ and $\mathcal{P}$, where $\mathcal{V}$ aims to ensure
that $\mathcal{P}$ is in a desired state; it is deemed secure if a cheating
prover would be caught with high probability. This model has built-in the
device isolation requirement, since the local prover $\mathcal{P}$ does not
interact with $\mathcal{A}$ throughout the protocol. Since we are interested
in memory erasure and not attestation, in addition to strengthening the
attacker model, we may also relax the requirement on the state of the prover,
requiring only that it should utilize enough memory at some point in the
protocol. The definition of secure memory erasure in [28] makes this
relaxation on the prover state. However, as in [10], the prover $\mathcal{P}$
is assumed computationally bounded, which amounts to the device isolation
assumption. In order to lift this assumption, it is not sufficient to simply
make $\mathcal{P}$ computationally unbounded, but we need to consider two
adversaries $\mathcal{A}$ and $\mathcal{P}$ that can communicate throughout
the protocol, and make $\mathcal{A}$’s memory unbounded.

A symbolic Dolev-Yao style model for secure erasure is proposed in [43]. Their
main contribution is a formal proof of the necessity of the distant attacker
assumption in some situations and a construction of a protocol that can be
proven secure symbolically. However, the symbolic model in [43] cannot be used
to quantify the size of the adversarial state, or the adversary’s probability
of success. Hence, it cannot be used to faithfully analyse existing PoSE
protocols, which use information theoretical constructions rather than
symbolic ones.

##  3 A Formal Model for PoSE-DB protocols

In this section, we introduce a class of memory erasure protocols that aim to
resist collusion between a corrupt prover and a distant attacker, and a formal
model that allows to prove their security. We call this class of protocols
_Proofs of Secure Erasure with Distance Bounding_ (PoSE-DB). We denote by
$[n]$ the set $\set{1,\ldots,n}$, by $a\sample A$ the uniformly random
sampling of $a$ from the set $A$ and by $o\leftarrow F(x,\ldots)$ the output
of an algorithm $F$ running on given inputs. For two bitstrings
$a,b\in\set{0,1}^{*}$, we denote by $a\concat b$ their concatenation. An
adversary is a probabilistic Turing machine, generally denoted by
$\mathcal{A}$. It may be endowed with oracles for restricted access to some
resources. In Section 6.1, we will use the random oracle methodology to model
and reason about the access of the adversary to a hash function [12]. An
adversary with access to a (possibly empty) list of oracles $\mathcal{O}$ is
denoted by $\mathcal{A}^{\mathcal{O}}$.

###  3.1 Proof of Secure Erasure with Distance Bounding

The key feature of a PoSE-DB protocol is the use of a distance-bounding
mechanism over several challenge-response rounds to prevent the prover from
outsourcing the erasure proof to the distant attacker. Figure 3 depicts the
generic scheme that we consider for a PoSE-DB protocol. We consider the
following protocol parameters as global constants: block size ($w$), size of
memory in blocks ($m$), number of rounds ($r$) and time threshold ($\Delta$).
The size of the memory to be erased is therefore $m\cdot w$. The time
threshold is chosen at deployment so that the distant attacker assumption
holds within round-trip-time bounded by $\Delta$. In a setup phase which
happens once before the protocol sessions, the verifier is instantiated with
certain additional parameters necessary to run the protocol: the space used to
draw initialization parameters for each session ($\mathcal{I}$, which could be
a set of bitstrings or hash functions) and some auxiliary data ($\rho$) common
for all sessions. Each PoSE-DB session then runs in three phases:

_Initialization phase:_ the local device (playing the role of the prover) has
to perform a prescribed sequence of computation steps and store its result
$\sigma$ in its internal memory. Such a value is meant to fill the prover’s
memory, leaving no room for data previously stored in the device.

_Interactive phase:_ verifier and prover interact over a number of challenge-
response rounds; the verifier measures the round-trip-time of those exchanges
and stores all the challenges and their corresponding responses.

_Verification phase:_ the verifier accepts the proof if all challenge-response
pairs from the interactive phase satisfy a prescribed verification test, and
if the round-trip-times are below the time threshold $\Delta$.

Prover[ρ] Verifier[ρ, $\mathcal{I}$] [dotted] Initialisation phase σ ←
Precmp(ρ, Υ) *Υ Υ $\mathcal{I}$[dotted] Interactive phase for i:=1  to r x_i ←
Chal(ρ)
*x_i t^b_i ← clock()
y_i ← Resp(ρ,σ, x_i) *y_i t^e_i ← clock() [dotted] Verification phase ∀ i :
Vrfy(ρ, Υ, x_i, y_i) =
∀ i : t^e_i - t^b_i < Δ

Figure 3: PoSE-DB protocol session

Notice that there are no identities exchanged during the protocol, nor pre-
shared cryptographic material. Like in existing software-based memory
attestation and erasure protocols, we assume the existence of an out-of-the-
band authentication channel, such as visual inspection, that allows the
verifier to identify the prover. In Definition 1, we formally specify PoSE-DB
protocols as a set of algorithms to be executed by the prover and the
verifier. We do not specify the way in which messages are exchanged or the
time verification step. These are handled by the security definition as
described below, considering a Dolev-Yao model with a distant attacker that
cannot act within the challenge-response round.

######  Definition 1.

A _proof of secure erasure with distance bounding_ (PoSE-DB) protocol is
defined by a tuple of algorithms
$\sequence{\mathsf{Setup},\mathsf{Precmp},\mathsf{Chal},\mathsf{Resp},\mathsf{Vrfy}}$
and parameters $\sequence{m,w,r,\Delta}$ as illustrated in Figure 3. We have:

  * •

$(\rho,\mathcal{I})\leftarrow\mathsf{Setup}(m,w)$: computes some data $\rho$
necessary to run the protocol and a parameter space $\mathcal{I}$ to be used
for instantiating protocol sessions;

  * •

$\Upsilon\sample\mathcal{I}$: sample data uniformly from $\mathcal{I}$ for
each protocol session; some protocols may instantiate a hash function at this
step;

  * •

$\sigma\leftarrow\mathsf{Precmp}(\rho,\Upsilon)$: computes a value of size
$m\cdot w$, to be stored in memory;

  * •

$x\leftarrow\mathsf{Chal}(\rho)$: generates a uniformly random challenge;

  * •

$y\leftarrow\mathsf{Resp}(\rho,\sigma,x)$: computes the response to the
challenge. This should be a very-lightweight operation consistent with the
design principles of distance bounding, such as a lookup operation.

  * •

$\mathsf{Vrfy}(\rho,\Upsilon,x,y)$: determines if $y$ is the correct response
to challenge $x$

######  Example 1.

As a running example, consider the simple idea (similar to Perito and Tzudik’s
protocol [37]) of filling the memory of the device with random data, then
challenging it to return randomly chosen blocks of that data during the
interactive phase. We call this the _unconditional PoSE-DB protocol_, as its
security proof in Section 5 does not rely on cryptographic assumptions. For
such a protocol, the parameter space $\mathcal{I}$ is set to $\bin^{m\cdot
w}$. This means that every protocol session will start with a random sequence
of length $\bin^{m\cdot w}$, which is equal to the memory size of the prover.
The complete specification of this protocol is as follows.

######  Definition 2 (The unconditional PoSE-DB protocol).

  * •

$\mathsf{Setup}(m,w)$: return $\rho=\emptyset,\leavevmode\nobreak\
\mathcal{I}=\bin^{m\cdot w}$

  * •

$\psi\sample\bin^{m\cdot w}$

  * •

$\mathsf{Precmp}(\rho,\psi)$: parse $\psi\text{ as }t_{1}\concat\ldots\concat
t_{m}$ with $t_{i}\in\bin^{w}$, and return $\sigma=t_{1}\concat\ldots\concat
t_{m}$

  * •

$\mathsf{Chal}(\rho)$: return $x\sample[m]$

  * •

$\mathsf{Resp}(\rho,\sigma,x)$: return $t_{x}$, which was stored in $\sigma$

  * •

$\mathsf{Vrfy}(\rho,\psi,x,y)$: return true if and only if $y=t_{x}$

Note that the erasure procedure itself running on the local device cannot be
overwritten by $\sigma$. Hence, in practice, the device should allocate memory
to store and execute the erasure procedure, and the goal should be for this
procedure to introduce minimal memory overhead. This is a necessary condition
in any memory erasure protocol. The erasure procedure for the unconditionally
secure protocol consists in simply storing and fetching blocks from the
memory. We expect its memory overhead to be minimal. For the graph-based
protocol that we introduce in Section 6, the in-place property we devise for
the graph in Section 7 is aimed at keeping this overhead as small as possible.

###  3.2 Formalizing Secure Erasure Against Distant Attackers

[msc keyword=, draw frame = none, instance distance=3cm,head top distance=0cm,
foot distance=0cm,first level height=0cm, environment distance=0cm,foot
height=0cm, level height=0.4cm, label distance=0.5ex] v$V$ p$\mathcal{A}_{1}$
a$\mathcal{A}_{0}$ [1] $\Upsilon$vp *$\Upsilon$pa [2] $\sigma_{1}$ap
$x_{1}$vp[1] [l]$\Delta$vv[3] [1] *$x_{1}$pa[1] [1] $y_{1}$pv[1] [1]
[l]$\Delta$vv[3] $\sigma_{2}$ap $x_{2}$vp[1] [1] *$x_{2}$pa[1] [1]
$y_{2}$pv[1] [1] $\sigma_{3}$ap

Figure 4:  The y-axis denotes a timeline. Because $A_{0}$ is far, $A_{1}$
cannot relay the verifier’s challenge to $A_{0}$ and wait for a response.
$A_{0}$ does help $A_{1}$ in the other phases of the protocol execution.

To define secure erasure, we formally split the adversary in two: we use
$\mathcal{A}_{0}$ to denote the distant attacker, and $\mathcal{A}_{1}$ to
denote the local (possibly corrupt) device. Like in a Dolev-Yao model, our
adversary $\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ is in full control
of the network and can corrupt agents. It can eavesdrop, inject and modify
messages sent to the network. One limitation for the pair of attackers is
given by the physical constraints of the communication medium, which are
leveraged by the distance-bounding mechanism, and the assumption that
$\mathcal{A}_{0}$ is distant, i.e. sufficiently far from the device. In our
security definition we abstract away from the distance-bounding check by not
letting $\mathcal{A}_{0}$ act between the sending of the challenge and the
receipt of the corresponding response in each round. The intuition of this
abstraction is illustrated in Figure 4: because $\mathcal{A}_{0}$ is far and
the function $\mathsf{Resp}$ should be computed fast, $\mathcal{A}_{0}$ does
not have time to respond to the verifier’s challenge in time. We do allow
$\mathcal{A}_{0}$, before each round of the fast phase, to precompute some
state $\sigma_{i}$ to be used by $\mathcal{A}_{1}$ during the $i$th round of
the fast phase. Assuming that $\sigma_{i}$ is computed by $\mathcal{A}_{0}$ is
without loss of generality, since $\mathcal{A}_{0}$ is unbounded and has at
least as much knowledge as $\mathcal{A}_{1}$, which forwards all information
to $\mathcal{A}_{0}$. Therefore, we assume that right before the challenge
$x_{i}$, the attacker’s available memory on the device is filled by
$\sigma_{i}$ and this is the only information that $\mathcal{A}_{1}$ can use
to compute the response in the $i$th round of the fast phase.

(ρ,$\mathcal{I}$) ← Setup(m,w); Υ $\mathcal{I}$
---
i:=1  to r :
σ_i ← A_0(1^w,ρ,Υ,x_j | j < i)
x_i← Chal(ρ); y_i ← A_1^O(1^w,ρ,σ_i,x_i)
∀ i : Vrfy(ρ,Υ, x_i,y_i)=
Figure 5: Security experiment
$\mathsf{Exp}^{m,r,w}_{\mathcal{A}_{0},\mathcal{A}_{1}}$.

Figure 5 formalizes the environment described above in the form of a security
experiment. As $\mathcal{A}_{1}$ is acting within the fast phase, we may bound
its number of computation steps. This is especially interesting for protocols
that may rely on computational security assumptions. The only computational
assumption that we will use in this paper is the random oracle assumption for
two of our three protocols. Therefore, in the security definition, if
$\mathcal{A}_{1}$ has access to a hash function, we will restrict its use
through an oracle and will count the number of calls $\mathcal{A}_{1}$ makes
to it. This restriction is formalized by the parameter $q$ in Definition 3
that bounds resources for an adversary. A second parameter in this definition
is $M$, which bounds the size of the memory used by $\mathcal{A}$ on the
device throughout the protocol, i.e. the maximum value of $\sigma_{i}$ in the
security experiment. We consider an attacker successful if it passes the
protocol while not erasing a significant proportion of the $m\cdot w$ bits of
memory on the device. Assume the portion of memory that is needed by the
adversary to store malware or any other information is $y$. If the adversary
needs to use more than $m\cdot w-y$ bits to successfully execute the protocol,
then the device becomes “clean”, as the memory required by the attacker is
erased. Therefore, the goal of the attacker is to use at most $M=m\cdot w-y$
bits of space during the protocol execution.

######  Definition 3.

An adversary $\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ against the
memory challenge game is called _$(M,q)$ -bounded_ if and only if in any
execution of $\mathsf{Exp}^{m,r,w}_{\mathcal{A}_{0},\mathcal{A}_{1}}$ and any
round $i$ we have that $|\sigma_{i}|\leq M$ and $\mathcal{A}_{1}$ makes at
most $q$ queries to $\mathcal{O}$.

To evaluate the security of a given PoSE-DB protocol, we will consider the
class of $(M,q)$-bounded adversaries and determine the probability of any
adversary from this class to win the security game.

######  Definition 4 (PoSE-DB security).

Assume some fixed parameters $(m,r,w)$ for the experiment from Figure 5. An
adversary $(\mathcal{A}_{0},\mathcal{A}_{1})$ _wins the memory-challenge game_
with probability $\zeta$ if and only if
$\prob{\mathsf{Exp}^{m,r,w}_{\mathcal{A}_{0},\mathcal{A}_{1}}=\text{true}}=\zeta$,
where probability is taken over the randomness used by the experiment.

There are similarities between our security definition presented above and the
definition of secure proof of space [21, 38], the main difference being that
in proofs of space $\mathcal{A}_{1}$ is isolated from $\mathcal{A}_{0}$ in the
interactive challenge phase. We discuss more details about this relation and
our modelling choices in the appendix.

##  4 Initial results

Before specifying and analysing our three PoSE-DB protocols, we provide useful
initial results on the security of PoSE-DB protocols in general. Concretely,
we show that PoSE-DB security increases proportionally to the number of
rounds. This will allow us to simplify the security analysis by proving a
level of security for the protocol executed in a single round, and then
generically deriving the corresponding security guarantees over multiple
rounds. Throughout all our proofs we consider deterministic adversaries
$\mathcal{A}$. This is without loss of generality: since our security
definition upper-bounds the success probability of $\mathcal{A}$, we can
always consider that $\mathcal{A}$ is initialized with its best random tape.
In this setting, by fixing its best-case random-tape, we can consider
$\mathcal{A}$ deterministic. This idea is well known and has been applied
elsewhere [44]. Note that we still have randomness left in the security
experiment, coming from probabilistic choices in honest algorithms and the
random oracle.

Let $\Upsilon$ be an element from the initialization space $\mathcal{I}$ of a
PoSE-DB protocol. For an adversary
$\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$, denote by
$\underset{\Upsilon\sample\mathcal{I}}{\operatorname{\probname}}[\mathcal{A}^{r}]$
the probability that $\mathcal{A}$ wins the memory game with $r$ rounds. For a
fixed $\Upsilon$, we denote the corresponding winning conditional probability
by $\condprob{\mathcal{A}^{r}}{\Upsilon}$. We say that an adversary
$\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ playing the memory challenge
game with fixed $\Upsilon\in\mathcal{I}$ is _uniform_ if, for any sequence of
challenges $x_{1},\ldots,x_{r}$, $\mathcal{A}_{0}$ returns the same state
$\sigma_{i}$ in each round, i.e. $\sigma_{1}=\cdots=\sigma_{r}$. The following
lemma allows us to focus on uniform adversaries when proving the security of a
PoSE-DB protocol. The main idea of the proof is that, since the challenge in
each round is chosen independently, the best that $\mathcal{A}_{0}$ can do in
any round is to choose a state $\sigma_{\mu}$ that maximizes the success
probability of $\mathcal{A}_{1}$ for a random challenge. The proof of this
lemma is in the appendix. The same holds for all results we state without
proof in the rest of this work.

######  Lemma 1.

For any $(M,q)$-bounded adversary $\mathcal{A}$ against the PoSE-DB security
experiment, there is a uniform $(M,q)$-bounded adversary $\bar{\mathcal{A}}$
that wins the experiment with at least the same probability:
$\underset{\Upsilon\sample\mathcal{I}}{\operatorname{\probname}}[\mathcal{A}^{r}]\leq\underset{\Upsilon\sample\mathcal{I}}{\operatorname{\probname}}[\bar{\mathcal{A}}^{r}]$.

###### Proof.

It is sufficient to prove that, for any fixed $\Upsilon\in\mathcal{I}$, we
have
$\condprob{\mathcal{A}^{r}}{\Upsilon}\leq\condprob{\bar{\mathcal{A}}^{r}}{\Upsilon}$.
In this case, since $\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ is
deterministic and $\Upsilon$ is fixed, for every $i$ the state$\sigma_{i+1}$
returned by $\mathcal{A}_{0}$ is uniquely determined by the sequence of
challenges $x_{1},\ldots,x_{i}$ in the experiment
$\mathsf{Exp}^{m,r,w}_{\mathcal{A}_{0},\mathcal{A}_{1}}$. Let $\Sigma$ be the
set of all possible states $\sigma_{i}$ that can be output in any round by
$\mathcal{A}_{0}$ over all possible sequences of challenges. We denote by
$\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma}$ the probability that
$\mathcal{A}_{1}$ answers a single challenge correctly when given the state
$\sigma$ as input:

$\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma}=\condprob{\mathsf{Vrfy}(\rho,\Upsilon,x,y)}{\begin{subarray}{c}x\leftarrow\mathsf{Chal}(\rho)\\\
y\leftarrow\mathcal{A}_{1}^{\mathcal{O}_{h}}(1^{w},\rho,\sigma,x)\end{subarray}}$

where the probability is taken over the randomness used by the challenge
generation algorithm. We define $\sigma_{\mu}$ to be the state in $\Sigma$ for
which the probability of winning given a random challenge is maximal
$\sigma_{\mu}=\argmax_{\sigma\in\Sigma}\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma}$.
Let $\bar{\mathcal{A}}=(\bar{\mathcal{A}_{0}},\mathcal{A}_{1})$, where
$\bar{\mathcal{A}_{0}}$ always returns $\sigma_{\mu}$, independent of the set
of challenges it obtains as input. Note that $\bar{\mathcal{A}}$ is
$(M_{0},q)$-bounded, since the state returned by $\bar{\mathcal{A}_{0}}$ is
among the possible states returned by $\mathcal{A}_{0}$, and the adversary
$\mathcal{A}_{1}$ is the same. We will now show that $\bar{\mathcal{A}}$
achieves at least the same probability of success as $\mathcal{A}$. If
$\bar{x}_{k}$ is a sequence of challenges $\set{x_{1},x_{2},\ldots,x_{k}}$ we
denote by:

  * •

$\condprob{\mathcal{A}^{k}}{\Upsilon,\bar{x}_{k}}$ the probability that the
adversary $\mathcal{A}$ gets a correct answer in the first $k$ rounds given
that the first $k$ challenges are $\bar{x}_{k}$. As $\mathcal{A}$ is
deterministic, this probability is either $0$ or $1$.

  * •

$\condprob{\mathcal{A}^{t}(\bar{x}_{k})}{\Upsilon,\bar{x}_{k}}$ the
probability that the adversary $\mathcal{A}$ gets a correct answer in $t$
successive rounds starting from round $k+1$ given that the challenges in the
first $k$ rounds are $\bar{x}_{k}$.

  * •

$\condprob{\bar{x}_{k}}{\Upsilon}$ the probability, taken over the randomness
used by the challenge algorithm, that the first $k$ challenges are
$\bar{x}_{k}$.

For a vector of challenges $\bar{x}_{k}$ we have
$\condprob{\mathcal{A}^{1}(\bar{x}_{k})}{\Upsilon,\bar{x}_{k}}=\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma,\bar{x}_{k}}$
where $\sigma\leftarrow\mathcal{A}_{0}(\bar{x}_{k})$ and:

$\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma,\bar{x}_{k}}=\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma}\leq\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma_{\mu}}$

where the equality comes from the independence between $A_{1}$ and
$\bar{x}_{k}$ given $\Upsilon,\sigma$; the inequality follows by definition of
$\sigma_{\mu}$. Using the inequality above, we prove by induction that, for
any $k\geq 0$, we have
$\condprob{\mathcal{A}^{k+1}}{\Upsilon}\leq\condprob{\bar{\mathcal{A}}^{k+1}}{\Upsilon}$.
The case $k=0$ is trivial. For $k>1$, we obtain:

$\begin{split}\condprob{\mathcal{A}^{k+1}}{\Upsilon}&=\sum_{\bar{x}_{k}}\condprob{\bar{x}_{k}}{\Upsilon}\cdot\condprob{\mathcal{A}^{k}}{\Upsilon,\bar{x}_{k}}\cdot\condprob{\mathcal{A}^{1}(\bar{x}_{k})}{\Upsilon,\bar{x}_{k}}\\\
&\leq\sum_{\bar{x}_{k}}\condprob{\bar{x}_{k}}{\Upsilon}\cdot\condprob{\mathcal{A}^{k}}{\Upsilon,\bar{x}_{k}}\cdot\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma_{\mu}}\\\
&=\condprob{\mathcal{A}^{k}}{\Upsilon}\cdot\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma_{\mu}}\\\
&\leq\condprob{\bar{\mathcal{A}}^{k}}{\Upsilon}\cdot\condprob{\mathcal{A}_{1}}{\Upsilon,\sigma_{\mu}}=\condprob{\bar{\mathcal{A}}^{k+1}}{\Upsilon}\qed\end{split}$

Next, we show that there is a direct relationship between the winning
probability of an adversary in one round and the winning probability in
multiple rounds. The analysis is simplified by the fact that we can focus on
uniform adversaries, according to Lemma 1. If the initialization parameters
are fixed, it follows immediately that running the experiment for $r$ rounds
exponentially decreases the cheating ability of the adversary.

######  Lemma 2.

For any uniform adversary $\mathcal{A}$ and any $\Upsilon\in\mathcal{I}$, we
have
$\condprob{\mathcal{A}^{r}}{\Upsilon}=\condprob{\mathcal{A}^{1}}{\Upsilon}^{r}$.

###### Proof.

$\condprob{\mathcal{A}^{r}}{\Upsilon}=\condprob{\mathcal{A}^{r}}{\Upsilon,\sigma\leftarrow\mathcal{A}_{0}}=\condprob{\mathcal{A}}{\Upsilon}^{r}\qed$

When lifting this lemma to uniformly chosen parameters from $\mathcal{I}$, it
will be necessary to account for the fact that the (one-round) adversary may
be lucky on a small proportion of those random choices. The following
definition and proposition tolerate this, by bounding the success probability
of the adversary only for a subset of good parameters, and showing the effect
after $r$ rounds.

######  Definition 5.

For a set $\mathcal{I}_{\mathsf{good}}\subseteq\mathcal{I}$ and a value
$\zeta<1$, we say that $\mathcal{A}$’s _winning probability is bounded by
$\zeta$ within $\mathcal{I}_{\mathsf{good}}$_ if and only if
$\forall\Upsilon\in\mathcal{I}_{\mathsf{good}}\colon\condprob{\mathcal{A}^{1}}{\Upsilon}\leq\zeta$.

If the proportion of cases $\mathcal{I}\setminus\mathcal{I}_{\mathsf{good}}$
in which the adversary is lucky is negligible, then for a large enough number
of rounds the success probability of the adversary is also negligible, as
shown by the next proposition.

######  Proposition 1.

Given $\zeta<1$, $\mathcal{I}_{\mathsf{good}}\subseteq\mathcal{I}$ and a
uniform adversary $\mathcal{A}$ whose winning probability is bounded to
$\zeta$ within $\mathcal{I}_{\mathsf{good}}$, we have
$\underset{\Upsilon\sample\mathcal{I}}{\operatorname{\probname}}[\mathcal{A}^{r}]\leq\zeta^{r}+\frac{|\mathcal{I}\setminus\mathcal{I}_{\mathsf{good}}|}{|\mathcal{I}|}$.

###### Proof.

From Lemma 2, we have:

$\underset{\Upsilon\sample\mathcal{I}}{\operatorname{\probname}}[\mathcal{A}^{r}]=\frac{1}{|\mathcal{I}|}\sum_{\Upsilon\in\mathcal{I}}\condprob{\mathcal{A}^{r}}{\Upsilon}=\frac{1}{|\mathcal{I}|}\sum_{\Upsilon\in\mathcal{I}}\condprob{\mathcal{A}}{\Upsilon}^{r}$

To reduce notation in what follows, we let
$p_{\Upsilon}=\condprob{\mathcal{A}}{\Upsilon}$ and omit
$\Upsilon\in\mathcal{I}$ when we sum over all $\Upsilon$ in $\mathcal{I}$. We
have:

$\begin{split}&\sum_{\Upsilon}\condprob{\mathcal{A}}{\Upsilon}^{r}=\sum_{\Upsilon}p_{\Upsilon}^{r}=\sum_{\Upsilon,p_{\Upsilon}>\zeta}p_{\Upsilon}^{r}+\sum_{\Upsilon,p_{\Upsilon}\leq\zeta}p_{\Upsilon}^{r}\\\
&\leq\sum_{\Upsilon,\leavevmode\nobreak\
p_{\Upsilon}>\zeta}1+\sum_{\Upsilon}\zeta^{r}\leq\sum_{\begin{subarray}{c}\Upsilon,\leavevmode\nobreak\
p_{\Upsilon}>\zeta\\\
\Upsilon\in\mathcal{I}_{\mathsf{good}}\end{subarray}}1+\sum_{\begin{subarray}{c}\Upsilon,\leavevmode\nobreak\
p_{\Upsilon}>\zeta\\\
\Upsilon\notin/I_{\mathsf{good}}\end{subarray}}1+\sum_{\Upsilon}\zeta^{r}\\\
&\leq
0+|\mathcal{I}\setminus\mathcal{I}_{\mathsf{good}}|+|\mathcal{I}|\cdot\zeta^{r}\end{split}$

where for the last inequality we use that $\mathcal{A}$’s winning probability
is bounded to $\zeta$ within $\mathcal{I}_{\mathsf{good}}$ to deduce that the
first sum is empty. Combining the two results above, we deduce
$\underset{\Upsilon\sample\mathcal{I}}{\operatorname{\probname}}[\mathcal{A}^{r}]\leq\zeta^{r}+\frac{|\mathcal{I}\setminus\mathcal{I}_{\mathsf{good}}|}{|\mathcal{I}|}$
as claimed. ∎

##  5 The unconditional PoSE-DB protocol

This section provides the security analysis for the unconditional PoSE-DB
protocol presented in Section 3, Definition 2. Since this protocol does not
use any hash function, the bound on the number of oracle calls by
$\mathcal{A}_{1}$ is not relevant. Such an adversary is $(M,\infty)$-bounded.
As a consequence, there is no computational bound on the adversary
$\mathcal{A}_{1}$, but only a memory bound. Recall that the value $y=m\cdot
w-M$ is the amount of memory that the adversary cannot erase (where it may
store malware).

######  Theorem 1.

Assume that the unconditional PoSE-DB protocol is instantiated with parameters
$(m,1,w)$. Let $\mathcal{A}$ be any adversary with measure $(M,\infty)$. Then,
there exists a set $\mathcal{I}^{1}_{\mathsf{good}}\subseteq\mathcal{I}$ such
that $\mathcal{A}$’s winning probability is bounded to $1-m^{-1}$ within
$\mathcal{I}^{1}_{\mathsf{good}}$ and
$\abs{\mathcal{I}^{1}_{\mathsf{good}}}\geq 2^{m\cdot w}\cdot(1-2^{-y})$.
Furthermore, if $y\geq m+w$, then there exists a set
$\mathcal{I}^{2}_{\mathsf{good}}\subseteq\mathcal{I}$ such that
$\mathcal{A}$’s winning probability is bounded to
$1-\left\lceil\frac{y-m-w+1}{w}\right\rceil m^{-1}$ within
$\mathcal{I}^{2}_{\mathsf{good}}$ and
$\abs{\mathcal{I}^{2}_{\mathsf{good}}}\geq 2^{m\cdot w}\cdot(1-(m^{2}+m)\cdot
2^{-w})$.

###### Proof.

Let $\sigma$ be a bitstring of size $M$. Let
$R_{\sigma}=\\{\psi_{1},\ldots\psi_{k}\\}$ be the set of all bitstrings such
that $\mathcal{A}_{0}(1^{w},\rho,\psi_{i})=\sigma$. We will lower-bound the
number of queries related to elements in $R_{\sigma}$ for which
$\mathcal{A}_{1}$ gives an incorrect answer. To prove the first result, we
count for how many bitstrings there is at least one error. Call this set
$\mathcal{I}^{1}_{\mathsf{good}}$. Let $\psi^{\prime}$ be the concatenation of
the blocks in
$\\{\mathcal{A}_{1}(1^{w},\rho,\sigma,1),\ldots,\mathcal{A}_{1}(1^{w},\rho,\sigma,m)\\}$,
i.e. a bitstring of size $m\cdot w$. Since $\psi^{\prime}$ can be equal to at
most one string in $R_{\sigma}$, $\mathcal{A}_{1}$ is wrong for at least one
input $q\in\set{1,\ldots,m}$ for at least $\abs{R_{\sigma}}-1$ of the
bitstrings in $R_{\sigma}$. Summing up for all possible sets $R$ and for all
possible $\sigma$, we deduce that $\mathcal{A}_{1}$ is wrong for at least one
query w.r.t. at least $2^{m\cdot w}-2^{m\cdot w-y}$ bitstrings (as there are
at most $2^{m\cdot w-y}$ different sets $R_{\sigma}$). We obtain
$\abs{\mathcal{I}^{1}_{\mathsf{good}}}\geq 2^{m\cdot w}\cdot(1-2^{-y})$ and:

$\forall
r\in\mathcal{I}^{1}_{\mathsf{good}}\colon\underset{q\sample[n]}{\operatorname{\probname}}[\mathcal{A}_{1}(1^{w},\rho,\sigma,q)\text{
is correct}\,\left|\,\sigma\vphantom{q\sample[n]}\right.]\leq 1-m^{-1}$

where $\sigma\leftarrow\mathcal{A}_{0}(1^{w},\rho,\psi)$. For a proof of the
second result of the theorem, see Section 10.3. ∎

From Proposition 1 and Theorem 1, we obtain:

######  Corollary 1.

If we execute the unconditional PoSE-DB protocol for $r$ rounds in presence of
any $(M,\infty)$-bounded adversary, then
$\prob{\mathsf{Exp}^{m,r,w}_{\mathcal{A}_{0},\mathcal{A}_{1}}=\leq{(1-m^{-1})}^{r}+2^{M-m\cdot
w}$.Furthermore,when$M\leq m\cdot
w-m-w$theboundimprovesto${(1-\left\lceil\frac{m\cdot w-m-
w-M+1}{w}\right\rceil\cdot m^{-1})}^{r}+m\cdot(m+1)\cdot
2^{-w}$.\end{corollary}}$

##  6 PoSE based on depth-robust graphs

While the unconditional PoSE-DB protocol offers interesting security
properties, it comes at the cost of a high communication complexity, since the
verifier needs to transmit a nonce of length equal to the size of the prover’s
memory. This section offers an alternative protocol where the prover computes
the labelling of a graph in its memory, starting from a small random seed
transmitted by the verifier.

###  6.1 Graph-based notation and PoSE scheme

We first introduce the general notion of graph-labelling and discuss its use
in the literature. We let $H$ be the set of all functions from
$\set{0,1}^{\kappa}$ to $\set{0,1}^{w}$, for a suitably large $\kappa$. Each
new session of the protocol will rely on a hash function $h$ instantiated
randomly from this set. Elements from the set $H$ are also called random
oracles, since we will make the random oracle assumption for $h$ drawn from
this set. Given a directed acyclic graph (DAG) $G$, the list of successors and
predecessors of the node $v$ in $G$ are respectively $\Gamma^{+}(v)$ and
$\Gamma^{-}(v)$. If $\Gamma^{-}(v)=\emptyset$ then $v$ is an input node. For a
node $v$ of $G$, we let $\mathsf{llp}(v,G)$ be the length of the longest path
in $G$ that ends in $v$. If $R\subseteq V(G)$, we denote by $G\setminus R$ the
graph obtained after removing the nodes in $R$ and keeping all edges between
the remaining nodes.

######  Definition 6.

Given a hash function $h$ and a DAG $G$, $l\colon V(G)\to{\\{0,1\\}}^{w}$ is
an $h$-labeling of $G$ if and only if for each $v\in V(G)$:

$l(v)\coloneqq h(v\concat l(v_{1})\concat\ldots\concat l(v_{d}))$

where $\sequence{v_{1},\ldots,v_{d}}=\Gamma^{-}(v)$. If a node $v$ has no
predecessor, then $l(v)=h(v)$. We also let
$\ell^{-}(v)=v||\ell(v_{1})||\ldots||\ell(v_{d})$.

Graph labelling as defined above is a well established technique used in
protocols for proofs of space [21, 11, 38], memory hardness [5, 6, 2, 3, 4]
and classic secure erasure [22, 28]. The typical structure of these protocols
is as follows:

  * •

the verifier sends a nonce to the prover, which is used as a seed to determine
the hash function $h$;

  * •

the prover uses $h$ to compute the labelling of an agreed-upon graph $G$, and
stores a subset of the resulting labels, denoted $O(G)$;

  * •

the verifier challenges the prover to reply with the labels of several
randomly chosen vertices in the graph, and accepts the proof if these labels
are correct.

Let $m$ be the size of $O(G)$ in words. The general goal of this technique is
to ensure that any cheating prover that uses less than $m$ words of memory to
compute the responses can only do so correctly by paying a noticeable amount
of computational time. This has been achieved by using depth-robust graphs
[24, 38], which are graphs that contain _at least one long path_ , even if a
significant proportion of nodes have been removed. Intuitively, in the
corresponding protocol, this means that the label for at least one of the
verifier challenges will be hard to compute if the prover has cheated.

Given a DAG $G_{m}$, a hash function $h\in H$ (which we model as a random
oracle) and a list of nodes $O(G_{m})\subseteq V(G_{m})$ of size $m$, we
define our remote memory erasure protocol as follows:

  * •

$\mathsf{Setup}(m,w)$: return $\rho=(G_{m},O(G_{m})),\leavevmode\nobreak\
\mathcal{I}=H$

  * •

$h\sample H$

  * •

$\mathsf{Precmp}(\rho,h)$: compute the labels of the nodes in $O(G_{m})$, and
output the concatenation of these labels $\sigma=l(o_{1})\concat\ldots\concat
l(o_{m})$ where $\sequence{o_{1},\dots,o_{m}}=O(G_{m})$

  * •

$\mathsf{Chal}(\rho)$: return a random vertex in $O(G_{m})$

  * •

$\mathsf{Resp}(\rho,\sigma,x)$: responds with $l(x)$, which was stored in
$\sigma$

  * •

$\mathsf{Vrfy}(\rho,h,x,y)$: return true if and only if $y=l(x)$

In order to prove our graph based PoSE-DB secure, there are several issues we
need to address. First, as we need fast responses, our verifier can query only
one random challenge node per round. This means that it is not sufficient to
have a single long path in the graph in order to catch a cheating prover; we
will thus strengthen the depth-robustness property to require _at least a
certain number of long paths_ to be present. Another constraint, particularly
relevant to memory erasure, is that we should be able to compute the graph
labelling with minimal memory overhead, so that as much memory as possible can
be erased from the device. We call this property _in-place_ , since
intuitively it means that the set of labels to be stored should be computed in
almost the same amount of space as their total size. To our knowledge, no
graph in the literature exists that satisfies these two properties. We design
one in Section 7.

######  Definition 7.

A graph $G$ can be labelled in-place with respect to a list of nodes
$O(G)\subseteq V(G)$ if and only if there is an algorithm that outputs the
list of labels for all nodes in $O(G)$ using at most $\abs{O(G)}\cdot
w+\mathcal{O}(w)$ bits of memory.

A second issue that we address lies in the tightness of the security bound,
i.e. how big is the gap between the memory erased by a cheating prover and the
memory it is supposed to erase. In our case study, this gap could be used to
store malware, so it should be as small as possible. We improve upon previous
security bounds for protocols based on graph labelling, first by performing a
fine-grained and formal security analysis, and second by identifying a
restricted class of adversaries, that simplifies the proofs while also further
improving the security bound. We relate this class to previous restrictions in
this area and argue that it is a strictly more general notion, resulting in
weaker restrictions for the adversary and therefore stronger security
guarantees.

###  6.2 Depth-robustness is sufficient for security

We show that a variation of the classic graph depth-robustness property [24,
38] is sufficient to prove security for the PoSE scheme from Section 6.1. As
explained above, while depth-robustness in all previous works requires the
existence of one single long path after some nodes have been removed, we
require the existence of several long paths. The computation required by a
cheating prover in this context is proportional to the depth of the longest
remaining path. While in most previous works the length is linear in the size
of the graph, we will tolerate graphs with slightly shorter paths, i.e. of
sublinear size. On the one hand, this is useful in practice, since it will
allow us to construct a class of depth-robust graphs that can be labelled in-
place efficiently. On the other hand, we show that this does not affect
security, as long as the computational power of the adversary during the
interactive phase is constrained in proportion to the prescribed path length,
which can be done by the time measurements we described in Section 3.

######  Definition 8.

Let $G$ be a DAG and let $O(G)\subseteq V(G)$ with $\abs{O(G)}=\mu$. We say
$G$ is $(\mu,\gamma)$-depth-robust with respect to $O(G)$ if and only if for
every set $R\subset V(G)$ s.t. $\abs{R}<\mu$ there exists a subset of nodes
$O^{\prime}\subseteq O(G)$ with $\abs{O^{\prime}}\geq\mu-\abs{R}$ such that
for every node $v\in O^{\prime}$ there is a path in $G\setminus R$ of length
at least $\gamma$ that ends in $v$, i.e. $\mathsf{llp}(v,G\setminus
R)\geq\gamma$.

The security bounds obtained using such a depth-robust graph in the graph-
based PoSE scheme are presented in Corollary 2, which can be obtained by a
direct application of Theorem 2 and Proposition 1. For this protocol, the
oracle $\mathcal{O}$ in Figure 5 gives to $\mathcal{A}_{1}$ oracle access to
the hash function $h$ resulting from the initialization phase. The first part
of Corollary 2 shows that we obtain better security bounds if we consider a
notion of graph-restricted adversaries, which will be discussed in the next
subsection. Note that the parameter $m$ for the number of memory blocks in the
experiment and the bound $q<\gamma$ on the number of oracle calls by
$\mathcal{A}_{1}$ are related to the pair $(m,\gamma)$ determined by the
depth-robustness of the graph.

######  Corollary 2.

Assume that the graph-based PoSE scheme is instantiated with parameters
$(m,r,w)$ and an $(m,\gamma)$-depth-robust graph $G$. Then, for any
$(M,q)$-bounded adversary $(\mathcal{A}_{0},\mathcal{A}_{1})$, with
$q<\gamma$, we have:

$\underset{h}{\operatorname{\probname}}[\mathsf{Exp}^{m,r,w}_{\mathcal{A}_{0},\mathcal{A}_{1}}=\leq{\left(M^{\prime}/m\right)}^{r}+2^{-w_{0}}\text{
where:}$

  * •

if $\mathcal{A}$ is _graph-restricted_ : $w_{0}=w$ and $M^{\prime}=\left\lceil
M/w\right\rceil$

  * •

else: $w_{0}=w-\log(m)-\log(q)$ and $M^{\prime}=\left\lceil
M/w_{0}\right\rceil$

Intuitively, the previous result shows that the attacker’s success probability
is proportional to $M$: the smaller the state it uses to reply to our
challenges, the higher the probability that it will fail to pass the
verification test. This result is not far from optimal, as this bound can
actually be achieved by an adversary that stores $\frac{M}{w}$ of the labels
in $O(G)$. For example, if we would like to erase a malware of size at least
$6$ KB from a device with total memory $100$ KB, then the parameters would be
$w=256,m=100\cdot 2^{13}/256=3200,M=(100-5)\cdot 2^{13}=778240$. If we wanted
to be certain that any graph-restricted attacker can pass the protocol without
erasing malware with probability at most $10^{-3}$, then we need to execute
the protocol for $112$ rounds.

###  6.3 Graph-restricted adversary

Several works studying protocols based on graph labelling related to ours
consider restricted classes of adversaries in order to obtain tight security
bounds and reductions to graph pebbling [20, 21, 5]. In all these notions, the
adversary can only make oracle calls corresponding to valid labels in the
graph and, in addition, the adversary is restricted in the type of computation
that it can apply to get a state to be stored in memory, e.g. it can only
store labels [20, 21] or so-called entangles labels [5]. The notion that we
consider in Definition 9 is more general, considering the full class of graph-
restricted adversaries that can perform any computation to obtain the state to
be stored.

######  Definition 9.

We say that $\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ is _graph-
restricted to_ $G$ if and only if all oracle calls done by $\mathcal{A}_{1}$
correspond to valid labels (equal to $\ell^{-}(v)$ for some node $v$), and its
responses to the verifier challenges are always correct.

A graph-restricted adversary may compute arbitrary functions (for example
compression, cut labels into pieces, entangle them with new algorithms, etc),
but it doesn’t do any guessing while making oracle queries nor when responding
challenges. The assumption is that the adversary knows what it is doing, i.e.
knows that an oracle query would be useless or that a particular response to
the challenge would be wrong. The notable difference with respect to the
previous classes of graph-playing adversaries, e.g. the pebbling adversary
from [21] or the entangled pebbling adversary from [5], is that we have no a
priori restriction on how the labels of values are processed and stored. We
discuss these notions in more detail in Section 10.1.

###  6.4 Security proof: first step

The following theorem will be the main ingredient for proving Corollary 2. We
split its proof in two steps. The first step is presented in this subsection
and is independent of the adversarial class. The second step is simpler for
graph-restricted adversaries. We present the proof for that case in the next
subsection and for the case of general adversaries in appendix. Our proof
strategy builds upon the proofs from [5] and [38]. Relying on our new notion
of depth-robustness, we combine ideas from both proofs, improve on their
security bounds, and adapt them to graph-restricted adversaries and the case
where we only ask one challenge from the prover.

######  Theorem 2.

Assume that the graph-based PoSE scheme is instantiated with parameters
$(m,1,w)$ and with a $(m,\gamma)$-depth-robust graph $G$. Let $\mathcal{A}$ be
any _$(M,q)$ -bounded_ adversary, with $q<\gamma$. There exists a set of
random oracles $H_{\mathsf{good}}\subseteq H$ such that $\mathcal{A}$’s
winning probability is bounded by $\frac{M^{\prime}}{m}$ within
$H_{\mathsf{good}}$, where:

  * •

$M^{\prime}=\left\lceil\frac{M}{w}\right\rceil$ and
$\abs{H_{\mathsf{good}}}\geq\abs{H}\cdot(1-2^{-w})$ if $\mathcal{A}$ is graph-
restricted

  * •

else: $M^{\prime}=\left\lceil\frac{M}{w_{0}}\right\rceil$ and
$\abs{H_{\mathsf{good}}}\geq\abs{H}\cdot(1-2^{-w_{0}})$, where
$w_{0}=w-\log(m)-\log(q)$.

Consider an adversary $\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ against
the memory challenge game for our PoSE instantiated with a graph $G$. Let
$\sigma=\mathcal{A}_{0}(1^{w},\rho,h)$. Let $O(G)=\set{o_{1},\ldots,o_{m}}$ be
the set of all challenge vertices that can be given to $\mathcal{A}_{1}$
during the experiment. For this protocol the adversary $\mathcal{A}_{1}$ has
access to the random oracle $h$ through $\mathcal{O}$, which we make clear in
the notation onwards by calling the oracle function $\mathcal{O}_{h}$. A query
$Q$ from $\mathcal{A}_{1}$ to $\mathcal{O}_{h}$ is good if $\exists v\colon
Q=\ell^{-}(v)$. For every $i\in\\{1,\ldots,m\\}$, considering the execution of
$\mathcal{A}_{1}^{\mathcal{O}_{h}}(1^{w},\rho,\sigma,o_{i})$, we let:

  * •

$Q_{i,j}$ be the input to the $j$-th oracle call made to $\mathcal{O}_{h}$ by
$\mathcal{A}_{1}$ in this execution;

  * •

$t_{i}$ be the total number of oracle calls made by $\mathcal{A}_{1}$ in this
execution;

  * •

$Q_{i,t_{i}+1}$ be the output of $\mathcal{A}_{1}$ on this execution.

######  Definition 10 (Blue node).

We say that a node $v\in V(G)$ is blue if and only if there exists
$v^{\prime}\in V(G)$, $i\in\\{1,\ldots,m\\}$ and $j\geq 1$ such that:

  1. 1.

$v\in\Gamma^{-}(v^{\prime})$ and $Q_{i,j}=\ell^{-}(v^{\prime})$

  2. 2.

$\forall i^{\prime}\in\set{1,\ldots,m}\forall
j^{\prime}<j.\leavevmode\nobreak\ Q_{i^{\prime},j^{\prime}}\neq\ell^{-}(v)$

We say that $v$ is a _blue node_ from iteration $j$, and that $Q_{i,j}$ is the
query associated to $v$. Denote by $B_{j}$ all blue nodes in iteration $j$,
and by $B$ the set of all blue nodes. A bitstring is a _pre-label_ if it is
equal to $\ell^{-}(v)$ for some $v$, and a _possible pre-label_ if it is the
concatenation of a node $v$ and $w\cdot\abs{\Gamma^{-}(v)}$ bits.

The first point above implies that:

$\ell^{-}(v^{\prime})=v^{\prime}\concat y_{1}\concat\ldots\concat
y_{m}\wedge\ell(v)\in\set{y_{1},\ldots,y_{m}}$

The second point will ensure that we can extract the labels of blue nodes for
free, i.e. without querying them to the random oracle, by running
$\mathcal{A}_{1}$ in parallel for all possible challenges on the state
$\sigma$ computed by $\mathcal{A}_{0}$. Let $T_{i}=t_{i}$ if the response to
the challenge $o_{i}$ by $\mathcal{A}_{1}$ is correct, or infinite otherwise.
The strategy for the proof of Theorem 2 will be the following:

  * •

_First step:_ prove that the success probability of the adversary is smaller
than the fraction between the number of blue nodes, whose label it has stored,
and the total number of labels it is supposed to store.

  * •

_Second step:_ prove an upper bound on the number of blue nodes; for graph-
restricted adversaries, this will be $\left\lceil\frac{M}{w}\right\rceil$,
matching the value $M^{\prime}$ from Theorem 2.

First, we show that to answer a challenge correctly, $A_{1}$ needs to
recompute the labels of the longest path to any node that is not blue:

######  Lemma 3.

$\forall i\in\\{1,\ldots,m\\}\colon T_{i}\geq\mathsf{llp}(o_{i},G\setminus
B)$, i.e. the time it takes to compute the label of $o_{i}$ is at least the
length of the longest path $\mathsf{llp}(o_{i},G\setminus B)$.

Furthermore, if the graph is $(m,\gamma)$-depth-robust, such paths are with
high probability longer than $\gamma$ if $M$ is significantly smaller than
$m\cdot w$.

######  Lemma 4.

If the graph $G$ is $(m,\gamma)$-depth-robust, then:

$\underset{i\sample[m]}{\operatorname{\probname}}[T_{i}\geq\gamma]\geq
1-\abs{B}m^{-1}$

Given the previous results, we can bound the probability of success of the
adversary in proportion to the number of blue nodes, as shown in the following
lemma. This concludes the first step of the proof of Theorem 2.

######  Lemma 5.

Given an _$(M,q)$ -bounded_ adversary $\mathcal{A}$, with $q<\gamma$, and a
random oracle $h\in H$ such that $\abs{B}\leq\bar{B}$, then its probability of
success is bounded by $\bar{B}\cdot m^{-1}$.

###### Proof.

From Lemma 4 we deduce that the probability that $T_{i}\geq\gamma$ is at least
$1-\abs{B}m^{-1}\geq 1-\bar{B}m^{-1}$. But given that $q<\gamma$, it follows
that the adversary cannot reply to these challenges on time, which implies
that its probability of success is bounded by $\bar{B}m^{-1}$, as claimed. ∎

###  6.5 Security proof: second step for graph-restricted $\mathcal{A}$

Next we show that, with high probability over the choice of the random oracle,
we obtain the desired upper bound on the number of blue nodes. That is, for a
big proportion of (good) random oracles, $\abs{B}$ is smaller than the number
of blocks stored by $\mathcal{A}_{0}$ in $\sigma$. This will help us bound the
prediction ability of a cheating adversary that did not store enough labels.
Recall that $H$ is the set of all random oracles from $\set{0,1}^{\kappa}$ to
$\set{0,1}^{w}$. We will rely on the following well-known result.

######  Lemma 6 (adapted from Fact 8.1 in [19]).

If there is a deterministic encoding procedure $\mathit{Enc}\colon
H\to\bin^{s}$ and a decoding procedure $\mathit{Dec}\colon\bin^{s}\to H$ such
that $\underset{x\sample
H}{\operatorname{\probname}}[\mathit{Dec}(\mathit{Enc}(x))=x]\geq\delta$, then
$s\geq\log\abs{H}+\log{\delta}$.

Intuitively, relying on the adversary $\mathcal{A}$ and its set of blue nodes,
we will construct an encoder and a decoder to which we will be able to apply
Lemma 6 to derive the desired bounds.

######  Definition 11 (Good oracle).

We say that $h\in H$ is a good oracle for a _graph-restricted_ $\mathcal{A}$
if $\abs{B}\leq\left\lceil\frac{M}{w}\right\rceil$.

Let ${\cal{}S}$ be the oracle machine in Figure 6. It executes
$\mathcal{A}_{1}$ in parallel for all possible challenges. Notice that
${\cal{}S}$ executes basically the same operations as $\mathcal{A}_{1}$ and
does not make repeated queries to the oracle. ${\cal{}S}$ terminates when it
has finished processing all parallel executions of $\mathcal{A}_{1}$. In each
round, ${\cal{}S}$ processes the respective oracle calls of each instance of
$\mathcal{A}$, and outputs all calls to the environment at the end of the
round. In the next lemma ${\cal{}S}$ will be used by the encoder and decoder
that we construct, which will observe its outputs and process all the oracle
calls of ${\cal{}S}$. The encoder will answer the oracle calls by looking
directly at $h$, while the decoder will obtain the desired values from the
encoded state. The fact that $\mathcal{A}_{1}$ is graph-restricted helps the
decoder determine blue nodes directly.

run A_1^O_h(1^w,ρ,σ,o_1), …, A_1^O_h(1^w, ρ, σ,o_m)  in parallel:
j=1  to  maxt_1, …, t_n + 1:  Let L be an empty list
i=1  to  m:
A_1^O_h(1^w, ρ, σ,o_i)  has not finished:
run  A_1^O_h(1^w, ρ, σ, o_i) until the j -th query (or output)  Q_ij
\- if Q_ij  is an output, add $(0,i,Q_{ij})$ to $L$
\- if Q_ij  is repeated, answer with the previous response
\- if Q_ij  is a possible pre-label of $v$, add $(1,v,Q_{ij})$ to $L$
\- else ask $\mathcal{O}_{h}(Q_{ij})$, relay the answer to  A_1  and store it
each  (t, v, q)  in L:  (ordered in inverse topological order w.r.t. $G$)
output  (t, v, q)
if $t=1$ ask  O_h(q) , relay the answer to  A_1  and store it

Figure 6: Procedure for
${\cal{}S}^{\mathcal{O}_{h}}_{\mathcal{A}}(1^{w},\rho,\sigma)$

######  Lemma 7.

Let $\mathcal{A}$ be an attacker with parameters $(m,1,w)$ and
$H_{\mathsf{good}}\subseteq H$ be the corresponding set of good oracles. Then
$\abs{H_{\mathsf{good}}}\geq(1-2^{-w})\cdot\abs{H}$.

###### Proof.

We show that there exists an encoder (and corresponding decoder) algorithm
that using $\mathcal{A}$ is able to compress a random function from $H$, as
long as the size of $B$ is greater than $\left\lceil\frac{M}{w}\right\rceil$,
i.e. the function is not in $H_{\mathsf{good}}$. Then we apply Lemma 6 to
obtain an upper bound for the number of functions for which this is possible.

The encoder works as follows: for a function $h$, first run $\mathcal{A}_{0}$
to obtain $\sigma$. Second, run ${\cal{}S}$ with input $\sigma$ and keep track
of its outputs. As the adversary is graph-restricted, all these outputs are
either tuples that correspond to labels of challenge nodes, or pre-labels. In
both cases, store the blue nodes in order. Once $S$ finishes, if the number of
blue nodes stored is less than or equal $\left\lceil\frac{M}{w}\right\rceil$,
output nothing. Else, output $\sigma$, the responses $c$ to all oracles calls
made by ${\cal{}S}$ in order (except the ones associated with blue nodes), and
all the remaining oracle values $c^{\prime}$ (not asked by $S$, nor labels of
blue nodes) in lexicographic order. Note that the labels of blue nodes are not
stored explicitly but encoded in $\sigma$.

The decoder works as follows: given $\sigma$, $c$, $c^{\prime}$, it will
output the whole function table for $h$. First, it executes ${\cal{}S}$ with
input $\sigma$. When ${\cal{}S}$ makes an output, as the adversary is graph-
restricted, the decoder can deduce the labels of the blue nodes associated to
it (if any), and store these values. When ${\cal{}S}$ makes an oracle call, if
the response to the oracle call is known (because it is the label of a node
that was stored before, or is a repeated call), then respond with that value.
Else respond with the next value from $c$. When $S$ finishes, read all the
remaining values in the input $c^{\prime}$. At this point the decoder knows
the whole table for $h$, and outputs it.

The size of the encoding is exactly $M+\log\abs{H}-\abs{B}\cdot w$, and it is
correct with probability $\delta$, which is the proportion of functions $h$
such as the number of blue nodes is more than
$\left\lceil\frac{M}{w}\right\rceil$ (oracles not in $H_{\mathsf{good}}$).
From Lemma 6 we deduce $M+\log\abs{H}-\abs{B}\cdot
w\geq\log\abs{H}+\log(\delta)$ which, together with
$\abs{B}>\left\lceil\frac{M}{w}\right\rceil$, implies $\delta\leq 2^{-w}$. We
conclude that
$\abs{H_{\mathsf{good}}}=(1-\delta)\cdot\abs{H}\geq(1-2^{-w})\cdot\abs{H}$. ∎

Putting together Lemma 7, Definition 11 for good oracles and Lemma 4, we
obtain immediately the statement of Theorem 2 for graph-restricted
adversaries. The proof for general adversaries is similar, and can be found in
the appendices. The main difference is that the decoder will need some
additional advice to detect where the blue nodes are, resulting in worse
bounds when applying Lemma 6.

##  7 Depth-robust graphs that can be labelled in-place

In this section we look for a family of depth-robust graphs w.r.t. a subset of
nodes that can be labelled in-place w.r.t. the same subset of nodes. Although
some classes of graphs from previous works, e.g. [28, 11], satisfy pebbling-
hardness notions related to depth-robustness and can be labelled in place,
they don’t satisfy the strong depth-robustness property that we require. We
therefore propose a new construction. Our construction is based on the graph
in [41], where a simple and recursively constructible depth-robust graph
w.r.t. edge deletions was proposed. The recent results in [13] showed that it
is possible in general to transform an edge depth-robust graph into a vertex
depth-robust graph where only one single long path is guaranteed to exist
after node deletions. We require several long paths, though. Inspired by these
results, although using a different (and ad-hoc) transformation on the graph
from [41], we designed a new class of graphs with the properties needed by the
protocol in Section 6. The main result of this section is the following:

######  Theorem 3.

There exists a family of DAGs $\set{G_{n}}$ where $G_{n+1}$ has
$\mathcal{O}(2^{n}\cdot n^{2})$ nodes and a subset of nodes
$O(G_{n+1})\subset{V(G_{n+1})}$ of size $2^{n}$ such that:

  1. 1.

$G_{n+1}$ is $(2^{n},2^{n})$-depth-robust w.r.t. $O(G_{n+1})$;

  2. 2.

$G_{n+1}$ can be labelled in-place w.r.t. $O(G_{n+1})$.

If $\Gamma$ is a graph, we say that a graph $G$ is a fresh copy of $\Gamma$ if
it is isomorphic and disjoint, and denote it by $G\cong\Gamma$. Let $L_{n}$ be
a list of $2^{n}$ nodes. For any DAG $G$, let $\mathsf{In}(G)$,
$\mathsf{Out}(G)$ its input and output nodes respectively. If $Y$ and $Z$ are
two disjoint lists of nodes of the same size, denote by $X=Y\colon Z$ the
concatenation of both lists. If $X=\sequence{x_{1},\ldots,x_{n}}$ and
$Y=\sequence{y_{1},\ldots,y_{n}}$ are lists of nodes of size $n$, let $X\to
Y=\set{(x_{i},y_{i})\mid 1\leq i\leq n}$.

In our construction we use graph with high connectivity, the so-called
connectors.

######  Definition 12 (Connector).

A directed acyclic graph with bounded indegree, $n$ inputs, and $n$ outputs is
an $n$-connector if for any $1\leq k\leq n$ and any sequences
$(s^{\prime}_{1},\ldots,s^{\prime}_{k})$ of inputs and
$(t^{\prime}_{1},\ldots,t^{\prime}_{k})$ of outputs there are $k$ vertex-
disjoint paths connecting each $s^{\prime}_{i}$ to the corresponding
$t^{\prime}_{i}$.

Next, we introduce notation for connecting two lists of nodes using a
connector graph. Let $H_{n}$ be a $2^{n}$-connector. Given two lists of nodes
$I$ and $O$ of size $2^{n}$, and a fresh copy of $H_{n}$ named $C$, we denote
by $I\overset{H}{\to}O$ the graph with nodes $I\cup O\cup V(C)$ and edges
$E(C)\cup(I\to\mathsf{In}(C))\cup(\mathsf{Out}(C)\to O)$.

Now we are ready to construct our graph family. For each graph $G_{n}$ from
our family, we also define a list of so-called base nodes, which will serve
for connecting $G_{n}$ with other graphs in order to construct the graph
$G_{n+1}$. We define $G_{0}$ to be the graph formed by a single node. Then,
$G_{n+1}$ is constructed from two copies of $G_{n}$ and a copy of $H_{n}$,
which we connect with a set of additional edges. First, every base node in the
first copy of $G_{n}$ is connected through an edge to a corresponding input
node in the copy of $H_{n}$. Second, the copy of $H_{n}$ is connected to the
second copy of $G_{n}$ through a recursive edge construction described below
and illustrated in Figure 7. Formally, we have:

  * •

$G_{0}$: $V(G_{0})=\set{v}$, $E(G_{0})=\emptyset$ and
$\mathsf{Base}(G_{0})=\sequence{v}$.

  * •

$G_{n}$ contains three components $(L,C,R)$, denoted by
$\mathsf{Left}(G_{n})$, $\mathsf{Center}(G_{n})$, $\mathsf{Right}(G_{n})$,
where $L\cong R\cong G_{n-1}$, and $C\cong H_{n-1}$. We let
$\mathsf{Base}(G_{n})=\mathsf{Base}(L)\colon\mathsf{Base}(R)$ denote the base
vertices.

  * •

The operator $\triangleright$ denotes a recursively defined subgraph,
$X\triangleright G_{0}=X\to\mathsf{Base}(G_{0})$, and:

$(X_{1}:X_{2})\triangleright
Y=(X_{1}\triangleright\mathsf{Left}(Y))\cup(X_{2}\overset{H}{\to}\mathsf{In}(\mathsf{Center}(Y)))$

The vertices of $G_{n}$ are:

$V(G_{n})=V(L)\cup V(C)\cup V(R)\cup V(\mathsf{Out}(C)\triangleright R)$

The edges of $G_{n}$ include the edges in the components $L,C,R$, plus two new
sets of edges: the first from $\mathsf{Base}(L)$ to $\mathsf{In}(C)$, and the
second from $\mathsf{Out}(C)$ to $R$:

$\begin{split}E(X)&=E(L)\cup E(C)\cup E(R)\\\
&\cup(\mathsf{Base}(L)\to\mathsf{In}(C))\cup E(\mathsf{Out}(C)\triangleright
R)\end{split}$

$G_{n}$$H_{n}$$H_{n-1}$$G_{n-1}$$G_{n-1}$$G_{n+1}$H Figure 7: $G_{n+1}$,
continuous arrows represent simple edges $\to$, $H$ arrows represent connector
subgraphs $\overset{H}{\to}$ and dashed arrows represent the operator
$\triangleright$.

The next result is essential for our construction. It states that if some
nodes are removed from a connector with the objective of disconnecting
input/output pairs, then it is always possible to do so by just removing
inputs or outputs. For a set of nodes $R$, let $\mathsf{Con}(R)$ be all pairs
of nodes $(v,w)$, where $v$ is an input and $w$ is an output, such that all
paths from $v$ to $w$ contain at least one node in $R$.

######  Lemma 8.

Let $C_{n}$ be an $n$-connector and $R\subset V(C_{n})$ be a subset of its
nodes with $\abs{R}<n$. Then there exists a subset of nodes $R^{\prime}$
containing only input and output nodes, such that
$\abs{R^{\prime}}\leq\abs{R}$ and
$\mathsf{Con}(R)\subseteq\mathsf{Con}(R^{\prime})$.

###### Proof.

Consider a bipartite graph $B_{R}$ with $n$ nodes on each side such that two
nodes are connected if and only if the corresponding pair is in
$\mathsf{Con}(R)$. Consider a maximum matching $M$ and the minimum vertex
cover $VC$ in this graph. From König’s theorem [30] we deduce that
$\abs{M}=\abs{VC}$. Moreover, from the connector property of $C_{n}$ we deduce
that $\abs{M}\leq\abs{R}$: otherwise, using the connector property between the
sets of nodes in the matching, we would find $\abs{R}+1$ disjoint paths from
the input to the output, and those cannot be covered by the nodes in $R$.
Then, $\abs{VC}\leq\abs{R}$. Consider the set $R^{\prime}=VC$. If these nodes
are removed from $C_{n}$, consider the bipartite graph $B_{R^{\prime}}$
(analogous to $B_{R}$). Clearly $B_{R}$ is a subgraph of $B_{R^{\prime}}$ by
the vertex cover property. This implies that
$\mathsf{Con}(R)\subseteq\mathsf{Con}(R^{\prime})$, as claimed. ∎

To prove the depth-robustness of $G_{n}$, we will prove first that after
removing some nodes, there remains a long path containing nodes from
$\mathsf{Base}(G_{n})$.

######  Theorem 4.

Consider $G_{n}$ and any subset of nodes $R\subset V(G_{n})$, with
$\abs{R}<2^{n}$. There is a path $L$ in $G_{n}\setminus R$ such that
$\abs{V(L)\cap\mathsf{Base}(G_{n})}\geq 2^{n}-\abs{R}$.

###### Proof sketch.

First, by using Lemma 8 we reduce the problem by showing that if there is a
counterexample set $R$, then there is also a counterexample set $R^{\prime}$,
but for which no node removed is strictly inside any connector graph, i.e.
they must be part of the input or output. To conclude, we prove by induction a
stronger statement, in which not only the path $L$ exists, but the nodes in
$V(L)\cap\mathsf{Base}(\mathsf{Right}(\mathsf{Left}^{k}(G_{n})))$ also must be
reachable from the nodes in
$\mathsf{In}(\mathsf{Center}(\mathsf{Left}^{k}(G_{n})))$ for $0\leq k\leq n$.
This property makes possible to glue together paths while proving the
induction hypothesis. For the full proof see Section 10.5. ∎

######  Corollary 3.

$G_{n+1}$ is $(2^{n},2^{n})$-depth-robust w.r.t.
$\mathsf{Base}(\mathsf{Right}(G_{n+1}))$

###### Proof.

Consider a set $R$ of size less than $2^{n}$ and the path $L$ given by the
previous theorem (the theorem would be applicable even if
$2^{n}\leq\abs{R}<2^{n+1}$, but we are only using a restricted result). Then
$V(L)\cap\mathsf{Base}(G_{n+1})\geq 2^{n+1}-\abs{R}$. Let
$M=V(L)\cap\mathsf{Base}(\mathsf{Right}(G_{n+1}))$. Then $\abs{M}\geq
2^{n}-\abs{R}$ given:

$\begin{split}&2^{n}+\abs{M}=\abs{\mathsf{Base}(\mathsf{Left}(G_{n+1}))}+\abs{M}\\\
&\geq\abs{V(L)\cap\mathsf{Base}(G_{n+1})}\geq 2^{n+1}-\abs{R}\end{split}$

We conclude that the $2^{n}-\abs{R}$ rightmost elements (with respect to $L$)
in $M$ contain each at least $2^{n+1}-\abs{R}-(2^{n}-\abs{R})=2^{n}$
predecessors in $L$, as claimed. ∎

As connectors we use the butterfly family of graphs [13], which can be easily
labelled in-place, and allow the next result to hold:

######  Lemma 9.

$G_{n+1}$ can be labelled in-place with respect to $\mathsf{Base}(G_{n+1})$,
and also with respect to $\mathsf{Base}(\mathsf{Right}(G_{n+1}))$, in
$\mathcal{O}(2^{n+1}\cdot{(n+1)}^{2})$ time.

###### proof sketch.

We apply induction on both statements at the same time. For the induction step
of the first statement, notice that in order to label $G_{n+1}$ with respect
to its $\mathsf{Base}$, we can first label $\mathsf{Left}(G_{n+1})$ using
$2^{n}\cdot w+\mathcal{O}(w)$ memory. Then, while keeping the previous labels
stored, compute the labels of $\mathsf{In}(\mathsf{Center}(G_{n+1}))$ using
$2^{n}\cdot w+\mathcal{O}(w)$ extra memory. From these we can compute in-place
the labels of the nodes in $\mathsf{Center}(G_{n+1})$ and later
$\mathsf{Out}(\mathsf{Center}(G_{n+1}))\triangleright\mathsf{Right}(G_{n+1})$,
as these subgraphs only contain copies of butterfly graphs, which can be
easily labelled in-place. Then, by the induction hypothesis, compute the
labels of $\mathsf{Base}(\mathsf{Right}(G_{n+1}))$ using the same memory as
before. The proof for the induction step for the second statement is the same,
except that the labels of $\mathsf{Base}(\mathsf{Left}(G_{n+1}))$ are not
stored, so this memory is overwritten afterwards. ∎

The proposed protocol for memory erasure depends on a graph and a subset of
its nodes $O(G)$. In particular, the memory size in words needs to be the same
as the $O(G)$. Thus, the graphs constructed previously can only be used if the
memory size is a power of two, which may not be true in practice. The next
results solve this issue: they show how to construct depth-robust graphs that
can be labelled in-place with respect to a subset of nodes of arbitrary size.

######  Lemma 10.

Let $G_{1}$ be $(a_{1},b)$-depth-robust with respect to $O(G_{1})$ and $G_{2}$
be $(a_{2},b)$-depth-robust with respect to $O(G_{2})$. Then the graph $G$
defined by the disjoint union $G_{1}$ and $G_{2}$ is $(a_{1}+a_{2},b)$-depth-
robust with respect to $O(G)=O(G_{1})\cup O(G_{2})$.

###### Proof.

Let $R$ be a set of nodes in $G$ with $\abs{R}<a_{1}+a_{2}$. Let
$r_{1}=\abs{R\cap V(G_{1})}$ and $r_{2}=\abs{R\cap V(G_{2})}$. Notice that, if
$r_{1}<a_{1}$ then by the depth-robustness of $G_{1}$ there are at least
$a_{1}-r_{1}$ nodes $v$ in $G_{1}\setminus R$ with $\mathsf{llp}(v)\geq b$,
and the analogous result is true for $G_{2}$. We conclude by case analysis:

  * •

if $r_{2}\geq a_{2}\implies r_{1}<a_{1}$, from which the result follows given
that $a_{1}-r_{1}\geq a_{1}+a_{2}-r_{1}-r_{2}$.

  * •

if $r_{1}\geq a_{1}$ the result follows by symmetry with the previous case.

  * •

else $r_{2}<a_{2}\wedge r_{1}<a_{1}$, which means that we can find $a-r_{2}$
paths in $G_{2}$ and $a-r_{1}$ paths in $G_{1}$ with length greater than $b$,
ending in different vertices in $O(G_{1})\cup O(G_{2})$.

∎

######  Lemma 11.

Let $G$ be $(a,b)$-depth-robust with respect to $O(G)$. Let $O^{\prime}$ be a
subset of $O(G)$ of size $a^{\prime}$. Then $G$ is $(a^{\prime},b)$-depth-
robust with respect to $O^{\prime}$.

###### Proof.

Let $R^{\prime}$ be a set of nodes with $\abs{R^{\prime}}<a^{\prime}$. Let
$R=R^{\prime}\cup(O(G)\setminus O^{\prime})$. Notice that $\abs{R}<a$. Then
the nodes with longs paths guaranteed by the depth robustness of $G$ in
$G\setminus R$ will also be nodes with long paths in $G\setminus R^{\prime}$.
Moreover, by definition of $R$ these nodes are in $O^{\prime}$ and there are
at least $a-\abs{R}=a^{\prime}-\abs{R^{\prime}}$ such nodes, as needed. ∎

######  Lemma 12.

Let $G$ be a graph that can be labelled in-place with respect to $O(G)$, and
$G^{\prime}$ the graph defined by the disjoint union of two copies of $G$,
$G_{1}$ and $G_{2}$. If $O^{\prime}$ is a subset of $O(G_{2})$, then
$G^{\prime}$ can be labelled in-place with respect to $O(G_{1})\cup
O^{\prime}$.

###### Proof.

First compute the labels of $O(G_{2})$ in-place. Then keep storing only the
labels from $O^{\prime}$. With the space left, compute the labels of
$O(G_{1})$ in-place. The result follows. ∎

######  Theorem 5.

Let $m$ be any memory size, and let $n$ be the smallest integer such that
$2^{n+1}\geq m$. Then there exists a $(m,2^{n})$-depth-robust graph $G$ with
respect to $O(G)$ that can be labelled in-place with respect to $O(G)$.

###### Proof.

Take $G=C_{1}\cup C_{2}$ where $C_{1}\cong C_{2}\cong G_{n+1}$ (as defined in
our construction). By Corollary 3 and Lemma 10, $G$ is
$(2^{n+1},2^{n})$-depth-robust with respect to $O(C_{1})\cup O(C_{2})$. Let
$O^{\prime}$ be a subset of $O(C_{2})$ with size $m-2^{n}$, and let
$O(G)=O(C_{1})\cup O^{\prime}$. Then by Lemma 11 $G$ is $(m,2^{n})$-depth-
robust with respect to $O(G)$. Furthermore, by Lemma 9 and Lemma 12 $G$ can be
labelled in-place with respect to $O(G)$, as claimed. ∎

##  8 Lightweight protocol

In this section we focus on a trade-off between efficiency and security our
graph-based memory-erasure protocol. To this end, we construct new graphs with
relaxed depth-robustness properties, which will help boost the performance of
the protocol by a polylogarithmic factor. This will have the cost of offering
slightly less security. Hence, we suggest this lightweight version is used
when more performance is needed, and the original one when the highest level
of security is required.

Next we analyse the trade-off between the depth-robustness of the graph and
the protocol security in Corollary 2, which we reproduce to the reader’s
advantage.

See 2

Notice that the parameter $\gamma$ (which represents the depth of paths) in
the depth-robustness property must be greater than the number of queries the
adversary can do within a fast phase round. This is the only restriction this
parameter has. For the family of graphs constructed in Section 7, $\gamma$ is
at least $m$, the number of output nodes in the graph. Note that this is quite
high, considering that a realistic attacker may at most do a small constant
amount of operations during the fast phase, and that the operations we bound
are hash computations. Therefore, for $\kappa$ a small constant and each $m$,
we construct a $(m,\kappa)$-depth-robust graph $G^{\prime}_{m}$. Applying
Corollary 2 to $G^{\prime}_{m}$ we obtain a secure protocol against
$(M,\kappa-1)$-bounded adversaries with exactly the same security bounds.

For the sake of simplicity, assume $\kappa$ is fixed in a small power of 2,
for example 16. Then, the graph $G_{4}$ from the previous section is a
$(16,\kappa)$-depth-robust graph with respect to
$O(G_{4})=\set{o_{1},o_{2},\ldots,o_{16}}$.

######  Definition 13.

Let $Q_{i}$ for $1\leq i\leq 16$ be the subgraph of $G_{4}$ that contains all
nodes which belong to some path ending in a node from
$\set{o_{1},\ldots,o_{i}}$, and $O(Q_{i})=\sequence{o_{1},\ldots,o_{i}}$.

######  Lemma 13.

$Q_{i}$ is $(i,\kappa)$-depth-robust with respect to $O(Q_{i})$.

###### Proof.

Notice that, by definition, $Q_{i}$ is a subgraph of $G_{4}$ (which is
$(16,\kappa)$-depth-robust) and $O(Q_{i})\subseteq
O(G_{4})\wedge\abs{O(Q_{i})}=i$. Then, the result follows from Lemma 11. ∎

######  Definition 14.

Let $G^{\prime}_{m}$ be a graph and $O(G^{\prime}_{m})$ a subset of nodes
defined as follows. Let $m=16\cdot k+i$ be the result of the Euclidean
division lemma.

  * •

If $i=0\wedge k=0$: $G^{\prime}_{m}$ is the empty graph

  * •

If $i=0$ then: $G^{\prime}_{m}$ is the disjoint union of $k$ graphs isomorphic
with $G_{4}$, and $O(G^{\prime}_{m})$ the union of the corresponding nodes in
each copy of $O(G_{4})$.

  * •

If $i>0$: $G^{\prime}_{m}$ is the disjoint union of $k$ copies of
$G^{\prime}_{16}$ and $Q_{i}$, and $O(G^{\prime}_{m})$ the union of the
corresponding nodes in each copy of $O(G^{\prime}_{16})$ and $O(Q_{i})$.

######  Lemma 14.

The graph $G^{\prime}_{m}$ is $(m,\kappa)$-depth-robust with respect to
$O(G^{\prime}_{m})$.

###### Proof.

By definition, if $m=16\cdot k+i$, $G^{\prime}_{m}$ is the disjoint union of
$k$ copies of $G_{4}$, which is $(16,\kappa)$-depth-robust, and a copy of
$Q_{i}$ which is $(i,\kappa)$-depth-robust. The result follows by applying
Lemma 10 to these disjoint graphs which form $G^{\prime}_{m}$. ∎

######  Lemma 15.

If $m\geq 16$, the graph $G^{\prime}_{m}$ can be labelled in-place with
respect to $O(G^{\prime}_{m})$.

###### Proof sketch.

We label the output nodes of each component of $G^{\prime}_{m}$ independently.
First, we compute and store the labels the nodes in $Q_{i}$, which can be done
using at most 16 words (because this is a subgraph of $G_{4}$). For this to
hold the condition $m\geq 16$ is necessary. The remaining space can be used to
compute and store the output labels in each copy of $G_{4}$, using the in-
place properties of these graphs. ∎

By the previous lemmas, we conclude that the graph $G^{\prime}_{m}$ has the
required properties to serve as the basis of our secure memory-erasure
protocol. It remains to compute how many hash computations are done by a
prover using our protocol instantiated with $G^{\prime}_{m}$, in comparison to
the original proposal. For simplicity, we analyse the case where $m=2^{k}$
with $k>3$.

######  Lemma 16.

If $m=2^{k}$, labelling $G_{k}$ requires exactly ${(k^{2}+k+3)}\cdot
2^{k+1}-2$ hash computations and labelling $G^{\prime}_{m}$ requires exactly
$367\cdot 2^{k-3}$ hash computations. Therefore, the lightweight protocol is
approximately $\frac{k^{2}+k+3}{23}$ times more efficient.

###### Proof.

Both graphs can be labelled optimally by the results shown in the previous
section (Lemmas 9, 12 and 5). Therefore, it remains to count the exact number
of nodes in $G_{k}$, from which we can easily obtain the exact amount for
$G^{\prime}_{m}$.

By the recursive definition of $G_{k}$, we have that its number of nodes is
equal to:

$2\cdot\abs{G_{k-1}}+\sum_{i=0}^{k}\abs{H_{i}}$

The butterfly graph $H_{i}$ has exactly $2\cdot(i+1)\cdot 2^{i}$ nodes.
Therefore, we can derive the recurrent equation:

$\abs{G_{k}}=7\cdot\abs{G_{k-1}}-18\cdot\abs{G_{k-2}}+20\cdot\abs{G_{k-3}}-8\cdot\abs{G_{k-4}}$

with initial conditions
$\abs{G_{0}}=4,\abs{G_{1}}=18,\abs{G_{2}}=70,\abs{G_{3}}=238$. The exact
solution to this recurrence is $\abs{G_{k}}={(k^{2}+k+3)}\cdot 2^{k+1}-2$.
From there we obtain that $\abs{G_{4}}=23\cdot 32-2$ and
$\abs{G^{\prime}_{m}}=2^{k-4}\cdot(23\cdot 32-2)$. Therefore, by removing the
small additive terms, we deduce that the lightweight protocol is approximately
$\frac{k^{2}+k+3}{23}$ times more efficient, as claimed. ∎

_A brief discussion on performance and feasibility._ We provide a prototype
implementation of the algorithm from Section 6 with the goal of showing that
our depth-robust graphs can indeed be labelled in-place. Our prototype
implementation can be found at 222https://gitlab.uni.lu/regil/memory-erasurein
two languages: python and C. To estimate memory overhead, we compiled our
prototype to a 32-bit architecture, obtaining a program of size 3.4KB
including the space necessary to store the hash values used for graph-
labelling. To estimate computational time, we ran our prototype in a standard
desktop computer and simulated the erasure of 32KB of memory, which took
0.25s. As far as communication overhead is concerned, we did not directly test
the speed of the fast phase. But, taking into account the results obtained in
a similar setting, that of performing distance-bounding via Bluetooth
communication [1], we estimate that 128 rounds of the fast phase should take
around 10 seconds. While recognizing the limitations of our performance
analysis, we believe these preliminary values are promising and leave for
future work a throughout performance analysis of software-based erasure
protocols, including ours.

##  9 Conclusions

We presented the first three provable secure PoSE protocols capable of
deterring provers from outsourcing the erasure proof to an external
conspirator. One protocol is simple to implement but suffers from high
communication complexity; the others ask the prover to label a depth-robust
graph from a random seed. Because the labelling algorithm is implemented by a
resource-constrained device, we introduced a class of graphs with depth-robust
properties that can be labelled in-place using hash functions. All protocols
were proven secure within a formal model. Notably, we proved security bounds
for the three protocols guaranteeing that all the prover’s memory, except for
a small part, is erased. Those security bounds are tighter against a
restricted, yet plausible, adversary. Hence, future work directed to closing
such gap is needed.

## References

  * [1] Aysajan Abidin et al.  “Secure, Accurate, and Practical Narrow-Band Ranging System”  In _IACR Transactions on Cryptographic Hardware and Embedded Systems_ , 2021
  * [2] Joël Alwen, Jeremiah Blocki and Ben Harsha  “Practical Graphs for Optimal Side-Channel Resistant Memory-Hard Functions”  In _Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security_ , 2017, pp. 1001–1017
  * [3] Joël Alwen, Jeremiah Blocki and Krzysztof Pietrzak  “Depth-Robust Graphs and Their Cumulative Memory Complexity”  In _Annual International Conference on the Theory and Applications of Cryptographic Techniques_ Springer, 2017, pp. 3–32
  * [4] Joël Alwen, Jeremiah Blocki and Krzysztof Pietrzak  “Sustained Space Complexity”  In _Annual International Conference on the Theory and Applications of Cryptographic Techniques_ Springer, 2018, pp. 99–130
  * [5] Joël Alwen et al.  “On the Complexity of Scrypt and Proofs of Space in the Parallel Random Oracle Model”  In _Annual International Conference on the Theory and Applications of Cryptographic Techniques_ Springer, 2016, pp. 358–387
  * [6] Joël Alwen et al.  “Scrypt Is Maximally Memory-Hard”  In _Annual International Conference on the Theory and Applications of Cryptographic Techniques_ Springer, 2017, pp. 33–62
  * [7] Mahmoud Ammar, Bruno Crispo and Gene Tsudik  “Simple: A Remote Attestation Approach for Resource Constrained Iot Devices”  In _2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS)_ IEEE, 2020, pp. 247–258
  * [8] Mahmoud Ammar, Wilfried Daniels, Bruno Crispo and Danny Hughes  “Speed: Secure Provable Erasure for Class-1 Iot Devices”  In _Eighth ACM Conference on Data and Application Security and Privacy_ , 2018, pp. 111–118
  * [9] Sigurd Frej Joel Jørgensen Ankergaard, Edlira Dushku and Nicola Dragoni  “State-of-the-Art Software-Based Remote Attestation: Opportunities and Open Issues for Internet of Things”  In _Sensors_ 21.5 Multidisciplinary Digital Publishing Institute, 2021, pp. 1598
  * [10] Frederik Armknecht, Ahmad-Reza Sadeghi, Steffen Schulz and Christian Wachsmann  “A Security Framework for the Analysis and Design of Software Attestation”  In _Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security_, 2013, pp. 1–12
  * [11] Giuseppe Ateniese, Ilario Bonacina, Antonio Faonio and Nicola Galesi  “Proofs of Space: When Space Is of the Essence”  In _International Conference on Security and Cryptography for Networks_ Springer, 2014, pp. 538–557
  * [12] Mihir Bellare and Phillip Rogaway  “Random Oracles Are Practical: A Paradigm for Designing Efficient Protocols”  In _Proceedings of the 1st ACM Conference on Computer and Communications Security_ , 1993, pp. 62–73
  * [13] Jeremiah Blocki and Mike Cinkoske  “A New Connection Between Node and Edge Depth Robust Graphs”  In _12th Innovations in Theoretical Computer Science Conference (ITCS 2021)_ , 2021  Schloss Dagstuhl-Leibniz-Zentrum für Informatik
  * [14] Ioana Boureanu, Tom Chothia, Alexandre Debant and Stéphanie Delaune  “Security Analysis and Implementation of Relay-Resistant Contactless Payments”  In _Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security_ , 2020, pp. 879–898
  * [15] Sergiu Bursuc, Reynaldo Gil-Pons, Sjouke Mauw and Rolando Trujillo-Rasua  “Software-Based Memory Erasure with Relaxed Isolation Requirements”  In _Proc. 37th IEEE Computer Security Foundations Symposium (CSF’24)_ , 2024, pp. to appear
  * [16] Claude Castelluccia, Aurélien Francillon, Daniele Perito and Claudio Soriente  “On the Difficulty of Software-Based Attestation of Embedded Devices”  In _Proceedings of the 16th ACM Conference on Computer and Communications Security_ , 2009, pp. 400–409
  * [17] Gérard Cohen, Iiro Honkala, Simon Litsyn and Antoine Lobstein  “Covering Codes”  Elsevier, 1997
  * [18] Mauro Conti, Denis Donadel, Radha Poovendran and Federico Turrin  “Evexchange: A Relay Attack on Electric Vehicle Charging System”  In _Computer Security–ESORICS 2022: 27th European Symposium on Research in Computer Security, Copenhagen, Denmark, September 26–30, 2022, Proceedings, Part I_ Springer, 2022, pp. 488–508
  * [19] Anindya De, Luca Trevisan and Madhur Tulsiani  “Time Space Tradeoffs for Attacks against One-Way Functions and PRGs”  In _Annual Cryptology Conference_ Springer, 2010, pp. 649–665
  * [20] Cynthia Dwork, Moni Naor and Hoeteck Wee  “Pebbling and Proofs of Work”  In _Annual International Cryptology Conference_ Springer, 2005, pp. 37–54
  * [21] Stefan Dziembowski, Sebastian Faust, Vladimir Kolmogorov and Krzysztof Pietrzak  “Proofs of Space”  In _Annual Cryptology Conference_ Springer, 2015, pp. 585–605
  * [22] Stefan Dziembowski, Tomasz Kazana and Daniel Wichs  “One-Time Computable Self-Erasing Functions”  In _Theory of Cryptography Conference_ Springer, 2011, pp. 125–143
  * [23] E… EMVCo  “Contactless Specifications for Payment Systems”  In _Book C-2, Kernel_ 2, 2021
  * [24] Paul Erdos, Ronald L. Graham and Endre Szemerédi  “On Sparse Graphs with Dense Long Paths”  In _Comp. and Math. with Appl_ 1, 1975, pp. 145–161
  * [25] Reynaldo Gil Pons et al.  “Is Eve Nearby? Analysing Protocols under the Distant-Attacker Assumption”  In _IEEE Computer Security Foundations Symposium, August 7-10, 2022, Haifa, Israel_ , 2022  DOI: 10.1109/CSF54842.2022.9919655
  * [26] Peter Gutmann  “Secure Deletion of Data from Magnetic and Solid-State Memory”  In _6th USENIX Security Symposium (USENIX Security 96)_ San Jose, CA: USENIX Association, 1996  URL: https://www.usenix.org/conference/6th-usenix-security-symposium/secure-deletion-data-magnetic-and-solid-state-memory
  * [27] Ghassan O. Karame and Wenting Li  “Secure Erasure and Code Update in Legacy Sensors”  In _International Conference on Trust and Trustworthy Computing_ Springer, 2015, pp. 283–299
  * [28] Nikolaos P. Karvelas and Aggelos Kiayias  “Efficient Proofs of Secure Erasure”  In _International Conference on Security and Cryptography for Networks_ Springer, 2014, pp. 520–537
  * [29] Chongkyung Kil et al.  “Remote Attestation to Dynamic System Properties: Towards Providing Complete System Integrity Evidence”  In _IEEE/IFIP International Conference on Dependable Systems & Networks_, 2009
  * [30] Dénes Konig  “Graphs and Matrices”  In _Matematikai és Fizikai Lapok_ 38, 1931, pp. 116–119
  * [31] Boyu Kuang et al.  “A Survey of Remote Attestation in Internet of Things: Attacks, Countermeasures, and Prospects”  In _Computers & Security_ 112 Elsevier, 2022, pp. 102498
  * [32] Daniel Malinowski and Karol Żebrowski  “Disproving the Conjectures from “On the Complexity of Scrypt and Proofs of Space in the Parallel Random Oracle Model””  In _International Conference on Information Theoretic Security_ Springer, 2017, pp. 26–38
  * [33] Francesca Meneghello et al.  “IoT: Internet of Threats? A Survey of Practical Security Vulnerabilities in Real IoT Devices”  In _IEEE Internet of Things Journal_ 6.5 IEEE, 2019, pp. 8182–8201
  * [34] Lily Hay Newman  “An Elaborate Hack Shows How Much Damage IoT Bugs Can Do”, https://www.wired.com/story/elaborate-hack-shows-damage-iot-bugs-can-do/, 2010
  * [35] Bryan Parno, Jonathan M. McCune and Adrian Perrig  “Bootstrapping Trust in Commodity Computers”  In _IEEE Symposium on Security and Privacy_ IEEE, 2010
  * [36] Wolfgang J. Paul, Robert Endre Tarjan and James R. Celoni  “Space Bounds for a Game on Graphs”  In _Mathematical systems theory_ 10.1 Springer, 1976, pp. 239–251
  * [37] Daniele Perito and Gene Tsudik  “Secure Code Update for Embedded Devices via Proofs of Secure Erasure”  In _European Symposium on Research in Computer Security_ Springer, 2010, pp. 643–662
  * [38] Krzysztof Pietrzak  “Proofs of Catalytic Space”  In _10th Innovations in Theoretical Computer Science Conference, ITCS 2019, January 10-12, 2019, San Diego, California, USA_ 124, LIPIcs  Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, pp. 59:1–59:25  DOI: 10.4230/LIPIcs.ITCS.2019.59
  * [39] Andreea-Ina Radu et al.  “Practical EMV Relay Protection”  In _2022 IEEE Symposium on Security and Privacy (SP)_ IEEE, 2022, pp. 1737–1756
  * [40] Kasper Bonne Rasmussen and Srdjan Capkun  “Realization of RF Distance Bounding.”  In _USENIX Security Symposium_ , 2010, pp. 389–402
  * [41] Georg Schnitger  “On Depth-Reduction and Grates”  In _24th Annual Symposium on Foundations of Computer Science (Sfcs 1983)_ IEEE, 1983, pp. 323–328
  * [42] Arvind Seshadri, Adrian Perrig, Leendert Van Doorn and Pradeep Khosla  “SWATT: Software-based Attestation for Embedded Devices”  In _IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004_ IEEE, 2004, pp. 272–282
  * [43] Rolando Trujillo-Rasua  “Secure Memory Erasure in the Presence of Man-in-the-Middle Attackers”  In _Journal of Information Security and Applications_ 57, 2019, pp. 102730
  * [44] Dominique Unruh  “Random Oracles and Auxiliary Input”  In _Annual International Cryptology Conference_ Springer, 2007, pp. 205–223

##  10 Appendix

###  10.1 Proof of Erasure vs Proof of Space

In a Proof of Space (PoS) protocol, a prover aims to convince a verifier that
it has reserved a non-trivial amount of memory space, making it a popular
alternative to proof of work. A PoS, as defined in [21], has two phases: one
where the verifier interacts with an attacker $\mathcal{A}_{0}$, which is
supposed to compute and store a state $\sigma_{0}$ of a certain size; another
one where a second attacker $\mathcal{A}_{1}$ takes $\sigma_{0}$ as input and
answers the verifier challenges. The verifier then accepts or rejects the
proof based on the responses received from $\mathcal{A}_{1}$. Let $\sigma_{1}$
be the state of maximal size used by $\mathcal{A}_{1}$. There are two notions
of proof of space security defined in [21, 38], one lower-bounding the size of
$\sigma_{0}$ and the other lower-bounding the size of $\sigma_{1}$. The
definition in [11] only lower-bounds the size of $\sigma_{1}$. These notions
are close to what we need, except that they isolate $\mathcal{A}_{1}$ from
$\mathcal{A}_{0}$ in the second phase, which amounts to the device isolation
assumption. We allow $\mathcal{A}_{0}$ to help $\mathcal{A}_{1}$ in the second
phase, subject to the constraint that the response to the challenge in each
round has to come from $\mathcal{A}_{1}$, i.e. from the local device.
$\mathcal{A}_{0}$ can freely modify the state of $\mathcal{A}_{1}$ between
challenges.

Leaving aside the isolation issue in the security model, a proof of space [21,
11, 38] could in theory be applied to erase memory, since the stored space is
typically a random looking sequence of data. However, all current
constructions are targeted for a different application scenario, where the
prover is a powerful device (e.g. a cloud server) that has more resources at
its disposal in order to prove that it has stored the claimed amount of
memory. They require $O(m\log(m))$ memory to prove memory storage of size $m$.
For a proof of erasure, this gap is too high, as it means a large proportion
of the memory is not guaranteed to be erased. Memory-hardness results [6]
cannot be applied in our case for similar reasons.

###  10.2 Notions related to the graph-restricted adversary

We review existing restrictions for an adversary against protocols based on
graph labelling, and show their relation with our new restriction presented in
Section 6.3. The main goal of these restrictions is to reduce the security
analysis of the considered protocol to the analysis of complexity bounds for a
combinatorial game on graphs, which is typically easier to perform, e.g.
relying on known graph-theoretical results.

_Pebbling adversary:_ The use of graph-labelling in security protocols can be
traced back to the work of Dwork et al. [20], who proposed its use for proofs
of work. Proofs of work don’t require pre-computation and storage of a
prescribed state; the adversary in [20] simply has to compute and return the
challenged label. Since guessing a previously unseen label can happen only
with negligible probability, the security analysis for such an adversary can
be reduced to the classic notion of graph-pebbling complexity [36], where the
adversary is restricted to playing a game on the graph (applying the hash
function corresponds to placing a pebble). This reduction is tight: the
difference between the probability of winning the game on the graph and that
of breaking security is negligible.

_Adversary with pre-stored pebbles:_ The pebbling technique cannot be applied
directly to proofs of space [21], since the adversary is supposed to perform
some pre-computation. Then it could use the available space to encode
information about the labels of the graph. When challenged, it will attempt to
make the minimal number of oracle calls that, combined with information stored
in the state, allows it to obtain the needed responses. For their security
proof, Dziembowski et al. [21] make the simplifying assumption that the best
the adversary can do is to choose a set of labels on the graph, not
necessarily corresponding to the challenge nodes, and store them in the
memory, i.e. the adversary cannot compress or combine labels. This fixed set
of labels is then used to reply to any of the given challenges. Relying on
this assumption, the security analysis can then be reduced to a pebbling game
on the graph where the power of $\mathcal{A}$ is slightly increased, i.e. it
is allowed to pre-store pebbles.

_Adversary with algebraically entangled pebbles._ Alwen et al. [5] have
further relaxed this restriction, allowing the adversary to store several
labels in one block of memory. However, these pebbles are not directly
accessible to $\mathcal{A}$, but are entangled in an algebraic relation that
allows to derive a subset of pebbles once another subset is available. They
show that this is possible in practice: the simplest example is storing the
exclusive or of several labels, but more complex encodings are possible, e.g.
based on polynomials. Interestingly, under some conjectures, they have shown
that the general computational adversary can be reduced with minimal security
loss to a graph-restricted adversary with entangled pebbles. However, these
conjectures have been later disproved in [32].

###  10.3 Bounds on random bitstrings

Before proving Theorem 1, we need some preliminary definitions and results.
Let $S_{c}=\sum_{j=0}^{c}\binom{m}{j}{(2^{w}-1)}^{j}$ for $c\geq 0$. This
coincides with the cardinality of a Hamming sphere over an alphabet of size
$2^{w}$ as defined in [17].

######  Lemma 17.

If $0\leq c<m$ and $2^{w}\geq m+3$ then $m(m+1)\binom{m}{c}{(2^{w}-1)}^{c}\geq
2^{w}\cdot S_{c-1}$.

###### Proof.

By induction on $c$. The base case $c=0$ follows directly. We need to prove
the induction step: $m\cdot(m+1)\cdot\binom{m}{c+1}\cdot{(2^{w}-1)}^{c+1}\geq
2^{w}\cdot S_{c}$. First we prove:

$\begin{split}&m(m+1)\binom{m}{c+1}{(2^{w}-1)}^{c+1}\\\ &\geq
m(m+1)\binom{m}{c}{(2^{w}-1)}^{c}+2^{w}\binom{m}{c}{(2^{w}-1)}^{c}\\\
&\iff\frac{m\cdot(m+1)}{c+1}\cdot(2^{w}-1)\geq\frac{m\cdot(m+1)}{m-c}+\frac{2^{w}}{m-c}\\\
&\iff\frac{m\cdot(m+1)\cdot(m-c)}{c+1}\cdot(2^{w}-1)\geq m\cdot(m+1)+2^{w}\\\
\end{split}$

which follows from $\frac{m\cdot(m+1)\cdot(m-c)}{c+1}\cdot(2^{w}-1)\geq
m\cdot(m+1)+2^{w}$. We conclude:

$\begin{split}&m\cdot(m+1)\cdot\binom{m}{c+1}\cdot{(2^{w}-1)}^{c+1}\\\ &\geq
m\cdot(m+1)\cdot\binom{m}{c}\cdot{(2^{w}-1)}^{c}+2^{w}\cdot\binom{m}{c}\cdot{(2^{w}-1)}^{c}\\\
&\geq 2^{w}\cdot
S_{c-1}\cdot{(2^{w}-1)}^{c-1}+2^{w}\cdot\binom{m}{c}\cdot{(2^{w}-1)}^{c}\\\
&=2^{w}\cdot S_{c}\qed\end{split}$

######  Lemma 18.

If $y\geq m+w$ and $c$ is maximal s.t. $S_{c}\leq 2^{y}$, then
$c\geq\left\lceil\frac{y-m-w+1}{w}\right\rceil$.

###### Proof.

Assume the contrary,
$c<\left\lceil\frac{y-m-w+1}{w}\right\rceil\implies(c+1)\cdot w+m\leq y$.
Then:

$\begin{split}&S_{c+1}=\sum_{j=0}^{c+1}\binom{m}{j}\cdot{(2^{w}-1)}^{j}\leq\sum_{j=0}^{c+1}\binom{m}{j}\cdot{(2^{w}-1)}^{c+1}\\\
&\leq 2^{m}\cdot{(2^{w}-1)}^{c+1}<2^{m+w\cdot(c+1)}\leq 2^{y}\end{split}$

which is a contradiction, as $c$ was the largest integer with this condition.
∎

Denote by $d(\psi,\psi^{\prime})$ the number of blocks in which two bitstrings
of size $m\cdot w$ differ. For a set $R\subseteq\bin^{n\cdot w}$, let
$d_{c}(R,\psi^{\prime})$ the number of $\psi\in R$ s.t.
$d(\psi,\psi^{\prime})\geq c$.

######  Lemma 19.

If $c\geq 1$, $\psi^{\prime}\in\bin^{m\cdot w}$, $R\subseteq\bin^{m\cdot w}$
then $d_{c}(R,\psi^{\prime})\geq\abs{R}-S_{c-1}$.

###### Proof.

If $\abs{R}\leq S_{c-1}$ the claim is trivial. Assume $\abs{R}>S_{c-1}$.
Notice that there are exactly $\binom{m}{j}{(2^{w}-1)}^{j}$ bitstrings $r$ of
size $m\cdot w$ such that $d(\psi,\psi^{\prime})=j$. Then, there are at most
$\sum_{j=0}^{c-1}\binom{m}{j}{(2^{w}-1)}^{j}=S_{c-1}$ bitstrings in $R$ such
that they differ from $\psi^{\prime}$ in less than $c$ blocks. ∎

######  Lemma 20.

If $c\geq 1,y\geq 0$ are integers, $\cup_{i=1}^{k}R_{i}$ is a partition of
$\bin^{m\cdot w}$ with $k\leq 2^{m\cdot w-y}$, and
$\psi^{\prime}_{i}\in\bin^{m\cdot w}$, then
$\sum_{i=0}^{k}d_{c}(R_{i},\psi^{\prime}_{i})\geq 2^{m\cdot
w-y}\cdot(2^{y}-S_{c-1})$.

###### Proof.

Without loss of generality assume $k=2^{m\cdot w-y}$ (we can always add empty
sets to the partition). By Lemma 19,
$d_{c}(R_{i},\psi^{\prime}_{i})\geq\abs{R_{i}}-S_{c-1}$. Adding for all
$R_{i}$:

$\sum_{i=0}^{k}d_{c}(R_{i},\psi^{\prime}_{i})\geq\sum_{i=0}^{k}\left(\abs{R_{i}}-S_{c-1}\right)=2^{m\cdot
w-y}\cdot(2^{y}-S_{c-1})\qed$

See 1

###### Proof.

Next we prove the second result. Assume that $y\geq m+w$ and $2^{w}\geq m+3$.
For each $R_{\sigma}$ as in the proof for the first result, we will be
interested in lower-bounding the number of errors that $\mathcal{A}_{1}$ makes
while answering the queries of a challenger using some $\psi\in R_{\sigma}$.
Notice this is exactly $d(R_{\sigma},\psi^{\prime})$ defined above. Clearly
the set of all possible $R$ is a partition of $\bin^{m\cdot w}$ with size at
most $2^{m\cdot w-y}$. Let $c$ be the largest integer such that $S_{c}\leq
2^{y}$ holds. By Lemma 18, we have that
$c\geq\left\lceil\frac{y-m-w+1}{w}\right\rceil$. Let
$\mathcal{I}^{2}_{\mathsf{good}}$ be the set of all substrings $\psi$ such
that $\mathcal{A}_{1}$ makes at least $c$ errors while answering queries about
$\psi$. From Lemma 20 we deduce that
$\abs{\mathcal{I}^{2}_{\mathsf{good}}}\geq 2^{m\cdot w-y}\cdot s$, where
$s=2^{y}-S_{c-1}$. By Lemma 17:

$\begin{split}&2^{m\cdot w}=2^{m\cdot w-y}\left(S_{c-1}+s\right)\\\ &\leq
2^{m\cdot w-y}\left(m(m+1)\cdot
2^{-w}\binom{m}{c}\cdot{(2^{w}-1)}^{c}+s\right)\\\ &\leq 2^{m\cdot
w-y}\cdot(m(m+1)\cdot 2^{-w}+1)\cdot s\\\
&\implies\abs{\mathcal{I}^{2}_{\mathsf{good}}}\geq 2^{m\cdot
w}\left(1-m(m+1)2^{-w}\right)\end{split}$

Then $\mathcal{A}_{1}$ makes $\left\lceil\frac{y-m-w+1}{w}\right\rceil$ errors
for $2^{m\cdot w}\cdot\left(1-(m^{2}+m)\cdot 2^{-w}\right)$ bitstrings. ∎

###  10.4 Reduction of PoSE security to depth-robustness

See 3

###### Proof.

Fix $i$. If the response to the challenge $o_{i}$ is not correct, then the
claim is trivial ($T_{i}$ is infinite). The case $o_{i}\in B$ is also trivial.
Assume $o_{i}\notin B$ and that the answer to the challenge $o_{i}$ is
correct. Consider the longest path ending in $o_{i}$, let it be
$\sequence{v_{1},v_{2},\ldots,v_{k-1},v_{k}=o_{i}}$, where
$k=\mathsf{llp}(o_{i},G\setminus B)$. As none of the nodes in this path are
blue, all their labels were computed by asking the oracle for the
corresponding value. Let $f_{j}$ be the smallest index such that
$Q_{x,f_{j}}=\ell^{-}(v_{j})$ for some $x$. As $v_{k}=o_{i}$, then $t_{i}\geq
f_{k}$.

We prove that $\forall j\colon 1\leq j<k$ we have $f_{j}<f_{j+1}$. Each
inequality can be proved using the same argument, so we prove only
$f_{1}<f_{2}$. As $v_{1}$ is not blue and $v_{2}$ is a successor of $v_{1}$,
then the query $\ell^{-}(v_{2})$ in round $f_{2}$ (which contains the label of
$v_{1}$) must have happened after the query $\ell^{-}(v_{1})$ in round
$f_{1}$. This implies $f_{2}>f_{1}$, as needed.

As $\forall i\colon f_{i}\geq 1$ then $f_{k}\geq k\implies T_{i}\geq k$. ∎

See 4

###### Proof.

We can assume $\abs{B}<m$, since the result trivially holds otherwise.
Therefore, from the definition of depth-robustness, there exist a set
$O^{\prime}\subseteq\set{o_{i}}\setminus B$ with $|O^{\prime}|\geq m-|B|$ s.t.
$\forall o_{i}\in O^{\prime}\colon\mathsf{llp}(o_{i},G\setminus B)\geq\gamma$.
From Lemma 3, we deduce $\forall o_{i}\in O^{\prime}\colon T_{i}\geq\gamma$.
Therefore, we deduce

$\underset{i\sample[m]}{\operatorname{\probname}}[T_{i}\geq\gamma]\geq\underset{i\sample[m]}{\operatorname{\probname}}[o_{i}\in
O^{\prime}]\geq 1-|B|m^{-1}\qed$

The next definition and lemma hold for general adversaries.

######  Definition 15 (Good oracle).

We say that $h\in H$ is a good oracle for an adversary
$\mathcal{A}=(\mathcal{A}_{0},\mathcal{A}_{1})$ if we have
$\abs{B}\leq\left\lceil\frac{M}{w-\log(m\cdot q)}\right\rceil$.

######  Lemma 21.

If $\mathcal{A}$ has parameters $(m,1,w)$ and $H_{\mathsf{good}}\subseteq H$
be the corresponding set of good oracles. Then
$\abs{H_{\mathsf{good}}}\geq\abs{H}\cdot(1-2^{-w+\log(m\cdot q)})$.

###### Proof.

The proof follows closely the one of Lemma 7, but must be extended for general
adversaries.

As before, the encoder will output $0$ if $h\in H_{\mathsf{good}}$. Else, it
will output $\sigma,p,c,c^{\prime}$, where the new value $p$ is a list of
indices, where each index $a_{i}$ corresponds to the $i$-th output of
${\cal{}S}$, and indicates that it contains the first appearance of the label
of a blue node. Each of these pairs can be encoded using $\log(m\cdot q)$
bits.

The decoder will also execute ${\cal{}S}$ as before. The difference is that
when ${\cal{}S}$ outputs a value, only if the corresponding index is in $p$,
it will extract and store the labels of the blue nodes associated with that
output. At the end of execution, the decoder will have stored all labels of
blue nodes.

As the size of $p$ is at most the number of blue nodes, the size of the
encoding is at most $M+\abs{B}\cdot\log(m\cdot q)+\log\abs{H}-\abs{B}\cdot w$,
and it is correct with probability $\delta=1-\abs{H_{\mathsf{good}}}/\abs{H}$.
From Lemma 6 we deduce:

$\begin{split}&M+\log\abs{H}-\abs{B}\cdot(w-\log(m\cdot
q))\geq\log\abs{H}+\log(\delta)\\\ &\implies\delta\leq 2^{-w+\log(m\cdot
q)}\quad\text{from $\abs{B}>\left\lceil\frac{M}{w-\log(m\cdot
q)}\right\rceil$}\end{split}$

Hence $\abs{H_{\mathsf{good}}}=(1-\delta)\cdot\abs{H}\geq(1-2^{-w+\log(m\cdot
q)})\cdot\abs{H}$. ∎

###  10.5 Graph construction

See 4

###### Proof.

Assume the contrary, there exists a set $R$ such that there is no path
containing $2^{n}-\abs{R}$ nodes from $\mathsf{Base}(G_{n})$. Consider the
partition $B\cup R_{1}\cup\ldots\cup R_{k}$ of the vertices in $R$ such that
the nodes in each partition $R_{i}$ belong to exactly one subgraph $H_{i}$
(defined by some $\overset{H}{\to}$, or the $\mathsf{Center}$ of some
component) and $B=R\cap\mathsf{Base}(G_{n})$. If $R^{\prime}_{i}$ is the set
of nodes guaranteed to exist by Lemma 8, then removing $R^{\prime}_{i}$
instead of $R_{i}$ doesn’t increase the connectivity between nodes in
$\mathsf{Base}(G_{n})$. We deduce that if the result is true for $R^{\prime}$,
then after removing the nodes in $R^{\prime}=B\cup
R^{\prime}_{1}\cup\ldots\cup R^{\prime}_{k}$ from $G_{n}$, there is a path
containing $2^{n}-\abs{R^{\prime}}\geq 2^{n}-\abs{R}$ nodes from
$\mathsf{Base}(G_{n})$. The vertices in $R^{\prime}$ are either in the input
or output of some $H_{i}$, or in $\mathsf{Base}(G_{n})$.

It remains to prove that if the nodes in $R^{\prime}$ are removed, there is a
path with the required features. We prove this by induction in a stronger
statement: in $G_{n}\setminus R^{\prime}$ there exists a path $L$ with the
required properties such that the nodes in
$V(L)\cap\mathsf{Base}(\mathsf{Right}(\mathsf{Left}^{k}(G_{n})))$ are
reachable from $\mathsf{In}(\mathsf{Center}(\mathsf{Left}^{k}(G_{n})))$ for
$0\leq k<n$.

The base cases $G_{0}$ and $G_{1}$ can be checked manually. For the induction
step assume in $R^{\prime}$ there are $l,r,c$ nodes from
$\mathsf{Left}(G_{n+1})$, $\mathsf{Right}(G_{n+1})$ and
$\mathsf{Center}(G_{n+1})\cup\left(\mathsf{Out}(\mathsf{Center}(G_{n+1}))\triangleright\mathsf{Right}(G_{n+1})\setminus\mathsf{Right}(G_{n+1})\right)$,
respectively. By the induction hypothesis, there is a path $L_{l}$ in
$\mathsf{Left}(G_{n+1})$ with the required properties, i.e.
$\abs{V(L_{l})\cap\mathsf{Base}(\mathsf{Left}(G_{n+1}))}\geq 2^{n}-l$. There
is also $L_{r}$ in $\mathsf{Right}(G_{n+1})$.

We will finish the proof by case analysis. If $r+c\geq 2^{n}$, then
$2^{n}-l\geq 2^{n+1}-\abs{R^{\prime}}$ and $L=L_{l}$ has the required
properties. Else, $r+c<2^{n}$. Let
$c_{i}=\abs{R^{\prime}\cap\mathsf{In}(\mathsf{Center}(G_{n+1}))}$.

Next we prove that there is a list of nodes $F\subseteq
V(L_{r})\cap\mathsf{Base}(\mathsf{Right}(G_{n+1}))$ such that $\abs{F}\geq
2^{n}-r-c+c_{i}$ and all nodes in $F$ are reachable from at least one node in
$\mathsf{Out}(\mathsf{Center}(G_{n+1}))$.

Consider a node $v\in V(L_{r})\cap\mathsf{Base}(\mathsf{Right}(G_{n+1}))$. Let
$k$ be the largest such that $v\in\mathsf{Left}^{k}(\mathsf{Right}(G_{n+1}))$,
and $G_{v}=\mathsf{Left}^{k}(\mathsf{Right}(G_{n+1}))$. If $k=n$, then the
only way that this node is not reachable from
$\mathsf{Out}(\mathsf{Center}(G_{n+1}))$ is if its predecessor in that set
belongs to $R^{\prime}$. If $k<n$, then by the induction hypothesis, given
that $v\in\mathsf{Base}(\mathsf{Right}(G_{v}))$, then $v$ is reachable from a
node in $\mathsf{In}(\mathsf{Center}(G_{v}))$, call this node $w$. The only
way that $v$ is not reachable from $\mathsf{Out}(\mathsf{Center}(G_{n+1}))$
through $w$ is if all paths in the connector $\bar{H}$ (which is isomorphic to
$H_{n-k-1}$) from this set to $w$ are covered by nodes in $R^{\prime}$. As $w$
is not covered, this is only possible if all nodes from
$\mathsf{Out}(\mathsf{Center}(G_{n+1}))$ connected to $\mathsf{In}(\bar{H})$
are in $R^{\prime}$, which are exactly $2^{n-k-1}$ nodes. But there are at
most $2^{n-k-1}$ nodes in $\mathsf{Base}(\mathsf{Right}(G_{v}))$. Applying the
previous deduction for all $v$, we deduce that the number of nodes in
$V(L_{r})\cap\mathsf{Base}(\mathsf{Right}(G_{n+1}))$ not reachable from
$\mathsf{Out}(\mathsf{Center}(G_{n+1}))$ is at most the number of nodes that
were removed from $\mathsf{Out}(\mathsf{Center}(G_{n+1}))$. As this number is
at most $c-c_{i}$, the claim follows.

Consider now the path $P_{F}$ determined by the list of nodes $F$. All these
nodes are reachable from $\mathsf{Out}(\mathsf{Center}(G_{n+1}))$.
Furthermore, as $c_{i}\leq c+r<2^{n}$, these nodes are also reachable from
some node in $\mathsf{In}(\mathsf{Center}(G_{n+1}))$. We will concatenate this
path with a suitable subset of $L_{l}$. Let $D\subseteq
L_{l}\cap\mathsf{Base}(\mathsf{Left}(G_{n+1}))$ be the set of nodes that are
connected to a node in $\mathsf{In}(\mathsf{Center}(G_{n+1}))$. Then
$\abs{D}\geq 2^{n}-l-c_{i}$. Consider the path $P_{D}$ determined by the list
of nodes $D$. This path can be extended with $P_{F}$ and the resulting path
contains at least $2^{n}-l-c_{i}+2^{n}-r-c+c_{i}=2^{n+1}-\abs{R^{\prime}}$
nodes in $\mathsf{Base}(G_{n+1})$, as was needed. ∎