# Automated verification of dynamic root of trust protocols
(long version)

Sergiu Bursuc University of Bristol, UKDept. of Informatics, University of
OsloWuhan Digital Engineering Institute, China Christian Johansen Dept. of
Informatics, University of OsloWuhan Digital Engineering Institute, China
Shiwei Xu Wuhan Digital Engineering Institute, China

###### Abstract

Automated verification of security protocols based on dynamic root of trust,
typically relying on protected hardware such as TPM, involves several
challenges that we address in this paper. We model the semantics of trusted
computing platforms (including CPU, TPM, OS, and other essential components)
and of associated protocols in a classical process calculus accepted by
ProVerif. As part of the formalization effort, we introduce new equational
theories for representing TPM specific platform states and dynamically loaded
programs.

Formal models for such an extensive set of features cannot be readily handled
by ProVerif, due especially to the search space generated by unbounded
extensions of TPM registers. In this context we introduce a transformation of
the TPM process, that simplifies the structure of the search space for
automated verification, while preserving the security properties of interest.
This allows to run ProVerif on our proposed models, so we can derive
automatically security guarantees for protocols running in a dynamic root of
trust context.

###### Contents

  1. 1 Introduction
  2. 2 Related work
  3. 3 Preliminaries
    1. 3.1 Trusted computing
    2. 3.2 ProVerif process calculus
  4. 4 Formalisation
    1. 4.1 Cryptographic primitives and platform constants
    2. 4.2 Dynamically loaded programs
    3. 4.3 Platform state
    4. 4.4 Read and write access
    5. 4.5 Communication channels
    6. 4.6 The trusted platform module
    7. 4.7 Dynamic root of trust: launch
    8. 4.8 Dynamic root of trust: execution
    9. 4.9 Security properties in the formal model
  5. 5 Process transformation for automated verification
    1. 5.1 Sketch of correctness proofs
  6. 6 Verification
  7. 7 Further work
  8. A Operational semantics of the process calculus
  9. B ProVerif code

##  1 Introduction

A hardware root of trust, including dynamic measurement of programs and their
protected execution, is a promising concept for ensuring the integrity of a
platform and the privacy of sensitive data, despite powerful software
attackers [19]. This relies on the idea that hardware is more difficult to
compromise than software, and therefore, it can play a crucial role in
protocols for handling sensitive data. When a secure computing platform is
needed, a special sequence of instructions allows for a trusted piece of
hardware to attest the integrity of the software to be run and to give access
to data in a protected environment.

However, turning this idea into a secure design and implementation is not
easy, as various attacks have shown [13, 29]. For more assurance, one could
use models and tools that allow automated verification of desired properties
against trusted computing protocols and implementations. One main challenge
for automated verification is the size and number of components involved in
running programs protected by a dynamic root of trust. Furthermore, messages
of such protocols consist not only of data, but also of programs that are to
be executed on the platform, and that can be supplied by an attacker or by an
honest participant. At the same time, modelling the platform configuration
registers (PCR) of the trusted platform module (TPM) [20] poses problems,
because PCRs can be extended an unbounded number of times. Even the most
efficient symbolic methods struggle with the structure of the resulting search
space [6, 12].

_Our contributions._ We propose a formal model in the ProVerif process
calculus [7] for the technology and for the security properties of a dynamic
root of trust (as instantiated by Intel’s Trusted Execution Technology or
AMD’s Secure Virtual Machine). Our model is more realistic than [12] and it
covers aspects of trusted computing that [10] does not cover (section 4). We
show how a platform state can be naturally represented as a term in ProVerif
(or applied pi-calculus [1, 27]) and how operations on the platform state can
be expressed as equations in a term algebra (sections 4.3 and 4.4).
Furthermore, we show how to model the dynamic loading of protected programs.
Our model is simple and does not require heavy encodings, being based on the
classic idea of processes as data, with a twist to take protection into
account (section 4.2).

We propose a new abstraction to model the extension of PCR registers that
allows automated verification for a larger class of protocols than in [12]. We
show how to over-approximate the model of the TPM such that the structure of
the search space is simplified, without losing possible attacks or introducing
false attacks. The main idea is that we can let the attacker set the PCR to
_any_ value, as long as it is “big enough” (section 5).

Putting the formalisation and the abstraction together, we obtain the first
automated verification for a realistic model of a dynamic root of trust. As
security properties, we prove code integrity (the PCR values correctly record
the measurement of the platform) and secrecy of sealed data (only a designated
program can access data that has been sealed for its use in a protected
environment).

Acknowledgements:  We would like to thank Cas Cremers and several reviewers
for helping improve this work.

##  2 Related work

A programming language and a logic for specifying trusted computing protocols
and properties are proposed in [10]. The setting is quite expressive and it
allows the analysis of protocols similar to the ones that we study in this
paper. [10] does not consider the seal/unseal functions of the TPM, but their
language could be extended to capture them. However, the formal analysis of
[10] is manual, and considering the complexity of the proofs involved, the
lack of automation can be a limitation. We also believe some of their axioms
(like those linking the PCR values to a late launch action) could be
decomposed into more atomic formulas, in closer relation to the computational
platform. Their security properties include correctly reading PCR values and
the ability of honest parties to launch roots of trust; our property of code
integrity, modeled as a correspondence assertion, can be seen as an additional
constraint for these two events.

The analysis of [12] is automated with ProVerif and is based on a Horn clause
model. Microsoft’s Bitlocker protocol is shown to preserve the secrecy of data
sealed against a static sequence of PCR values. Their model considers a static
root of trust, and cannot handle dynamically loaded programs. Furthermore,
there is no way to express a program that has access to data in a protected
environment. Without a richer model of platform states, code integrity
properties cannot be expressed either. To help with automation, [12] shows
that, for a specific class of Horn clauses, it is sound to bound the number of
extensions of PCR registers. Since our model is in applied pi-calculus and our
security properties are different, we cannot directly rely on their result,
and we propose a new way of handling the unbounded PCR extension problem.

_Information-flow security and computational models._ [14] presents a secure
compiler for translating programs and policies into cryptographic
implementations, distributed on several machines equipped with TPMs. A
computational model capturing functionalities similar to ours, in conjunction
with additional features such as authenticated key exchange, was recently
proposed in [5]. Our models are more abstract, yet could be related to
particular implementations - a closer connections between formal and
computational models could be explored in future.

_Unbounded search space._ Several works tackle the problem of an unbounded
search space for automated verification, but technically they are all based on
principles that cannot be translated to PCR registers. In [25], it is shown
that, for a class of Horn clauses, verification of protocols with unbounded
lists can be reduced to verification of protocols with lists containing a
single element. In [9], it is shown that to analyse routing protocols it is
sufficient to consider topologies with at most four nodes. These are strong
results, based on the fact that the elements of a list or the nodes in a route
are handled uniformly by the protocol. Similar results, in a different
context, are shown in [16, 15]. Their reductions are based on the principle of
data independence for memory stores. In [22] and respectively [2], it is shown
how to handle an unbounded number of Diffie-Hellman exponentiations and
respectively reencryptions in ProVerif. Surprisingly, the underlying
associative-commutative properties of Diffie-Hellman help in [22], while [2]
can rely on the fact that a re-encryption does not change the semantics of a
ciphertext. Another case where an unbounded number of operations is
problematic is file sharing [8]. In order to obtain an automated proof, [8]
assumes a bound on the number of access revocations, without providing
justifications for soundness. A sound abstraction for an unbounded number of
revocations, in a more general setting, is proposed in [24]. Still, it is
specialized to databases and it seems to rely on the same principle as several
results mentioned above: it does not matter what the data is, it only matters
to what set it belongs.

_Tools and models for non-monotonic state._ StatVerif [3] is aimed
specifically for the verification of protocols relying on non-monotonic
states, encoding the semantics of applied pi-calculus enriched with states
into a set of Horn clauses for input to ProVerif. Tamarin [28] is based on
multiset rewriting and inherently allows specification and automated reasoning
for non-monotonic states, where the set of facts can both augment and
decrease. SAPIC [21] takes as input a stateful variant of applied pi-calculus
and produces a multiset-based model, which is then analysed using Tamarin.

StatVerif [3], SAPIC [21], and Tamarin directly [23], have been used with
success to verify security protocols that rely on non-monotonic states or
trusted hardware: $PKCS\sharp 11$ for key management [26], YubiKey for user
authentication [32], and protocols for contract signing [17]. Our models, on
the other hand, are tailored for direct input to ProVerif, while extending the
scope of formal models for platform state operations and dynamic root of trust
protocols based on a TPM [18, 19, 20]. It is one of our main interests for
future work to see how the models of this paper can be analysed with tools
like [28, 21, 3], in order to obtain a closer alignment with the state
semantics of real systems.

##  3 Preliminaries

###  3.1 Trusted computing

We first describe the required computing platform (hardware and software) and
then describe the considered class of dynamic root of trust protocols.

A. Computing platform. We consider a general purpose computing platform
equipped with a CPU and a TPM (both trusted), as well as a generic untrusted
operating system.

_Trusted hardware._ Trusted computing relies on the CPU and the TPM111See
recent book [4] detailing the TPM version 2.0 specification and
implementations. to perform certain operations whose integrity cannot be
compromised by any software attacker. Regarding the TPM, two of its trusted
features are fundamental for the applications that we consider in this paper:
the ability to record a chain of values in its _platform configuration
registers_ (PCR) and the ability to _seal data_ against specified values of
the PCR.

The TPM allows the PCR to be _reset_ only by the CPU or by a system reset. On
the other hand, the PCR can be _extended_ with any value by software. If a PCR
records a value $p$ and is extended with a value $v$, the new value of the PCR
is $\texttt{h}((p,v))$, i.e. the result of applying a hash function to the
concatenation of $p$ and $v$. Crucially, these are the only two ways in which
the values of a PCR can be modified. The role of the PCR for the protocols
that we consider in this paper is to store the measurement of programs,
recording a chain of loaded programs. When data $d$ is _sealed_ against some
specified value $v$ of the PCR, the TPM stores $d$ internally and can release
it in future only if the value recorded in its PCR matches the value $v$
against which $d$ was sealed.

For the purpose of formal verification, we are flexible about who exactly of
the CPU or the TPM is doing a trusted operation, like measuring, sealing, etc.
This depends on the implementation, e.g., the Intel SGX can do all the
operations of a TPM. Changing the formalization from this paper to fit a
particular implementation should be easy.

_Privileged software._ When a system interrupt is triggered (e.g by network
communication or user interface action), all physical memory can be accessed
by the system management interrupt (SMI) handler. This means that any memory
protection mechanism, in particular the protocols that we consider in this
paper, must either disable interrupts for their whole duration (not practical
in general) or else rely on the fact that the SMI handler cannot be
compromised. That is why the SMI handler is stored in a memory area called
SMRAM, which enjoys special hardware protection. Still, as shown in [13, 29],
the security guarantees of trusted computing can be violated using the CPU
caching mechanism to compromise the SMI handler. Roughly, these attacks work
because the protection of the SMRAM is not carried on to its cached contents.
A countermeasure against such attacks, that we also adopt in this paper at an
abstract level, is a software transfer monitor (STM) [18]. It also resides in
the SMRAM, but it cannot be cached while a dynamic root of trust is running
(special registers of the CPU should ensure that), and its role is to protect
some memory regions from the SMI handler.

B. Dynamic root of trust. We consider the technology of dynamic measurement
and protected execution, also called dynamic root of trust (DRT), as
instantiated for example in Intel’s Trusted Execution Technology (TXT) or AMD
Secure Virtual Machine (SVM), and as illustrated in Fig. 1.

Trust assumptions Untrusted Measured Trusted OS INIT CPU SMI PP TPM STM

Figure 1: Execution flow in a Dynamic Root of Trust (DRT)

The goal of DRT is to establish a protected execution environment for a
program, where private data can be accessed without being leaked to an
attacker that controls the operating system. Assume a program, that we will
call PP (called measured launch environment on Intel and secure kernel on
AMD), needs to be loaded in a protected environment. The first entry point of
the DRT protocol is a trusted instruction of the CPU (called GETSEC[SENTER] on
Intel and SKINIT on AMD), that takes as input the program PP. To help with the
establishment of a protected environment, the CPU also receives as input
another program, that we will call INIT (called SINIT authenticated code
module on Intel and secure loader on AMD). The DRT launch and execution
sequence can then be summarized as follows:

1.

The CPU receives a request from the operating system containing the INIT code
and the PP code. The system interrupts are disabled at this step, as an
additional protection against untrusted interrupt handlers.

2-3.

A software attacker that controls the operating system could compromise INIT
and the STM, and that is why the CPU computes their measurement and extends
the result into the TPM, to keep a trace of programs responsible for the DRT.
Measuring a program means applying a hash function to its source code. This
computation is performed on the CPU and is trusted, entailing that the
resulting value is a correct measurement of INIT and STM. The CPU communicates
with the TPM on a trusted channel and requests that the PCR is reset and
extended with the resulting value (h(INIT),h(STM)).

4-7.

The INIT program is loaded and it computes the measurement of the PP program,
extending it into the PCR. The communication between INIT and the TPM is
performed on a private channel established by the CPU. INIT also allocates
protected memory for the execution of PP and loads it.

8.

The PP program can re-enable interrupts once appropriate interrupt handlers
are set. Furthermore, it can now request the TPM to unseal data that has been
sealed against the current PCR value, and it can have access to that data in a
protected environment. The communication between PP and the TPM is performed
on a private channel established by the CPU.

9.

Before ending its execution, the PP program extends the PCR with a dummy
value, to record that the platform state is not to be trusted any more.

Since the OS is untrusted it can supply malicious programs INIT and PP.
Therefore, INIT, PP and the STM are not trusted, but they are _measured_. If
their measurement does not correspond to some expected _trusted_ values, this
will be recorded in the TPM and secret data will not be unsealed for this
environment.

Security goals. Let us summarize the two main security goals of the DRT.

_Code integrity:_ In any execution of the platform, if the measurements
recorded in the PCR value of the TPM correspond to the sequence of programs
$\mathcal{P}_{\texttt{INIT}}$, $\mathcal{P}_{\texttt{STM}}$,
$\mathcal{P}_{\texttt{PP}}$, then the platform is indeed running a DRT for the
protected execution of $\mathcal{P}_{\texttt{PP}}$ in the context of
$\mathcal{P}_{\texttt{INIT}}$ and $\mathcal{P}_{\texttt{STM}}$. In particular,
this means that the programs $\mathcal{P}_{\texttt{PP}}$,
$\mathcal{P}_{\texttt{INIT}}$ and $\mathcal{P}_{\texttt{STM}}$ cannot be
modified while a DRT is running.

_Secrecy of sealed data:_ Any secret data that is sealed only against a PCR
value recording the sequence of programs $\mathcal{P}_{\texttt{INIT}}$,
$\mathcal{P}_{\texttt{STM}}$, $\mathcal{P}_{\texttt{PP}}$, is only available
for the program $\mathcal{P}_{\texttt{PP}}$, in any execution of the platform.

###  3.2 ProVerif process calculus

We review ProVerif [6, 7] and the special way in which we use (a restriction
of) its input calculus in our modelling.

A. Terms, equational theories and deducibility. We consider an infinite set of
_names_ , $a,b,c,k,n\ldots$, an infinite set of _variables_ , $x,y,z,\ldots$
and a possibly infinite set of _function symbols_ $\mathcal{F}$. Names and
variables are _terms_ ; new terms are built by applying function symbols to
names, variables and other terms. We split $\mathcal{F}$ into two disjoint
sets of _public_ functions $\mathcal{F}^{\texttt{pub}}$ and _private_
functions $\mathcal{F}^{\texttt{priv}}$. Public functions can be applied by
anyone to construct terms, including the attacker, whereas private functions
can be applied only as specified by the protocol. When
$\mathcal{F}^{\texttt{priv}}$ is not explicit, we assume that all functions
are public.

A _substitution_ $\sigma$ is a partial function from variables to terms. The
replacement of every variable $x$ with $x\sigma$ in a term $T$ is denoted by
$T\sigma$. A _context_ is a term $\mathcal{C}[\\_]$ that contains a special
symbol $\\_$ in place of a subterm. For a context $\mathcal{C}[\\_]$ and a
term $T$, we denote by $\mathcal{C}[T]$ the term obtained by replacing $\\_$
with $T$ in $\mathcal{C}[\\_]$. For any formal object $\cal D$, we denote by
$\texttt{sig}({\cal D})$ the set of function symbols appearing in $\cal D$,
and by $\texttt{top}(T)$ the outer-most function symbol in term $T$.

En equational theory $\mathcal{E}$ is defined by a set of rewrite rules
$U_{1}\rightarrow V_{1},\ldots,U_{n}\rightarrow V_{n}$, where
$U_{1},\ldots,U_{n},V_{1},\ldots,V_{n}$ are terms with variables. A term $U$
rewrites to $V$ in one step, denoted by $U\rightarrow V$, if there is a
context $\mathcal{C}[\\_]$, a substitution $\sigma$ and an index
$i\in\\{1,\ldots,n\\}$ such that $U=\mathcal{C}[U_{i}\sigma]$ and
$V=C[V_{i}\sigma]$. Several rewrite steps from $U$ to $V$ are denoted by
$U\rightarrow^{*}V$. We consider only convergent equational theories, i.e.,
for any term $T$ there exists a unique non-reducible term $T\\!\\!\downarrow$
s.t. $T\rightarrow^{*}T\\!\\!\downarrow$. We write $U=_{\mathcal{E}}V$ iff
$U\\!\\!\downarrow=V\\!\\!\downarrow$. ProVerif also allows operations on
sequences: for all $n$, from any terms $T_{1},\ldots,T_{n}$, one can derive
the term $(T_{1},\ldots,T_{n})$, and conversely.

_Deduction._ Given an equational theory $\mathcal{E}$, a set of terms $S$ and
a term $T$, the ability of an attacker to obtain $T$ from $S$ is captured by
the deduction relation $S\vdash_{\mathcal{E}}T$ (or simply $S\vdash T$ when
$\mathcal{E}$ is understood) defined as being true iff:
$\bullet$ there exists a term $T^{\prime}\in S$ such that
$T^{\prime}=_{\mathcal{E}}T$, or
$\bullet$ there are terms $T_{1},\ldots,T_{n}$ such that
$S\vdash_{\mathcal{E}}T_{1},\ldots,S\vdash_{\mathcal{E}}T_{n}$ and a function
symbol $f\in\mathcal{F}^{\texttt{pub}}$ such that
${f(T_{1},\ldots,T_{n})=_{\mathcal{E}}T}$

B. Processes and operational semantics.

$P,Q,R::=$
---
|  | $0$ | null process
---|---
$P\mid Q$ | parallel composition
$!P$ | replication
$\texttt{new}\,n;P$ | name restriction
|  | $\texttt{in}(U,T);P$ | message input on $U$
---|---
$\texttt{out}(U,T);P$ | message output on $U$
$\texttt{if }U=V\texttt{ then }P\texttt{\;else\;}Q$ | conditional
$\texttt{let\; }x=T\texttt{\; in\; }{P}$ | term evaluation
Figure 2: Process algebra, with $n$ a name, $x$ a variable, and $T,U,V$ terms.

_Processes_ of the calculus are built according to Fig. 2. Replication spawns
instances of a process: $!P$ is formally equivalent with $P\;|\;!P$. Names
introduced by new are called _bound_ or _private_ ; they represent the
creation of fresh data. Names that are not bound are called _free_ , or
_public_. The term $T$ in an input $\texttt{in}(U,T)$ allows to specify
filters for messages received on $U$: a message $M$ will be accepted only if
there is a substitution $\sigma$ such that $M=T\sigma$. A variable $x$ is
_free_ in a process $P$ if $P$ neither contains $x$ in any of its input
patterns nor does it contain any term evaluation of the form $x=T$.
Consecutive term evaluations can be written together as $\texttt{let\;
}(x_{1},\ldots,x_{n})=(T_{1},\ldots,T_{n})\texttt{\; in\; }{P}$. The notions
of substitution, contexts and normal forms translate to processes as expected.

_Operational semantics_ is defined as a transition system on configurations of
the form $({\cal N},\mathcal{M},\mathcal{P})$, where: ${\cal N}$ is a set of
fresh names created during the execution of a process; $\mathcal{M}$ is the
set of terms made available to the attacker; and $\mathcal{P}$ is the set of
processes executing in parallel at a given point in time. We write $({\cal
N},\mathcal{M},\mathcal{P})\rightarrow^{*}({\cal
N}^{\prime},\mathcal{M}^{\prime},\mathcal{P}^{\prime})$ if the configuration
$({\cal N}^{\prime},\mathcal{M}^{\prime},\mathcal{P}^{\prime})$ can be reached
from $({\cal N},\mathcal{M},\mathcal{P})$ in zero or more executions steps.
Such a sequence of execution steps is called a trace of $P$.

C. Security properties. The ability of an attacker to learn a term $T$ by
interacting with a process $P$ is denoted by $P\models\texttt{Att}(T)$,
defined as true iff there exists a process $Q$, with
$\texttt{sig}(Q)\cap\mathcal{F}^{\texttt{priv}}=\emptyset$, such that $({\cal
N}_{\texttt{init}},\emptyset,\\{P\mid Q\\})\rightarrow^{*}({\cal
N}^{\prime},\mathcal{M}^{\prime},\mathcal{P}^{\prime})$ and
$\mathcal{M}\vdash_{\mathcal{E}}T$, for some configuration $({\cal
N}^{\prime},\mathcal{M}^{\prime},\mathcal{P}^{\prime})$. Intuitively, $Q$
represents any computation that can be performed by the attacker.

A (simplified) _correspondence assertion_ [7] is a formula of the form

$\texttt{Att}(T)\implies
false\;\;\;\;\text{or}\;\;\;\;\texttt{Att}(T)\implies(U=V).$

For a correspondence assertion $\texttt{Att}(T)\implies\Phi$ as above, we have

$P\models\texttt{Att}(T)\implies\Phi\;\;\;\;\text{iff}\;\;\;\;\forall\sigma.\;\;[\;\;(P\models\texttt{Att}(T\sigma))\implies\Phi\sigma\;\;]$

Correspondence assertions of the first type model the _secrecy_ of $T$, while
those of second type enforce the constraint $U=V$ for deducible terms matching
the pattern $T$ (typically the terms $U,V$ will share variables with $T$).

##  4 Formalisation

Our formal specification for the trusted computing platform and protocols
described in section 3.1 assumes an attacker that controls the operating
system and can execute a DRT any number of times, with any INIT and PP
programs. Moreover, using the CPU cache, the attacker can compromise the STM
and SMI handler, and use them to access protected memory. The attacker has
access to all TPM functions. However, we assume that the attacker cannot
compromise the CPU nor the TPM, and that the platform state can only be
modified according to the equations that we present in section 4.4.

We model a system state as a term that can be updated by the CPU process, the
TPM process and, once it has been output on a public channel, by the attacker.
Multiple system states can be explored in parallel by the attacker, whose
knowledge monotonically accumulates the set of all reachable states. This is
an abstraction with respect to a real platform, where the CPU and the TPM have
their own internal state, part of a global, non-monotonic system state. We
also have a simplified model of TPM sealing: in reality, it relies on
encryption with a TPM private key and refers to a specific system state; in
our model, it is represented by the pair of public/private functions
seal/unseal. For unsealing, the TPM process will require the input of a system
state and check that the corresponding unseal request is valid for that state.

###  4.1 Cryptographic primitives and platform constants

To model cryptographic primitives and various constants on the platform state,
we consider the signature $\mathcal{F}_{\texttt{data}}$, where
$\mathcal{F}_{\texttt{data}}^{\texttt{priv}}=\\{\texttt{unseal}/2\\}$ and

$\mathcal{F}_{\texttt{data}}^{\texttt{pub}}=\\{\texttt{p}_{\texttt{s}}/0,\texttt{p}_{\texttt{d}}/0,\texttt{true}/0,\texttt{false}/0,\texttt{h}/1,\texttt{senc}/2,\texttt{sdec}/2,\texttt{seal}/2\\}.$

We also consider the set of rewrite rules $\mathcal{E}_{\texttt{data}}$:

$\begin{array}[]{rcl}\texttt{sdec}(\texttt{senc}(x_{\texttt{val}},x_{\texttt{key}}),x_{\texttt{key}})&\rightarrow&x_{\texttt{val}}\\\
\texttt{unseal}(\texttt{seal}(x_{\texttt{val}},x_{\texttt{pcr}}),x_{\texttt{pcr}})&\rightarrow&x_{\texttt{val}}\end{array}$

The constant $\texttt{p}_{\texttt{d}}$ (resp. $\texttt{p}_{\texttt{s}}$)
represents the result of a dynamic (resp. static) PCR reset. A dynamic reset
marks the start of a dynamic root of trust, and can only be performed by the
CPU. The functions senc and sdec, and the corresponding rewrite rule, model
symmetric key encryption. The symbol h represents a hash function. Anyone can
seal a value, while the corresponding rewrite rule and the fact that unseal is
private ensure that a value can be unsealed only according to the
specification of the TPM.

###  4.2 Dynamically loaded programs

To model the fact that arbitrary programs can be dynamically loaded on the
platform state (e.g. for the roles of INIT and PP), we consider a new public
function symbol $\texttt{prog}/1$ and an infinite signature of _private
constants $\mathcal{F}_{\mathcal{P}}$_, containing a different constant
$n_{P}$ for every possible process $P$. Intuitively, the term
$\texttt{prog}(n_{P})$ is a public and unique identifier for the program $P$.
In a computational model, such an identifier can for example be obtained by
hashing the source code of $P$. The first action of a process that models a
program will be to output the corresponding program identity
$\texttt{prog}(n_{P})$ on a public channel.

On the other hand, the constant $n_{P}$ represents a _private entry point_ for
the program $P$. Specifically, we consider a private function get_entry and
the rewrite rule $\texttt{get\\_entry}(\texttt{prog}(x))\rightarrow x$. The
idea is that a trusted loader of programs (the CPU in our case) has access to
the private function get_entry and, using this rewrite rule, it can gain
access to the private entry point of any program. Now, $n_{P}$ can play the
role of a private channel between the trusted loader and the loaded program.
Furthermore, we can store program identifiers in the platform state, to record
what programs are loaded. Then, we can rely on $n_{P}$ to model the ability of
certain loaded programs to affect the platform state (shown in section 4.4).
We denote by $\mathcal{E}_{\texttt{prog}}$ the equational theory defined in
this subsection:
$\mathcal{F}_{\texttt{prog}}=\\{\texttt{prog}/1\\}\cup\mathcal{F}_{\mathcal{P}}\
,\hskip
12.91663pt\mathcal{E}_{\texttt{prog}}=\\{\texttt{get\\_entry}(\texttt{prog}(x))\rightarrow
x\\}$.

###  4.3 Platform state

To model a platform state, we consider the signature:

$\begin{array}[]{rcl}\mathcal{F}_{\texttt{state}}&=&\\{\texttt{state}/4,\texttt{tpm}/1,\texttt{cpu}/2,\texttt{smram}/2,\texttt{drt}/3\\}\end{array}$

where all the symbols of $\mathcal{F}_{\texttt{state}}$ are private. This
ensures that a platform state can be constructed or modified only according to
the specification, relying on equations that we present in subsection 4.4.
Intuitively, a term of the form

$\begin{array}[]{rl}\texttt{state}(&\texttt{tpm}(T_{\texttt{PCR}}),\texttt{cpu}(T_{\texttt{INT}},T_{\texttt{CACHE}}),\texttt{smram}(T_{\texttt{STM}},T_{\texttt{SMIH}}),\texttt{drt}(T_{\texttt{INIT}},T_{\texttt{PP}},T_{\texttt{LOCK}}))\end{array}$

represents a platform state where:
$\bullet$ $T_{\texttt{PCR}}$ is a term that represents the value of the PCR
register of the TPM;
$\bullet$ $T_{\texttt{INT}}$ is the value of a register of the CPU showing if
interrupts are enabled;
$\bullet$ $T_{\texttt{CACHE}}$ represents the contents of the CPU cache;
$\bullet$ $T_{\texttt{SMIH}}$ represents the program for the SMI handler and
STM represents the STM program, which are located in SMRAM;
$\bullet$ $T_{\texttt{LOCK}}$ is showing if a dynamic root of trust is
running;
$\bullet$ $T_{\texttt{INIT}}$ represents the INIT program;
$\bullet$ $T_{\texttt{PP}}$ represents the protected program PP.

###  4.4 Read and write access

The read access is universal: any agent who has access to a platform state

$\texttt{state}(\texttt{tpm}(T_{\texttt{PCR}}),\texttt{cpu}(T_{\texttt{INT}},T_{\texttt{CACHE}}),\texttt{smram}(T_{\texttt{STM}},T_{\texttt{SMIH}}),\texttt{drt}(T_{\texttt{INIT}},T_{\texttt{PP}},T_{\texttt{LOCK}}))$

can read any of its components relying on the public unary function symbols

$\mathcal{F}_{\texttt{read}}=\\{\texttt{pcr},\texttt{int},\texttt{cache},\texttt{stm},\texttt{smi},\texttt{init},\texttt{pp},\texttt{lock}\\}$

and associated rewrite rules:

$\begin{array}[]{rcl}\texttt{pcr}(\texttt{state}(\texttt{tpm}(y),x_{1},x_{2},x_{3}))&\rightarrow&y\\\
\texttt{int}(\texttt{state}(x_{1},\texttt{cpu}(y_{1},y_{2}),x_{2},x_{3}))&\rightarrow&y_{1}\\\
\texttt{cache}(\texttt{state}(x_{1},\texttt{cpu}(y_{1},y_{2}),x_{2},x_{3}))&\rightarrow&y_{2}\\\
\texttt{init}(\texttt{state}(x_{1},x_{2},\texttt{drt}(y_{1},y_{2},y_{3}),x_{3}))&\rightarrow&y_{1}\\\
\texttt{pp}(\texttt{state}(x_{1},x_{2},\texttt{drt}(y_{1},y_{2},y_{3}),x_{3}))&\rightarrow&y_{2}\\\
\texttt{lock}(\texttt{state}(x_{1},x_{2},\texttt{drt}(y_{1},y_{2},y_{3}),x_{3}))&\rightarrow&y_{3}\\\
\texttt{stm}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{smram}(y_{1},y_{2})))&\rightarrow&y_{1}\\\
\texttt{smi}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{smram}(y_{1},y_{2})))&\rightarrow&y_{2}\end{array}$

The write access to the platform state is restricted by the equational theory
described and illustrated in Fig. 3, where tpm_acc and cpu_acc are private
constants and all other new symbols are public.

Figure 3: Write access to the platform state
$\begin{array}[]{c}\centerline{\hbox{ \leavevmode\resizebox{216.81pt}{}{
\includegraphics{state.pdf} }}}\\\
\begin{array}[]{l}\texttt{reset}(\texttt{state}(\texttt{tpm}(y),x_{1},x_{2},x_{3}),\texttt{tpm\\_acc},\texttt{p}_{\texttt{s}})\rightarrow\texttt{state}(\texttt{tpm}(\texttt{p}_{\texttt{s}}),x_{1},x_{2},x_{3})\\\
\texttt{reset}(\texttt{state}(\texttt{tpm}(y),x_{1},x_{2},x_{3}),\texttt{tpm\\_acc},\texttt{p}_{\texttt{d}})\rightarrow\texttt{state}(\texttt{tpm}(\texttt{p}_{\texttt{d}}),x_{1},x_{2},x_{3})\\\
\texttt{extend}(\texttt{state}(\texttt{tpm}(y),x_{1},x_{2},x_{3}),\texttt{tpm\\_acc},v)\rightarrow\texttt{state}(\texttt{tpm}(\texttt{h}((y,v))),x_{1},x_{2},x_{3})\\\
\texttt{set\\_pcr}(\texttt{state}(\texttt{tpm}(y),x_{1},x_{2},x_{3}),\texttt{tpm\\_acc},v)\rightarrow\texttt{state}(\texttt{tpm}(v),x_{1},x_{2},x_{3})\\\
\texttt{set\\_int}(\texttt{state}(x_{1},\texttt{cpu}(y_{1},y_{2}),x_{2},x_{3}),\texttt{cpu\\_acc},v)\rightarrow\texttt{state}(x_{1},\texttt{cpu}(v,y_{2}),x_{2},x_{3})\\\
\texttt{set\\_int}(\texttt{state}(x_{1},\texttt{cpu}(y,z),x_{2},\texttt{drt}(z_{1},\texttt{prog}(z_{2}),\texttt{true})),z_{2},v)\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},\texttt{cpu}(v,z),x_{2},\texttt{drt}(z_{1},\texttt{prog}(z_{2}),\texttt{true}))\\\
\texttt{cache}(\texttt{state}(x_{1},\texttt{cpu}(y_{1},y_{2}),x_{2},x_{3}),v)\rightarrow\texttt{state}(x_{1},\texttt{cpu}(y_{1},v),x_{2},x_{3})\\\
\texttt{flush}\\_\texttt{stm}(\texttt{state}(x_{1},\texttt{cpu}(y_{1},v),\texttt{smram}(z_{1},z_{2}),\texttt{drt}(w_{1},w_{2},\texttt{false})))\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},\texttt{cpu}(y_{1},v),\texttt{smram}(v,z_{2}),\texttt{drt}(w_{1},w_{2},\texttt{false})))\\\
\texttt{flush}\\_\texttt{smi}(\texttt{state}(x_{1},\texttt{cpu}(y_{1},v),\texttt{smram}(z_{1},z_{2}),x_{2}))\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},\texttt{cpu}(y_{1},v),\texttt{smram}(z_{1},v),x_{2})\\\
\texttt{set\\_init}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},y_{2},y_{3})),\texttt{cpu\\_acc},v)\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(v,y_{2},y_{3}))\\\
\texttt{set\\_pp}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},y_{2},y_{3})),\texttt{cpu\\_acc},v)\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},v,y_{3}))\\\
\texttt{set\\_pp}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(\texttt{prog}(y_{1}),y_{2},y_{3})),y_{1},v)\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(\texttt{prog}(y_{1}),v,y_{3}))\\\
\texttt{set\\_pp}(\texttt{state}(x,\texttt{cpu}(\texttt{true},z),\texttt{smram}(\texttt{prog}(z_{1}),\texttt{prog}(z_{2}))),\texttt{drt}(y_{1},y_{2},y_{3})),(z_{1},z_{2}),v)\\\
\ \ \ \
\rightarrow\texttt{state}(x,\texttt{cpu}(\texttt{true},z),\texttt{smram}(\texttt{prog}(z_{1}),\texttt{prog}(z_{2})),\texttt{drt}(y_{1},v,y_{3}))\\\
\texttt{set\\_lock}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},y_{2},y_{3})),\texttt{cpu\\_acc},v)\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},y_{2},v))\\\
\texttt{set\\_lock}(\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},\texttt{prog}(y_{2}),y_{3})),y_{2},v)\\\
\ \ \ \
\rightarrow\texttt{state}(x_{1},x_{2},x_{3},\texttt{drt}(y_{1},\texttt{prog}(y_{2}),v))\\\
\texttt{set\\_lock}(\texttt{state}(x,\texttt{cpu}(\texttt{true},z),\texttt{smram}(\texttt{prog}(z_{1}),\texttt{prog}(z_{2})),\texttt{drt}(y_{1},y_{2},y_{3})),(z_{1},z_{2}),v)\\\
\ \ \ \
\rightarrow\texttt{state}(x,\texttt{cpu}(\texttt{true},z),\texttt{smram}(\texttt{prog}(z_{1}),\texttt{prog}(z_{2})),\texttt{drt}(y_{1},y_{2},v))\end{array}\end{array}$

PCR.

Only the TPM can reset, extend or set the value of the PCR. This capability of
the TPM is modeled by the _private constant_ tpm_acc, which will be used only
in the TPM process, described later in Fig. 4.

INT.

The interrupts can be enabled or disabled by the CPU, whose capability is
modeled by the _private constant_ cpu_acc. Additionally, if a DRT is running,
then the corresponding protected program PP also has the ability to enable or
disable interrupts. This is modeled in the second set_int equation, by relying
on the fact that, if $\texttt{prog}(x)$ represents the public identity of a
program (as explained in section 4.2), then $x$ represents a private entry
point for that program. Therefore, we can use $x$ to model the ability of
$\texttt{prog}(x)$ to change certain elements of the platform state when it is
loaded.

CACHE.

Any values can be cached. The cache values can then be copied into the
contents of the SMI handler and, when a DRT is not running, into the STM
component of the state.

INIT.

Only the CPU has the ability to load an INIT program on the platform.

PP.

The PP program can be loaded by the CPU (the first equation for set_pp) or by
an INIT program, if the latter is already loaded on the platform (the second
equation for set_pp). Furthermore, the SMI in conjunction with the STM can
also modify the PP program, if the interrupts are enabled (the third equation
for set_pp).

LOCK.

Similarly, the DRT lock can be set/unset by the CPU, by the running PP, or by
the SMI in conjunction with the STM, if the interrupts are enabled.

We denote by $\mathcal{E}_{\texttt{state}}$ the equational theory defined in
this subsection.

###  4.5 Communication channels

The public constant os models a communication channel for platform states and
other messages that may be intercepted, modified or provided by the intruder
as inputs to the CPU or the TPM. A private constant cpu_tpm models the secure
channel between the CPU and the TPM. A private function tpm_ch models the
ability of the CPU to establish a private channel between a loaded program and
the TPM. Generally, these channels will be of the form
$\texttt{tpm\\_ch}(\texttt{prog}(t))$ and the CPU will send this term both to
the program represented by $\texttt{prog}(t)$ (on channel $t$) and to the TPM
(on channel cpu_tpm). We also use message tags that will be clear from the
context.

###  4.6 The trusted platform module

$\begin{array}[]{|ll|}\hline\cr\texttt{TPM}&=\;\;!\texttt{TPM}_{\texttt{RESET}}\;|\;!\texttt{TPM}_{\texttt{EXTEND}}\;|\;!\texttt{TPM}_{\texttt{UNSEAL}}\\\
\texttt{TPM}_{\texttt{RESET}}&=\texttt{let\;}(\mathit{ch},\mathit{rv})\\!=\\!(\texttt{cpu\\_tpm},\texttt{p}_{\texttt{d}})\texttt{\;in\;}!\texttt{PCR}_{\texttt{RESET}}\;|\\\
&\texttt{let\;}(\mathit{ch},\mathit{rv})=(\texttt{os},\texttt{p}_{\texttt{s}})\texttt{\;in\;}!\texttt{PCR}_{\texttt{RESET}}\\\
\texttt{PCR}_{\texttt{RESET}}&=\texttt{in}(\mathit{ch},(\texttt{reset\\_req},\mathit{nonce},\mathit{pf\\_state}));\\\
&\texttt{let\;}\mathit{new\\_st}=\texttt{reset}(\mathit{pf\\_state},\texttt{tpm\\_acc},\mathit{rv})\texttt{\;in\;}\\\
&\texttt{out}(\mathit{ch},(\texttt{reset\\_resp},\mathit{nonce},\mathit{new\\_st}))\\\
\texttt{TPM}_{\texttt{EXTEND}}&=\texttt{let\;}\mathit{ch}=\texttt{cpu\\_tpm}\texttt{\;in\;}!\texttt{PCR}_{\texttt{EXTEND}}\;|\\\
&\texttt{let\;}\mathit{ch}=\texttt{os}\texttt{\;in\;}!\texttt{PCR}_{\texttt{EXTEND}}\;|\\\
&!\;(\texttt{in}(\texttt{cpu\\_tpm},(\texttt{ext\\_channel},\mathit{ch}));!\texttt{PCR}_{\texttt{EXTEND}})\\\
\texttt{PCR}_{\texttt{EXTEND}}&=\texttt{in}(\mathit{ch},(\texttt{extend\\_req},\mathit{nonce},\mathit{pf\\_state},\mathit{v}));\\\
&\texttt{let\;}\mathit{new\\_st}=\texttt{extend}(\mathit{pf\\_state},\texttt{tpm\\_acc},\mathit{v})\texttt{\;in\;}\\\
&\texttt{out}(\mathit{ch},(\texttt{extend\\_resp},\mathit{nonce},\mathit{new\\_st}))\\\
\texttt{TPM}_{\texttt{UNSEAL}}&=\texttt{in}(\texttt{os},\mathit{pf\\_state});\\\
&\texttt{if }\texttt{lock}(\mathit{pf\\_state})=\texttt{true}\texttt{ then
}\\\
&\;\;\;\;\texttt{let\;}\mathit{ch}=\texttt{tpm\\_ch}(\texttt{pp}(\mathit{pf\\_state}))\texttt{\;in\;}\texttt{UNSEAL}\\\
&\texttt{else
}\texttt{let\;}\mathit{ch}=\texttt{os}\texttt{\;in\;}\texttt{UNSEAL}\\\
\texttt{UNSEAL}&=\texttt{in}(\mathit{ch},(\texttt{tag\\_unseal},\mathit{blob}));\\\
&\texttt{let\;}\mathit{v}=\texttt{unseal}(\mathit{blob},\texttt{pcr}(\mathit{pf\\_state}))\texttt{\;in\;}\\\
&\texttt{out}(\mathit{ch},(\texttt{tag\\_plain},\mathit{v})))\\\
\hline\cr\end{array}$ Figure 4: The TPM process

We model the TPM by the process in Fig. 4. A PCR reset request can come either
from the CPU, and then the PCR is reset to the value $\texttt{p}_{\texttt{d}}$
marking a dynamic root of trust, or else from the operating system. A PCR
extend request can come from the CPU, from the operating system or from a
private channel that the CPU can establish between the TPM and some other
process. To unseal a value, the TPM relies on the value of the PCR registers
recorded in the platform state that is associated to an unseal request. The
corresponding equation for unseal ensures that this operation will succeed
only if the PCR values from the state match the PCR values against which plain
data was sealed. If a DRT is running, we perform the unseal for the protected
program PP, on the private channel
$\texttt{tpm\\_ch}(\texttt{pp}(pf\\_state))$; otherwise, the unsealed value is
made public on channel os.

###  4.7 Dynamic root of trust: launch

$\begin{array}[]{|l|}\hline\cr\texttt{CPU}=\;\;\;\;!\;\;\;\;\;\;\text{{(***
The {CPU}\ process ***)}}\\\ \text{{(* Step 1: receive a {DRT}\ request
*)}}\\\
\;\texttt{in}(\texttt{os},(\texttt{drt\\_req},\mathit{init},\mathit{pp},\mathit{pf\\_state}))\\\
\;\texttt{if }\texttt{lock}(\mathit{pf\\_state})=\texttt{false}\texttt{ then
}\\\
\;\texttt{let\;}s_{0}^{\prime}=\texttt{set\\_int}(\mathit{pf\\_state},\texttt{cpu\\_acc},\texttt{false})\texttt{\;in\;}\\\
\;\texttt{let\;}s_{0}=\texttt{set\\_lock}(s_{0}^{\prime},\texttt{cpu\\_acc},\texttt{true})\texttt{\;in\;}\\\
\\\ \text{{(* Step 2: measure {INIT}\ and the {STM}\ *)}}\\\
\;\texttt{let\;}\mathit{measure}=(\texttt{h}(\mathit{init}),\texttt{h}(\texttt{stm}(\mathit{pf\\_state})))\texttt{\;in\;}\\\
\\\ \;\text{{(* Step 3: reset and extend the {PCR}\ *)}}\\\
\;\texttt{new}\,\texttt{nonce};\texttt{out}(\texttt{cpu\\_tpm},(\texttt{reset\\_req},\texttt{nonce},s_{0}));\\\
\;\texttt{in}(\texttt{cpu\\_tpm},(\texttt{reset\\_resp},\texttt{nonce},s_{1}));\\\
\;\texttt{out}(\texttt{cpu\\_tpm},(\texttt{extend\\_req},\texttt{nonce},s_{1},\mathit{measure}));\\\
\;\texttt{in}(\texttt{cpu\\_tpm},(\texttt{extend\\_resp},\texttt{nonce},s_{2}));\\\
\text{{(*Step 4a: load {INIT}\ \& grant {TPM}\ access*)}}\\\
\;\texttt{let\;}s_{3}=\texttt{set\\_init}(s_{2},\texttt{cpu\\_acc},\mathit{init})\texttt{\;in\;}\\\
\;\texttt{let\;}\mathit{einit}=\texttt{get\\_entry}(\mathit{init})\texttt{\;in\;}\\\
\;\texttt{out}(\mathit{einit},(\texttt{nonce},s_{3},\texttt{tpm\\_ch}(\mathit{init}),\mathit{pp}));\\\
\;\texttt{out}(\texttt{cpu\\_tpm},(\texttt{ext\\_channel},\texttt{tpm\\_ch}(\mathit{init}))));\\\
\text{{(* Step 7b: establish {TPM}\ access for {PP}\ *)}}\\\
\;\texttt{in}(\mathit{einit},(\texttt{drt\\_resp},\texttt{nonce},\mathit{new\\_state}));\\\
\;\texttt{let\;}\mathit{epp}=\texttt{get\\_entry}(\texttt{pp}(\mathit{new\\_state}))\texttt{\;in\;}\\\
\;\texttt{out}(\mathit{epp},(\mathit{new\\_state},\texttt{tpm\\_ch}(\texttt{prog}(\mathit{epp}))));\\\
\;\texttt{out}(\texttt{cpu\\_tpm},(\texttt{ext\\_channel},\texttt{tpm\\_ch}(\texttt{prog}(\mathit{epp}))))\\\
\\\ \texttt{INIT}=\;\;\;\text{{(*** A trusted {INIT}\ program ***)}}\\\
\;\texttt{out}(\texttt{os},\texttt{prog}(\texttt{Tinit}));\texttt{out}(\texttt{os},\texttt{prog}(\texttt{Tstm}));\\\
\text{{(* Step 4b: receive {PP}\ and {TPM}\ channel *)}}\\\
\;\texttt{in}(\texttt{Tinit},(\texttt{nonce},\mathit{pf\\_st},\mathit{tpmc},\mathit{pp}));\\\
\;\text{{(* Steps 5-6: extend $h(\texttt{PP})$ into {PCR}\ *)}}\\\
\;\texttt{let\;}\mathit{measure}=\texttt{h}(\mathit{pp})\texttt{\;in\;}\texttt{new}\,\texttt{nonce}_{1};\\\
\;\texttt{out}(\mathit{tpmc},(\texttt{extend\\_req},\texttt{nonce}_{1},\mathit{pf\\_st},\mathit{measure}));\\\
\;\texttt{in}(\mathit{tpmc},(\texttt{extend\\_resp},\texttt{nonce}_{1},\mathit{ext\\_st}));\\\
\text{{(* Step 7a: load {PP}\ on platform state *)}}\\\
\;\texttt{let\;}\mathit{new\\_st}=\texttt{set\\_pp}(\mathit{ext\\_st},\texttt{Tinit},\mathit{pp})\texttt{\;in\;}\\\
\;\texttt{out}(\texttt{exp\\_init},(\texttt{drt\\_resp},\texttt{nonce},\mathit{new\\_st})));\\\
\;\texttt{out}(\texttt{os},\mathit{new\\_st})\\\ \hline\cr\end{array}$ Figure
5: DRT process for CPU and INIT

The procedure for launching a dynamic root of trust, i.e. steps 1-7 from Fig.
1, is modeled by the processes CPU and INIT, from Fig. 5. The CPU receives a
request including the INIT and PP programs and the platform state where the
DRT is to be launched. If a DRT is not already running in the corresponding
platform state, then the CPU disables the interrupts and sets the DRT lock
(step 1). Next, the CPU measures the INIT and STM programs and extends the
result into the PCR (steps 2-3). In step 4a, the INIT program is loaded and we
use the term $\texttt{tpm\\_ch}(\texttt{init})$ to model an established
private channel between the TPM and the running INIT program. We use the
program abstraction introduced in section 4.2 to model the loading and the
execution of INIT, relying on the private constant Tinit. In turn, the loaded
INIT program measures the PP program, records the measurement into the TPM,
and loads PP on the platform state (steps 4b-7a). After the INIT program has
measured the PP program and loaded it into memory, the CPU gets back the new
platform state and sets up the private channel for communication between the
loaded PP and the TPM (step 7b).

###  4.8 Dynamic root of trust: execution

$\begin{array}[]{|l|}\hline\cr\texttt{PP}=\textbf{(* Example of protected
program *)}\\\ \text{{(* Step 7c: launch and get {TPM}\ access *)}}\\\
\texttt{out}(\texttt{os},\texttt{prog}(\texttt{Tpp})));\\\
\texttt{in}(\texttt{Tpp},(\mathit{pf\\_state_{0}},\mathit{tpmc}));\\\
\text{{(* Re-enable interrupts *)}}\\\
\texttt{let\;}\mathit{pf\\_st}=\texttt{set\\_int}(\mathit{pf\\_state_{0}},\texttt{Tpp},\texttt{true})\\\
\texttt{\;in\;}\texttt{out}(\texttt{os},\mathit{pf\\_st});\\\ \\\ \text{{(*
Step 8: unseal and decrypt *)}}\\\
\texttt{in}(\texttt{os},x_{\texttt{seal}});\texttt{in}(\texttt{os},x_{\texttt{enc}});\\\
\texttt{out}(\mathit{tpmc},(\texttt{tag\\_unseal},x_{\texttt{seal}}));\\\
\texttt{in}(\mathit{tpmc},(\texttt{tag\\_plain},x_{k}));\\\
\texttt{let\;}\mathit{mess}=\texttt{sdec}(x_{\texttt{enc}},x_{k})\texttt{\;in\;}\texttt{out}(\texttt{os},\mathit{mess});\\\
\\\ \text{{(* Step 9: Ending the execution *)}}\\\
\texttt{new}\,\texttt{rand};\texttt{out}(\mathit{tpmc},(\texttt{extend\\_req},\texttt{rand},\mathit{pf\\_st},\bot));\\\
\texttt{in}(\mathit{tpmc},(\texttt{extend\\_resp},\texttt{rand},\mathit{exts}));\\\
\texttt{let\;}\mathit{ends}=\texttt{set\\_lock}(\mathit{exts},\texttt{Tpp},\texttt{false})\texttt{\;in\;}\\\
\texttt{out}(\texttt{os},\mathit{ends})\\\ \hline\cr\end{array}$
Figure 6: DRT execution

We illustrate the execution of a trusted PP program with an example in Fig. 6,
where step 8 is an example of some useful execution of PP, i.e., unsealing and
decrypting, whereas the rest is behaviour we expect from any protected
program. The private constant Tpp represents the private entry point of PP
according to the model from section 4.2.

In Fig. 7 we consider a fresh symmetric key $k_{\texttt{pp}}$ and assume that
this key has been sealed against the measurement of the trusted PP program,
with identity $\texttt{prog}(\texttt{Tinit})$, of the trusted INIT program,
with identity $\texttt{prog}(\texttt{Tinit})$, and of the trusted STM program,
with identity $\texttt{prog}(\texttt{Tstm})$. This is represented by the term
sealed_key in the process DATA (see the code in the figure below), which we
publish on the channel os. We also assume that some private message
$\texttt{hi}_{\texttt{pp}}$ is encrypted with $k_{\texttt{pp}}$ and
$\texttt{senc}(\texttt{hi}_{\texttt{pp}},k_{\texttt{pp}})$ is made publicly
available on channel os.

In the context of a DRT, the program PP should be able to unseal the key
$k_{\texttt{pp}}$, decrypt and publish $\texttt{hi}_{\texttt{pp}}$. Before the
execution of PP ends, the DRT lock is set to false, and also the PCR is
extended with a dummy value in order to leave the PCR in a state which is not
to be trusted any more. We verify, in section 4.9, that secret DATA sealed for
this program remains secret.

$\begin{array}[]{|l|}\hline\cr\texttt{DATA}=\;\;\textbf{(* Seal and encrypt
private data *)}\\\
\texttt{new}\,k_{\texttt{pp}};\texttt{new}\,\texttt{hi}_{\texttt{pp}};\texttt{out}(\texttt{os},\texttt{senc}(\texttt{hi}_{\texttt{pp}},k_{\texttt{pp}}));\\\
\texttt{let
}\texttt{sealed\\_key}=\texttt{seal}(k_{\texttt{pp}},\texttt{hchain})\;\texttt{in}\;\texttt{out}(\texttt{os},\texttt{sealed\\_key});\\\
\textbf{(* where
}\texttt{hchain}=\texttt{h}(\texttt{h}(\texttt{p}_{\texttt{d}},(\texttt{h}(\texttt{prog}(\texttt{Tinit})),\texttt{h}(\texttt{prog}(\texttt{Tstm})))),\texttt{h}(\texttt{prog}(\texttt{Tpp})))\textbf{
*)}\\\ \\\ \texttt{SETUP}=\;\;\textbf{(* Launching the system *)}\\\ \text{{(*
Load the initial state *)}}\\\
\texttt{in}(\texttt{os},x_{\texttt{stm}});\texttt{in}(\texttt{os},x_{\texttt{smi}});\\\
\texttt{out}(\texttt{os},\texttt{state}(\texttt{tpm}(\texttt{p}_{\texttt{s}}),\texttt{cpu}(\texttt{true},\bot),\texttt{smram}(x_{\texttt{stm}},x_{\texttt{smi}}),\texttt{drt}(\bot,\bot,\texttt{false}));\\\
\text{{(* Run a {DRT}\ with any loaded programs *)}}\\\
\texttt{in}(\texttt{os},\texttt{init});\texttt{in}(\texttt{os},\texttt{pp});\texttt{in}(\texttt{os},\texttt{pf\\_state});\texttt{out}(\texttt{os},(\texttt{drt\\_req},\texttt{init},\texttt{pp},\texttt{pf\\_state}));\\\
\hline\cr\text{{(* The main processes put together *)}}\\\
\texttt{EXEC}=\;\;(\;\texttt{CPU}\;|\;!\;\texttt{INIT}\;|\;\texttt{SETUP}\;|\;\texttt{DATA}\;|\;!\;\texttt{PP}\;)\;\;\;\;\;\;\;\;\;\;\;\;\texttt{DRT}=\;\;(\;\texttt{TPM}\;|\;\texttt{EXEC}\;)\\\
\hline\cr\end{array}$
Figure 7: DRT setup and full process.

The SETUP process ties everything together, i.e., it loads and publishes an
initial state, and runs any DRT request from the operating system. We call
EXEC, all the processes put together, whereas the TPM is the one providing the
trusted functionalities of reset, extend, and unseal. We use
$\texttt{DRT}=(\texttt{TPM}\;|\;\texttt{EXEC})$.

###  4.9 Security properties in the formal model

Reachability. The reachability of a state in the platform can be expressed as
a (non-)secrecy property: a state is reachable when a corresponding state term
can be obtained by the attacker after interacting with the process DRT modulo
the theory
$\mathcal{E}_{\texttt{drt}}=\mathcal{E}_{\texttt{data}}\cup\mathcal{E}_{\texttt{prog}}\cup\mathcal{E}_{\texttt{state}}$,
expressed as a formula of the form

$\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}}\texttt{Att}(\texttt{state}(T_{\texttt{tpm}},T_{\texttt{cpu}},T_{\texttt{smram}},T_{\texttt{drt}})).$

The property that the $\texttt{DRT}=(\texttt{TPM}\;|\;\texttt{EXEC})$ process
can reach an expected state where some trusted programs INIT and PP have been
correctly measured and loaded on the platform can be expressed as follows:

$\begin{array}[]{lcl}\begin{array}[]{rll}\texttt{DRT}&\models_{\mathcal{E}_{\texttt{drt}}}&\texttt{Att}(\texttt{state}(\\\
&&\texttt{tpm}(\texttt{h}((\texttt{h}((\texttt{p}_{\texttt{d}},v_{1})),v_{2}))),\texttt{cpu}(\texttt{true},x),\\\
&&\texttt{smram}(\texttt{prog}(\texttt{Tstm}),\texttt{prog}(y))\\\
&&\texttt{drt}(\texttt{prog}(\texttt{Tinit}),\texttt{prog}(\texttt{Tpp}),\texttt{true})))\end{array}\par&&\begin{array}[]{rcl}where\\\
v_{1}&=&(\texttt{h}(\texttt{prog}(\texttt{Tinit})),\\\
&&\;\;\texttt{h}(\texttt{prog}(\texttt{Tstm}))\\\
v_{2}&=&\texttt{h}(\texttt{prog}(\texttt{Tpp})).\end{array}\end{array}$

An additional reachability property of interest is whether the program PP has
succeeded to unseal the key $k_{\texttt{pp}}$, decrypt the private message
$\texttt{hi}_{\texttt{pp}}$ and output it on the public channel os. This is
captured by the following (non-)secrecy formula:

$\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}}\texttt{Att}(\texttt{hi}_{\texttt{pp}}).$

Code integrity. We say that the trusted platform ensures code integrity if the
measurement contained in the PCR value correctly reflects the state of the
platform. Specifically, we require that whenever a dynamic root of trust is
active with a PCR value of $\texttt{p}_{\texttt{d}}$ extended with the
expected measurements $v_{1}$ and $v_{2}$, then only the corresponding PP,
INIT and STM are running on the platform, and they cannot be modified. This
can be expressed by the following correspondence assertion, which we will
_denote by $\Phi_{\texttt{int}}$_ in the rest of the paper:

$\begin{array}[]{rll}\texttt{DRT}&\models_{\mathcal{E}_{\texttt{drt}}}&\texttt{Att}(\texttt{state}(\texttt{tpm}(\texttt{h}((\texttt{h}((\texttt{p}_{\texttt{d}},v_{1})),v_{2}))),\texttt{cpu}(x,y),\texttt{smram}(x_{\texttt{stm}},x_{\texttt{smi}}),\\\
&&\;\;\;\;\;\;\texttt{drt}(x_{\texttt{init}},x_{\texttt{pp}},\texttt{true})))\;\;\implies\;\;(x_{\texttt{init}},x_{\texttt{pp}},x_{\texttt{stm}})=(p_{1},p_{2},p_{3})\end{array}$

where $p_{1}=\texttt{prog}(\texttt{Tinit})$,
$p_{2}=\texttt{prog}(\texttt{Tpp})$, $p_{3}=\texttt{prog}(\texttt{Tstm})$.

Note that we ensure the property only for trusted programs. Indeed, if any of
PP, INIT or STM are malicious, they could use their privileges to reach a
platform state that does not reflect the PCR values. This is fine, because the
PCR values will correctly record the identity of running programs in the chain
of trust. In particular, our property shows that untrusted DRT programs cannot
make the PCR values record the measurement of trusted programs.

Secrecy of sealed data. We also verify that data sealed for PP, i.e. the key
$k_{\texttt{pp}}$, remains secret (we _denote this formula by
$\Phi_{\texttt{sec}}$_):

$(\Phi_{\texttt{sec}})\;\;\;\;\;\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}}\texttt{Att}(k_{\texttt{pp}})\implies\mathit{false}.$

##  5 Process transformation for automated verification

ProVerif does not terminate for the DRT process and the equational theory
$\mathcal{E}_{\texttt{drt}}$. The main reason is the rewrite rule from
$\mathcal{E}_{state}$ that allows an unbounded number of PCR extensions,
reflecting a problem first noticed in [12]. In this section, we propose a
general transformation of processes that allows a more efficient exploration
of the search space by ProVerif. The transformation is based on a general
observation formalised in Proposition 5.1: we can replace a process $P$ with a
process $Q$ as input for ProVerif, as long as $Q$ and $P$ are equivalent with
respect to the security properties of interest. Concretely, we will replace
the process DRT with a process $\texttt{DRT}^{b}$ that bounds the number of
PCR extensions, while allowing a direct way for the attacker to set the PCR to
any value that is bigger than the considered bound.

For a process $P$, let $\texttt{Att}(P)=\\{T\;|\;P\models\texttt{Att}(T)\\}$
be the set of terms that can be obtained by the attacker when interacting with
$P$. For a set of terms $\mathcal{M}$, we let
$\texttt{Att}(\mathcal{M})=\\{T\;|\;\mathcal{M}\vdash T\\}$. We notice the
following.

###### Proposition 5.1

Let $P,Q$ be processes and $\texttt{Att}(T)\implies\Phi$ be a correspondence
assertion such that, for any substitution $\sigma$,

$T\sigma\in\texttt{Att}(P)\smallsetminus\texttt{Att}(Q)\implies\Phi\sigma\;\;\text{\
\ and\ \
}\;\;T\sigma\in\texttt{Att}(Q)\smallsetminus\texttt{Att}(P)\implies\Phi\sigma.$

Then we have: $P\models\texttt{Att}(T)\implies\Phi\text{\;\;if and only
if\;\;}Q\models\texttt{Att}(T)\implies\Phi$.

The proof of Proposition 5.1 follows immediately from definitions, yet this
result is crucial to make our models amenable for ProVerif. We are thus
allowed to transform the process DRT into a process $\texttt{DRT}^{b}$, that
is equivalent to DRT with respect to code integrity and secrecy properties
$\Phi_{\texttt{int}}$ and $\Phi_{\texttt{sec}}$, and whose search space can be
handled by ProVerif. It will be easier to express $\texttt{DRT}^{b}$ using
some additional rewrite rules. In conjunction with Proposition 5.1, we will
then rely on the following result for soundness and completeness:

###### Proposition 5.2

Let $\mathcal{P}$ be a process, $\mathcal{E}$ be an equational theory and
$\texttt{Att}(T)\implies\Phi$ be a correspondence assertion. Assume
$\mathcal{E}^{b}$ is a set of rewrite rules such that $\forall U\rightarrow
V\in\mathcal{E}^{b}:\texttt{top}(U)\in\mathcal{F}_{\texttt{priv}}$, i.e., is a
private symbol. Then we have:

$P\models_{\mathcal{E}}\texttt{Att}(T)\implies\Phi\text{\;\;if and only
if\;\;}P\models_{\mathcal{E}\cup\mathcal{E}^{b}}\texttt{Att}(T)\implies\Phi.$

_Notation._ We denoted a term of the form $h((\ldots
h((T_{0},T_{1}))),\ldots,T_{n}))$ by $\texttt{chain}(T_{0},\ldots,T_{n})$,
using $\texttt{chain}(T_{0})$ for $T_{0}$. We define
$\texttt{length}(\texttt{chain}(T_{0},\ldots,T_{n}))=n$, representing the
number of extensions of a PCR.

_Problematic rewrite rule._ We recall the rewrite rule that poses non-
termination problems for ProVerif:

$\texttt{extend}(\texttt{state}(\texttt{tpm}(y),x_{1},x_{2},x_{3}),\texttt{tpm\\_acc},v)\rightarrow\texttt{state}(\texttt{tpm}(\texttt{h}((y,v))),x_{1},x_{2},x_{3})\\\
$

Intuitively, ProVerif does not terminate because it is unable to make an
abstract reasoning about the introduction of the term $\texttt{h}((y,v))$ in
the right hand side of this rewrite rule. We propose a transformation of the
TPM process into a process $\texttt{TPM}^{b}$ that allows more values to be
written into the PCR, overapproximating the effect of the problematic rewrite
rule. This transformation will be sound and complete (satisfying the
conditions of Proposition 5.1) based on the observation that, once it exceeds
a certain bound, the value of the PCR does not matter for
$\Phi_{\texttt{sec}}$ and $\Phi_{\texttt{int}}$ – thus, we can let the
attacker have complete control over it.

_Proposed transformation._ For a given natural number $b$, we would like the
following behaviour of the $\texttt{TPM}^{b}$ process: if an extend request is
received for a platform state
$\texttt{state}(\texttt{tpm}(T_{1}),T_{2},T_{3},T_{4})$ and a value $V$:

$\bullet$ if the length of the PCR is smaller than $b$, i.e.
$\texttt{length}(T_{1})<b$, then execute this request normally, using the
function extend. The updated platform state returned by the $\texttt{TPM}^{b}$
should now be $\texttt{state}(\texttt{tpm}(h((T_{1},V))),T_{2},T_{3},T_{4})$.

$\bullet$ if the length of the PCR value $T_{1}$ is greater or equal to $b$,
i.e. $\texttt{length}(T_{1})\geq b$, then output $T_{1}$ and $V$ to the
attacker and wait for a new value $T_{1}^{\prime}$ as a response. If the
length of $T_{1}^{\prime}$ is big enough, i.e.
$\texttt{length}(T_{1}^{\prime})>b$, the updated platform state returned by
the $\texttt{TPM}^{b}$ should now be
$\texttt{state}(\texttt{tpm}(T_{1}^{\prime}),T_{2},T_{3},T_{4})$. In a normal
execution, we would have $T_{1}^{\prime}=h((T_{1},V))$. However, the attacker
has the choice to set $T_{1}^{\prime}$ to any value.

Formally, the $\texttt{TPM}^{b}$ process relies on the private function
is_small to detect if the value of the PCR is lower or higher than the bound,
and treat the two cases differently. The following set of rewrite rules, for
all $0\leq i<b$, define is_small:
$\texttt{is\\_small}(\texttt{chain}(v_{0},\ldots,v_{i}))\rightarrow\texttt{true}$,
where $v_{0}\in\\{\texttt{p}_{\texttt{s}},\texttt{p}_{\texttt{d}}\\}$ and
$v_{1},\ldots,v_{i}$ are mutually distinct variables. We also need to check if
some value to be extended into the PCR is big enough. For this, we introduce
the private function is_big, together with the rewrite rule:
$\texttt{is\\_big}(\texttt{chain}(v_{0},\ldots,v_{b+1}))\rightarrow\texttt{true}$,
where $v_{0},\ldots,v_{b+1}$ are mutually distinct variables.

$\begin{array}[]{|lcl|}\hline\cr\texttt{DRT}^{b}&=&\texttt{TPM}^{b}\;|\;\texttt{EXEC}\\\
\texttt{TPM}^{b}&=&\texttt{TPM}\;\\{\;\texttt{PCR}_{\texttt{EXTEND}}\mapsto\texttt{PCR}_{\texttt{EXTEND}}^{b}\;\\}\\\
\texttt{PCR}_{\texttt{EXTEND}}^{b}&=&\texttt{in}(\texttt{ch},(=\texttt{extend\\_req},nonce,pf\\_state,val));\\\
&&\texttt{let\;}pcr=\texttt{pcr}(pf\\_state)\texttt{\;in\;}\\\ &&\texttt{if
}\texttt{is\\_small}(pcr)=\texttt{true}\texttt{ then
}\;\;\texttt{PCR}_{\texttt{EXTEND}}^{\texttt{SMALL}}\;\;\texttt{else}\;\;\texttt{PCR}_{\texttt{EXTEND}}^{\texttt{BIG}}\\\
\texttt{PCR}_{\texttt{EXTEND}}^{\texttt{SMALL}}&=&\texttt{let\;}new\\_st=\texttt{extend}(pf\\_state,\texttt{tpm\\_acc},val)\texttt{\;in\;}\\\
&&\texttt{out}(\texttt{ch},(extend\\_resp,nonce,new\\_st))\\\
\texttt{PCR}_{\texttt{EXTEND}}^{\texttt{BIG}}&=&\texttt{out}(\texttt{os},(pcr,val));\texttt{in}(\texttt{os},new\\_pcr)\\\
&&\texttt{if }\texttt{is\\_big}(new\\_pcr)=\texttt{true}\texttt{ then }\\\
&&\texttt{let\;}new\\_st=\texttt{set\\_pcr}(pf\\_state,\texttt{tpm\\_acc},new\\_pcr)\texttt{\;in\;}\\\
&&\texttt{out}(\texttt{ch},(extend\\_resp,\texttt{nonce},new\\_st))\\\
\hline\cr\end{array}$

The only difference from the normal TPM process is in
$\texttt{PCR}_{\texttt{EXTEND}}^{b}$, which first detects if the current value
of the PCR is small or big: if it is small, the extension process proceeds
normally (the process $\texttt{TPM}_{\texttt{EXTEND}}^{\texttt{SMALL}}$); if
it is bigger than the given bound, then the TPM requests that the operating
system combines pcr and val itself (the process
$\texttt{TPM}_{\texttt{EXTEND}}^{\texttt{BIG}}$). Upon receiving the response
from the os, the TPM first checks that the value provided is indeed big (the
compromised operating system may be cheating). Only then, it updates the PCR
to the requested value.

We denote by $\mathcal{E}_{\texttt{drt}}^{b}$ the equational theory
$\mathcal{E}_{\texttt{drt}}$ augmented with the rules for is_small,is_big and
set_pcr introduced in this section and we assume that these new symbols are
private (they are used only by $\texttt{TPM}^{b}$).

###  5.1 Sketch of correctness proofs

We have to show that, for
$\Phi\in\\{\Phi_{\texttt{sec}},\Phi_{\texttt{int}}\\}$, we have
$\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}}\Phi\Leftrightarrow\texttt{DRT}^{b}\models_{\mathcal{E}^{b}_{\texttt{drt}}}\Phi$.
We note that soundness (direction $\Leftarrow$) is the property that is
necessary to derive the security guarantees for DRT, while completeness is
secondary: it explains why we dont get false attacks against
$\texttt{DRT}^{b}$ with ProVerif. Since
$\texttt{Att}(\texttt{DRT})\subseteq\texttt{Att}(\texttt{DRT}^{b})$, soundness
is easy to prove, while completeness requires careful analysis of terms in
$\texttt{Att}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}(\texttt{DRT})$. We
show that such terms are roughly limited to what we explicitly release in
$\texttt{DRT}^{b}$: state terms with big PCR values; they cannot be used by
the attacker to violate $\Phi_{\texttt{sec}}$ and $\Phi_{\texttt{int}}$.

First, from Proposition 5.2 and the definition of
$\mathcal{E}_{\texttt{drt}}^{b}$, we can easily translate between
$\mathcal{E}_{\texttt{drt}}$ and $\mathcal{E}_{\texttt{drt}}^{b}$, thus the
notions and results that follow are modulo $\mathcal{E}_{\texttt{drt}}^{b}$.

###### Corollary 5.3

For any $\Phi$, we have
$\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}}\Phi\Leftrightarrow\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}^{b}}\Phi$.

Terms $T$ with $\texttt{top}(T)\\!=\\!\texttt{state}$ are called state terms
(or states). For a state term
$T\\!=\\!\texttt{state}(\texttt{tpm}(T_{1}),\texttt{cpu}(T_{2},T_{3}),\texttt{smram}(T_{3},T_{4}),\texttt{drt}(T_{5},T_{6},T_{7}))$,
we let $\texttt{Comp}(T)\\!=\\!\\{T_{1},\dots,T_{7}\\}$. For a set of terms
$\mathcal{M}_{1}$, we say that a set of state terms $\mathcal{M}_{2}$ is
$\mathcal{M}_{1}$-saturated if for any $T\in\mathcal{M}_{2}$ we have $\forall
U\in\texttt{Comp}(T):\mathcal{M}_{1}\vdash U$.

###### Lemma 5.4

Let $\mathcal{M}_{1}$ be a set of terms and $\mathcal{M}_{2}$ be an
$\mathcal{M}_{1}$-saturated set of state terms. Then we have
$\texttt{Att}(\mathcal{M}_{1}\cup\mathcal{M}_{2})=\texttt{Att}(\mathcal{M}_{1})\cup\mathcal{M}_{2}$.

Lemma 5.4 formalizes the intuition that, without access to TPM or CPU, the
only operation that an attacker can perform on a state is to extract its
components. The proof follows by a straightforward inspection of rewrite
rules. To help in the sequel, we consider several restrictions of attacker’s
power against $\texttt{DRT}^{b}$:
$\bullet$ $\texttt{Att}_{0}(\texttt{DRT}^{b})$ is the set of terms that can be
obtained by an attacker interacting with $\texttt{DRT}^{b}$, while not being
allowed to use terms in
$\texttt{Att}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}(\texttt{DRT})$ when
constructing inputs for $\texttt{DRT}^{b}$. That is,
$\texttt{Att}_{0}(\texttt{DRT}^{b})$ can be seen as a passive attacker with
respect to the additional functionality in $\texttt{DRT}^{b}$.
$\bullet$ $\texttt{Att}_{1}(\texttt{DRT}^{b})$ is the knowledge of the
previous attacker whose power is augmented with the ability to unseal terms
from $\texttt{Att}_{0}(\texttt{DRT}^{b})$, with
$\texttt{TPM}\\_\texttt{UNSEAL}$, relying on state terms from
$\texttt{Att}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}(\texttt{DRT})$. This
attacker is not allowed to use terms from
$\texttt{Att}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}(\texttt{DRT})$ in
any other way.
$\bullet$ $\texttt{Att}_{2}(\texttt{DRT}^{b})$ is the knowledge of a _state
respecting_ attacker against $\texttt{DRT}^{b}$: the attacker is given
unrestricted access to $\texttt{DRT}^{b}$ and can use any terms from
$\texttt{Att}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}(\texttt{DRT})$ to
construct his inputs; however, the attacker can only use state terms according
to the specification of an honest behaviour while interacting with the TPM,
the CPU, or the equational theory.

Note that
$\texttt{Att}_{0}(\texttt{DRT}^{b})\subseteq\texttt{Att}_{1}(\texttt{DRT}^{b})\subseteq\texttt{Att}_{2}(\texttt{DRT}^{b})\subseteq\texttt{Att}(\texttt{DRT}^{b})$.
We denote by $\mathcal{M}^{b}$ the set of state terms returned to the attacker
by the $\texttt{PCR}_{\texttt{EXTEND}}^{\texttt{BIG}}$ process. Note that
$\mathcal{M}^{b}$ is an $\texttt{Att}(\texttt{DRT})$-saturated set of state
terms with $\forall T\in\mathcal{M}^{b}:\texttt{length}(\texttt{pcr}(T))>b$.

###### Lemma 5.5

For any $b$, we have
$\texttt{Att}(\texttt{DRT})\subseteq\texttt{Att}_{0}(\texttt{DRT}^{b})\subseteq\texttt{Att}(\texttt{DRT})\cup\mathcal{M}^{b}$.

The first inclusion follows easily from the definition of $\texttt{DRT}^{b}$,
which is able to simulate any normal PCR extension performed by DRT, without
access to any terms in
$\texttt{Att}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}(\texttt{DRT})$. For
the second inclusion, relying on the fact that $\mathcal{M}^{b}$ is
$\texttt{Att}(\texttt{DRT})$-saturated, we use Lemma 5.4 to deduce
$\texttt{Att}_{0}(\texttt{DRT}^{b})\subseteq\texttt{Att}(\texttt{Att}(\texttt{DRT})\cup\mathcal{M}^{b})\subseteq\texttt{Att}(\texttt{DRT})\cup\mathcal{M}^{b}$.

###### Lemma 5.6

For $b\geq 2$, we have
$\texttt{Att}_{1}(\texttt{DRT}^{b})\subseteq\texttt{Att}_{0}(\texttt{DRT}^{b})$.

By definition,
$\texttt{Att}_{1}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}_{0}(\texttt{DRT}^{b})\subseteq\\{U\;|\;\texttt{seal}(U,V)\in\texttt{Att}_{0}(\texttt{DRT}^{b})\\}$.
Note that the only sealed term in $\texttt{Att}_{0}(\texttt{DRT}^{b})$ that
does not originate from the attacker is
$\texttt{seal}(k_{\texttt{pp}},\texttt{hchain})$, with
$\texttt{length}(\texttt{hchain})=2$. For any other term
$\texttt{seal}(U,V)\in\texttt{Att}_{0}(\texttt{DRT}^{b})$, we have
$U\in\texttt{Att}_{0}(\texttt{DRT}^{b})$, and therefore
$U\notin\texttt{Att}_{1}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}_{0}(\texttt{DRT}^{b})$.
From lemma 5.5, the definition of $\texttt{TPM}_{\texttt{UNSEAL}}$, and the
fact that $\forall T\in\mathcal{M}^{b}:\texttt{length}(\texttt{pcr}(T))>b$, we
also deduce that
$k_{\texttt{pp}}\notin\texttt{Att}_{1}(\texttt{DRT}^{b})\smallsetminus\texttt{Att}_{0}(\texttt{DRT}^{b})$,
so we can conclude
$\texttt{Att}_{1}(\texttt{DRT}^{b})\subseteq\texttt{Att}_{0}(\texttt{DRT}^{b})$.

###### Lemma 5.7

For $b\geq 2$, we have
$\texttt{Att}_{2}(\texttt{DRT}^{b})\subseteq\texttt{Att}_{1}(\texttt{DRT}^{b})\cup\mathcal{M}^{b}$.

New terms $U\in\texttt{Att}_{2}(\texttt{DRT}^{b})$ come from using a state
term $V\in\texttt{Att}_{1}(\texttt{DRT}^{b})$ in
$\texttt{TPM}_{\texttt{RESET}}$,$\texttt{TPM}_{\texttt{EXTEND}}$ or CPU. From
lemmas 5.5 and 5.6, we have either $V\in\texttt{Att}(\texttt{DRT})$ or
$V\in\mathcal{M}^{b}$. In both cases, we can show that
$U\in\texttt{Att}_{1}(\texttt{DRT}^{b})\cup\mathcal{M}^{b}$.

###### Corollary 5.8

For $b\geq 2$, we have
$\texttt{Att}(\texttt{DRT})\subseteq\texttt{Att}(\texttt{DRT}^{b})\subseteq\texttt{Att}(\texttt{DRT})\cup\mathcal{M}^{b}\cup\mathcal{M}^{f}$,
where $\mathcal{M}^{f}$ is a set of terms such that any term
$T\in\mathcal{M}^{f}$ contains a state term $T^{\prime}$ with
$\texttt{pcr}(T^{\prime})>b$.

The set $\mathcal{M}^{f}$ represents the additional terms that a non state
respecting attacker can derive from $\mathcal{M}^{b}$. The property of
$\mathcal{M}^{f}$ is due to the fact that $\mathcal{E}_{\texttt{drt}}^{b}$ and
the $\texttt{DRT}^{b}$ process do not have effect on state terms that are used
outside their intended scope. Such terms will end up as harmless subterms of
attacker’s knowledge.

###### Corollary 5.9

For $b\geq 2$, DRT and $\texttt{DRT}^{b}$ satisfy the conditions of
Proposition 5.1 with respect to both $\Phi_{\texttt{sec}}$ and
$\Phi_{\texttt{int}}$.

Corollary 5.8 shows that it is sufficient to check that conditions of
Proposition 5.1 are satisfied for terms $T$ in
$\mathcal{M}^{b}\cup\mathcal{M}^{f}$. For $\Phi_{\texttt{sec}}$, this follows
from the fact that such terms $T$ are either state terms, or contain state
terms, and therefore the key $k_{\texttt{pp}}$ cannot be among them. For
$\Phi_{\texttt{int}}$, this follows from the fact that those state terms have
PCR lengths bigger than $2$, while the precondition of $\Phi_{\texttt{int}}$
is a state term with PCR length 2. From Corollary 5.9 and Proposition 5.1, we
deduce:

###### Corollary 5.10

For $\Phi\in\\{\Phi_{\texttt{sec}},\Phi_{\texttt{int}}\\}$, we have
$\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}^{b}}\Phi\Leftrightarrow\texttt{DRT}^{b}\models_{\mathcal{E}_{\texttt{drt}}^{b}}\Phi$.

From Corollaries 5.3 and 5.10, we conclude:

###### Theorem 5.11

For $\Phi\in\\{\Phi_{\texttt{sec}},\Phi_{\texttt{int}}\\}$,
$\texttt{DRT}\models_{\mathcal{E}_{\texttt{drt}}}\Phi\Leftrightarrow\texttt{DRT}^{b}\models_{\mathcal{E}_{\texttt{drt}}^{b}}\Phi$.

##  6 Verification

The ProVerif code for the $\texttt{DRT}^{b}$ process and the security
properties defined in sections 4 and 5 is available
online222www.dropbox.com/s/cvq4op3w106868t/drt.pi (using ProVerif version
1.85).. It uses the equational theory
$\mathcal{E}_{\texttt{data}}\cup\mathcal{E}_{\texttt{prog}}\cup\mathcal{E}_{\texttt{state}}^{b}$,
with $b=2$. The verification of each security property terminates in order of
minutes, returning the expected result. From these results (implying there is
no attack on $\texttt{DRT}^{b}$ modulo $\mathcal{E}_{\texttt{drt}}^{b}$) and
from Theorem 5.11 (implying there is no attack on DRT modulo
$\mathcal{E}_{\texttt{drt}}$), we derive:

###### Theorem 6.1

The DRT process satisfies, modulo
$\mathcal{E}_{\texttt{data}}\cup\mathcal{E}_{\texttt{prog}}\cup\mathcal{E}_{\texttt{state}}$,
the properties of code integrity and data secrecy defined in section 4.9.

In order to check the reachability properties $\texttt{DRT}\models\Phi$
defined in section 4.9, we give $\neg(\texttt{DRT}\models\Phi)$ as input query
for ProVerif - an attack with respect to this query would be a witness trace
for the desired reachability property. When returning such a trace, ProVerif
can either confirm that it is valid (_attack found_) or cannot confirm it. Our
models fall in the latter case, and we have to further inspect the output
trace to see how its steps can be used to reconstruct a valid trace: we do
observe in the output trace the expected intermediary messages on the channels
cpu_tpm and os, and we can follow the source of these messages up to a dynamic
root of trust request, of whose validity we have to again make sure. By a
similar analysis of attack traces returned by ProVerif, we can observe the
attacks of [13, 29] in our models, when we allow the STM to be modified
arbitrarily.

##  7 Further work

While our model takes into account at an abstract level the attacks and
mitigations of [13, 29], further refinements and soundness results are
necessary in order to be able to conclude that attacks such as these or as
[31, 30] are not possible in practice. We need to develop models that are
abstract enough to allow clear specifications and automated reasoning, and
realistic enough to capture for instance implementation flaws. We plan to see
how the models of this paper can be expressed in richer frameworks like
StatVerif [3] and SAPIC [21], in order to capture more closely the state
semantics of real platforms. We think the process transformation that we have
presented in section 5 is an instance of a more general result, whose
exploration would also be fruitful for future applications.

## References

  * [1] M. Abadi and C. Fournet.  Mobile values, new names, and secure communication.  In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL’01), pages 104–115, January 2001.
  * [2] M. Arapinis, S. Bursuc, and M. D. Ryan.  Reduction of equational theories for verification of trace equivalence: Re-encryption, associativity and commutativity.  In Degano and Guttman [11], pages 169–188.
  * [3] M. Arapinis, E. Ritter, and M. D. Ryan.  StatVerif: Verification of Stateful Processes.  In CSF, pages 33–47. IEEE Computer Society, 2011.
  * [4] W. Arthur, D. Challener, and K. Goldman.  A Practical Guide to TPM 2.0.  APress, 2015.
  * [5] M. Barbosa, B. Portela, G. Scerri, and B. Warinschi.  Foundations of hardware-based attested computation and application to SGX.  In IEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016, pages 245–260. IEEE, 2016\.
  * [6] B. Blanchet.  An efficient cryptographic protocol verifier based on Prolog rules.  In Computer Security Foundations Workshop (CSFW’01), 2001.
  * [7] B. Blanchet.  Automatic verification of correspondences for security protocols.  Journal of Computer Security, 17(4):363–434, 2009.
  * [8] B. Blanchet and A. Chaudhuri.  Automated formal analysis of a protocol for secure file sharing on untrusted storage.  In IEEE Symposium on Security and Privacy, pages 417–431. IEEE Computer Society, 2008.
  * [9] V. Cortier, J. Degrieck, and S. Delaune.  Analysing routing protocols: Four nodes topologies are sufficient.  In Degano and Guttman [11], pages 30–50.
  * [10] A. Datta, J. Franklin, D. Garg, and D. Kaynar.  A logic of secure systems and its application to trusted computing.  In Security and Privacy, 2009 30th IEEE Symposium on, pages 221–236. IEEE, 2009.
  * [11] P. Degano and J. D. Guttman, editors.  Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings, volume 7215 of Lecture Notes in Computer Science. Springer, 2012.
  * [12] S. Delaune, S. Kremer, M. D. Ryan, and G. Steel.  Formal analysis of protocols based on TPM state registers.  In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF’11), pages 66–82, Cernay-la-Ville, France, June 2011. IEEE Computer Society Press.
  * [13] L. Duflot, O. Grumelard, O. Levillain, and B. Morin.  ACPI and SMI handlers: some limits to trusted computing.  Journal in computer virology, 6(4):353–374, 2010.
  * [14] C. Fournet and J. Planul.  Compiling information-flow security to minimal trusted computing bases.  In G. Barthe, editor, ESOP, volume 6602 of Lecture Notes in Computer Science, pages 216–235. Springer, 2011.
  * [15] J. Franklin, S. Chaki, A. Datta, J. M. McCune, and A. Vasudevan.  Parametric verification of address space separation.  In Degano and Guttman [11], pages 51–68.
  * [16] J. Franklin, S. Chaki, A. Datta, and A. Seshadri.  Scalable parametric verification of secure systems: How to verify reference monitors without worrying about data structure size.  In IEEE Symposium on Security and Privacy, pages 365–379. IEEE Computer Society, 2010.
  * [17] J. A. Garay, M. Jakobsson, and P. D. MacKenzie.  Abuse-free optimistic contract signing.  In Advances in Cryptology - CRYPTO ’99, 19th Annual International Cryptology Conference, Santa Barbara, California, USA, August 15-19, 1999, Proceedings, pages 449–466, 1999.
  * [18] D. Grawrock.  Dynamics of a Trusted Platform: A Building Block Approach.  Intel Press, 2009.
  * [19] T. C. Group.  TCG Architecture Overview, Specification revision 1.4, 2007.  www.trustedcomputinggroup.org.
  * [20] T. C. Group.  TPM main specification, 2011.  www.trustedcomputinggroup.org.
  * [21] S. Kremer and R. Künnemann.  Automated analysis of security protocols with global state.  In IEEE Symposium on Security and Privacy, pages 163–178. IEEE Computer Society, 2014.
  * [22] R. Küsters and T. Truderung.  Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation.  In 22nd IEEE Computer Security Foundations Symposium (CSF 2009), pages 157–171. IEEE Computer Society, 2009.
  * [23] S. Meier.  Advancing automated security protocol verification.  PhD Thesis, ETH Zürich, 2013.
  * [24] S. Mödersheim.  Abstraction by set-membership: verifying security protocols and web services with databases.  In E. Al-Shaer, A. D. Keromytis, and V. Shmatikov, editors, ACM Conference on Computer and Communications Security, pages 351–360. ACM, 2010\.
  * [25] M. Paiola and B. Blanchet.  Verification of security protocols with lists: From length one to unbounded length.  In Degano and Guttman [11], pages 69–88.
  * [26] RSA Security Inc., v2.20.  PKCS #11: Cryptographic token interface standard.  June 2004.
  * [27] M. D. Ryan and B. Smyth.  Applied pi calculus.  In V. Cortier and S. Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press, 2011.
  * [28] B. Schmidt, S. Meier, C. J. F. Cremers, and D. A. Basin.  Automated analysis of Diffie-Hellman protocols and advanced security properties.  In S. Chong, editor, 25th IEEE Computer Security Foundations Symposium (CSF), pages 78–94. IEEE Computer Society, 2012.
  * [29] R. Wojtczuk and J. Rutkowska.  Attacking INTEL trusted execution technology.  Black Hat DC, 2009.
  * [30] R. Wojtczuk and J. Rutkowska.  Attacking INTEL TXT via SINIT code execution hijacking.  Invisible Things Lab, 2009.
  * [31] R. Wojtczuk, J. Rutkowska, and A. Tereshkin.  Another way to circumvent INTEL trusted execution technology.  Invisible Things Lab, 2009.
  * [32] Yubico AB, Kungsgatan 37, 111 56 Stockholm Sweden.  The YubiKey manual - Usage, configuration and introduction of basic concepts (version 2.2).  2010\.

##  Appendix A Operational semantics of the process calculus

$\begin{array}[]{ll}\texttt{(NIL)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{0\\})\rightarrow({\cal
N},\mathcal{M},\mathcal{P})\\\ \texttt{(BANG)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{!P\\})\rightarrow({\cal
N},\mathcal{M},\mathcal{P}\cup\\{P,!P\\})\\\ \texttt{(PAR)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{P\;|\;Q\\})\rightarrow({\cal
N},\mathcal{M},\mathcal{P}\cup\\{P,Q\\})\\\ \texttt{(NEW)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{\texttt{new}\,n;P\\})\rightarrow({\cal
N}\cup\\{n^{\prime}\\},\mathcal{M},\mathcal{P}\cup\\{P\\})\\\
&\;\;\;\;\;\;\;\;\;\text{where }n^{\prime}\notin{\cal N}\\\
\texttt{(COMM)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{\texttt{out}(U,T);P\;,\;\texttt{in}(U,A);Q\\})\rightarrow({\cal
N},\mathcal{M}^{\prime},\mathcal{P}\cup\\{P,Q\sigma\downarrow\\})\\\
&\;\;\;\;\;\;\;\;\;\text{where }\sigma\text{ is such that
}T=_{\mathcal{E}}A\sigma\text{ and}\\\ &\;\;\;\;\;\;\;\;\;\text{if
}\mathcal{M}\vdash_{\mathcal{E}}U,\text{ then
}\mathcal{M}^{\prime}=\mathcal{M}\cup\\{T\\};\text{ else,
}\mathcal{M}^{\prime}=\mathcal{M}\\\
\texttt{(IF}_{\texttt{T}}\texttt{)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{\texttt{if }U=V\texttt{ then
}P\texttt{\;else\;}Q\\})\rightarrow({\cal
N},\mathcal{M},\mathcal{P}\cup\\{P\\})\\\ &\;\;\;\;\;\;\;\;\;\text{if
}U=_{\mathcal{E}}V\\\ \texttt{(IF}_{\texttt{F}}\texttt{)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{\texttt{if }U=V\texttt{ then
}P\texttt{\;else\;}Q\\})\rightarrow({\cal
N},\mathcal{M},\mathcal{P}\cup\\{Q\\})\\\ &\;\;\;\;\;\;\;\;\;\text{if
}U\neq_{\mathcal{E}}V\\\ \texttt{(LET)}&({\cal
N},\mathcal{M},\mathcal{P}\cup\\{\texttt{let\; }x=T\texttt{\; in\;
}{P}\\})\rightarrow({\cal N},\mathcal{M},\mathcal{P}\cup\\{P[x\mapsto
T]\downarrow\\})\\\ &\;\;\;\;\;\;\;\;\;\text{if }T\downarrow\text{ does not
contain destructors}\\\ \end{array}$ Figure 8: Operational semantics

##  Appendix B ProVerif code

    (***
    ABBREVIATIONS:
    DRT - DYNAMIC ROOT OF TRUST
    DRT_INIT - THE SINIT (INTEL) OR SLB (AMD) PROGRAM
    DRT_PP - THE PROTECTED PROGRAM: MLE(INTEL) OR SK(AMD)
    ***)

    param reconstructTrace = false.

    (*CHANNELS*)
    free os. (* PUBLIC CHANNEL FOR THE OPERATING SYSTEM CONTROLLED BY THE INTRUDER *)Ψ
    private free cpu_tpm.  (* PRIVATE CHANNEL FOR THE COMMUNICATION BETWEEN CPU AND TPM *)
    private fun tpm_ch/1. (* tpm_ch(x) REPRESENTS A PRIVATE CHANNEL USED BY
              A PROGRAM x TO COMMUNICATE WITH TPM *)
    (*CRYPTO*)
    fun h/1.Ψ(* HASH FUNCTION *)
    fun senc/2.Ψ(* SYMMETRIC ENCRYPTION *)
    reduc sdec(x,senc(x,y)) = y.
    fun ps/0.  (* STATIC RESET VALUE OF THE PCR *)
    fun pd/0.  (* DYNAMIC RESET VALUE OF THE PCR *)
    fun false/0. fun true/0. (* BOOLEAN VALUES *)

    (* TPM SEAL/UNSEAL*)
    fun seal/2.
    private reduc unseal(seal(xpcr,xvalue), xpcr) = xvalue.

    (* STATE STRUCTURE: state(tpm(PCR),cpu(INT,CACHE), drt(INIT,PP,LOCK),smram(STM,SMI) *)
    private fun state/4. private fun tpm/1. private fun cpu/2.
    private fun drt/3.  private fun smram/2.

    (*EXAMPLE STATE:
    state(tpm(pd),cpu(true,false), drt(program(expected_init),program(expected_pp),true),
    smram(program(expected_stm),program(expected_smih)))
    *)

    (* PRIVATE CONSTANTS FOR THE PRIVILEGED ACCESS THAT
    THE CPU AND TPM HAVE TO THE PLATFORM STATE *)
    private fun cpuAccess/0. private fun tpmAccess/0.

    (* ABSTRACTION FOR DYNAMICALLY LOADING PROGRAMS*)
    fun program/1.
    private reduc getENTRY(program(x)) = x.

    (*** ACCESSING THE PLATFORM STATE ***)
    reduc getPCR (state(tpm(y),x1,x2,x3)) = y.
    reduc getINT(state(x1,cpu(y1,y2),x2,x3)) = y1.
    reduc getCACHE(state(x1,cpu(y1,y2),x2,x3)) = y2.
    reduc getINIT(state(x1,x2,drt(y1,y2,y3),x3)) = y1.
    reduc getPP(state(x1,x2,drt(y1,y2,y3),x3)) = y2.
    reduc getLOCK(state(x1,x2,drt(y1,y2,y3),x3)) = y3.
    reduc getSTM (state(x1,x2,x3,smram(y1,y2))) = y1.
    reduc getSMIH (state(x1,x2,x3,smram(y1,y2))) = y2.

    (*** MODIFYING THE PLATFORM STATE + ABILITIES OF LOADED PROGRAMS ***)
    (* TPM *)
    reduc resetPCR (state(tpm(y),x1,x2,x3),tpmAccess,pd)ΨΨ=state(tpm(pd),x1,x2,x3);
          resetPCR (state(tpm(y),x1,x2,x3),tpmAccess,ps)ΨΨ=state(tpm(ps),x1,x2,x3).

    reduc
        (*** PROBLEMATIC EQUATIOn *)
          extendPCR(state(tpm(x),x1,x2,x3), tpmAccess, value) =
          state(tpm(h((x,value))),x1,x2,x3).
        (***)

    reduc setPCR(state(tpm(y),x1,x2,x3),tpmAccess,value)ΨΨ=state(tpm(value),x1,x2,x3).

    reduc isSMALL(pd) = true;
          isSMALL(ps) = true;
          isSMALL(h((pd,y))) = true;
          isSMALL(h((ps,y))) = true.

    reduc isBIG(h((h((h((x,y)),z)),w))) = true.

    (* CPU *)
    reduc setINT(state(x1,cpu(y1,y2),x2,x3),cpuAccess,value) = state(x1,cpu(value,y2),x2,x3);
          setINT(state(x1,cpu(y1,y2),drt(z1,program(z2),true),x2),z2,value) =
          state(x1,cpu(value,y2),drt(z1,program(z2),true),x2).
    reduc cache(state(x1,cpu(y1,y2),x2,x3),value) = state(x1,cpu(y1,value),x2,x3).
    reduc flush_smi(state(x1,cpu(y1,y2),x2,smram(z1,z2))) =
          state(x1,cpu(y1,y2),x2,smram(z1,y2)).
    reduc flush_stm(state(x1,cpu(y1,y2),drt(w1,w2,false),smram(z1,z2))) =
          state(x1,cpu(y1,y2),drt(w1,w2,false),smram(y2,z2)).
    (* TO OBTAIN THE ATTACK, ADD THE EQUATION: *)
    (* flush_stm(state(x1,cpu(y1,y2),x2,smram(z1,z2))) = state(x1,cpu(y1,y2),x2,smram(y2,z2)). *)

    (* DRT *)
    reduc setINIT(state(x1,x2,drt(y1,y2,y3),x3),cpuAccess,value) Ψ=
          state(x1,x2,drt(value,y2,y3),x3).
    reduc setPP(state(x1,x2,drt(y1,y2,y3),x3),cpuAccess,value)Ψ=
          state(x1,x2,drt(y1,value,y3),x3);
          setPP(state(x1,x2,drt(program(y1),y2,y3),x3),y1,value)Ψ=
          state(x1,x2,drt(program(y1),value,y3),x3);
          setPP(state(x1,cpu(true,z),drt(y1,y2,y3),
                smram(program(z1),program(z2))),(z1,z2),value)=
          state(x1,cpu(true,z),drt(y1,value,y3),smram(program(z1),program(z2))).
    reduc setLOCK(state(x1,x2,drt(y1,y2,y3),x3),cpuAccess,value)Ψ=
          state(x1,x2,drt(y1,y2,value),x3);
          setLOCK(state(x1,x2,drt(y1,program(y2),true),x3),y2,value)=
          state(x1,x2,drt(y1,program(y2),value),x3);
          setLOCK(state(x, cpu(true,z),drt(y1,y2,y3),
          smram(program(z1),program(z2))),(z1,z2),value)
    Ψ=state(x,cpu(true,z),drt(y1,y2,value),smram(program(z1),program(z2))).
    ΨΨΨΨΨΨΨ

    (** MESSAGE TAGS **)ΨΨ
    free drt_request,drt_response,pcr_extend_request,pcr_extend_response,
    pcr_reset_request,pcr_reset_response, drt_start, tag_unseal, tag_plain, ext_channel.

    (* FUNCTION FOR CREATING NONCES *)
    private fun fnonce/1.

    let DRT_CPU = (* GET A DRT REQUEST FROM THE OPERATING SYSTEM *)
      ΨΨ  in(os, (=drt_request, drt_init, drt_pp, pf_state));
    ΨΨ  (* ONLY ACCEPT THE REQUEST IF NOT ALREADY RUNNING A DYNAMIC ROOT OF TRUST *)
    ΨΨ  if getLOCK(pf_state) = false then
    ΨΨ  (
    ΨΨ   (* DISABLE INTERRUPTS *)
    ΨΨ   let s0’=setINT(pf_state,cpuAccess, false) in
    ΨΨ   (* UPDATE THE LOCK *)
    ΨΨ   let s0 = setLOCK(s0’, cpuAccess, true) in

    ΨΨ   (* RESET THE PCR *)
    ΨΨ   (* DESIRED CODE: *)
    ΨΨ   (* new nonce; *)
    ΨΨ   (* CLASSIC ABSTRACTION THAT RUNS FASTER: NONCES ARE A FUNCTION OF THEIR CONTEXT *)
    ΨΨ   let nonce = fnonce((drt_init,drt_pp, getSTM(pf_state))) in
    ΨΨ
    ΨΨ   out(cpu_tpm, (pcr_reset_request, nonce, s0));
    ΨΨ   in(cpu_tpm, (=pcr_reset_response,=nonce,s1));
    ΨΨ
    ΨΨ   (* EXTEND THE PCR WITH THE MEASUREMENT *)
    ΨΨ   let measurement = (h(drt_init),h(getSTM(pf_state))) in
    ΨΨ   out(cpu_tpm, (pcr_extend_request, nonce, s1, measurement));
    ΨΨ   in(cpu_tpm, (=pcr_extend_response, =nonce,s2));
    ΨΨ
    ΨΨ   (* LOAD DRT_INIT AND ESTABLISH TPM CHANNELS *)
    ΨΨ   let s3 = setINIT(s2,cpuAccess, drt_init) in
    ΨΨ   out(cpu_tpm, (ext_channel, tpm_ch(drt_init)));
    ΨΨ   let entry_init = getENTRY(drt_init) in
    ΨΨ   out(entry_init, (drt_request, nonce, s3, tpm_ch(drt_init), drt_pp));
    ΨΨ
    ΨΨ   (* THE drt_init PROGRAM HAS MEASURED AND SET UP THE drt_pp PROGRAM*)
    ΨΨ    in(entry_init, (=drt_response, =nonce, new_state));
    ΨΨ
    ΨΨ   (* SETUP TPM CHANNELS FOR THE LOADED DRT_PP *)
    ΨΨ    let entry_pp = getENTRY(getPP(new_state)) in
    ΨΨ    out(entry_pp, (drt_start, new_state, tpm_ch(program(entry_pp))));
    ΨΨ    out(cpu_tpm, (ext_channel, tpm_ch(program(entry_pp))))
    ΨΨ
    ΨΨ   ).

    (*
    THE TWO EQUATIONS BELOW TOGETHER WITH THE CACHE PROCESS ARE A CONSEQUENCE OF
    cache, flush_smi,flush_stm EQUATIONS. WRITING THEM EXPLICITLY HELPS PROVERIF
    TERMINATE 5 MINUTES FASTER
    *)
    reduc setSTM (state(x1,x2,x3,smram(y1,y2)),cpuAccess,value)Ψ=
    state(x1,x2,x3,smram(value,y2)).
    reduc setSMIH(state(x1,x2,x3,smram(y1,y2)),cpuAccess,value)Ψ=
    state(x1,x2,x3,smram(y1,value)).
    let CACHE = ( in(os, (pf_state,xsmi));
    ΨΨlet new_state = setSMIH(pf_state,cpuAccess, xsmi) in
    ΨΨout(os, new_state) )
    ΨΨ|
    ΨΨ( in(os,(pf_state,xstm));
    ΨΨif getLOCK(pf_state) = false then
    ΨΨlet new_state = setSTM(pf_state,cpuAccess,xstm) in
    ΨΨout(os, new_state) ).
    ΨΨ
    private fun expected_init/0.
    let EXPECTED_INIT = out(os, program(expected_init));
    ΨΨ    (* RECEIVE DRT_PP AND TPM ACCESS FROM THE CPU *)
    ΨΨ    in(expected_init, (=drt_request, nonce0, pf_state, tpmc, drt_pp));
    ΨΨ    (* MEASURE AND EXTEND DRT_PP INTO THE PCR *)
    ΨΨ    let measurement = h(drt_pp) in
    ΨΨ    (* DESIRED CODE: *)
    ΨΨ    (* new nonce; *)
    ΨΨ    (* CLASSIC ABSTRACTION THAT RUNS FASTER: NONCES ARE A FUNCTION OF THEIR CONTEXT *)
    ΨΨ    let nonce = fnonce(drt_pp) in
    ΨΨ    out(tpmc, (pcr_extend_request,nonce, pf_state, measurement));
    ΨΨ    in(tpmc, (=pcr_extend_response,=nonce, ext_state));
    ΨΨ    (* LOAD DRT_PP ON THE PLATFORM STATE *)
    ΨΨ    let new_state = setPP(ext_state,expected_init, drt_pp)  in
    ΨΨ    (* PASS THE CONTROL BACK TO THE CPU *)
    ΨΨ    out(expected_init, (drt_response, nonce0, new_state));
    ΨΨ    (* MAKE THE NEW PLATFORM STATE PUBLIC *)
    ΨΨ    out(os, new_state).

    private fun expected_pp/0.
    let EXPECTED_PP = (* DECRYPT A SEALED BLOB, RELYING ON COMMUNICATION WITH TPM*)
    ΨΨ  out(os, program(expected_pp));
    ΨΨ  in(expected_pp, (=drt_start,pf_state0,tpmc));
    ΨΨ  (* RE-ENABLE INTERRUPTS *)
    ΨΨ  let pf_state = setINT(pf_state0,expected_pp,true) in
    ΨΨ  out(os,pf_state);
    ΨΨ  (* UNSEAL THE KEY AND DECRYPT THE PRIVATE MESSAGE *)ΨΨ
    ΨΨ  in(os,xSealedBlob);  in(os,xEncBlob);
    ΨΨ  out(tpmc,(tag_unseal,xSealedBlob));
    ΨΨ  in(tpmc,(=tag_plain,xSymKey));
    ΨΨ  let xMessage = sdec(xSymKey,xEncBlob) in
    ΨΨ  out(os,xMessage);

    ΨΨ  (* ENDING THE EXECUTION: THE LOCK IS SET TO FALSE AND THE PCR VALUE IS DESTROYED *)
    ΨΨ  (*new nonce; *)
    ΨΨ  (* ABSTRACTION THAT RUNS FASTER *)
    ΨΨ  let nonce = fnonce(drt_pp) in
    ΨΨ  out(tpmc, (pcr_extend_request, nonce, pf_state, zero));
    ΨΨ  in(tpmc, (=pcr_extend_response, =nonce, ext_state));
    ΨΨ  let end_state = setLOCK(ext_state,expected_pp,false) in
    ΨΨ  out(os,end_state).

    let TPM = !TPM_RESET | !TPM_EXTEND | !TPM_UNSEAL.

    let TPM_RESET = let (channel, reset_type) = (cpu_tpm,pd) in !PCR_RESET |
    ΨΨ let (channel, reset_type) = (os,ps) in !PCR_RESET.
    ΨΨ
    let PCR_RESET = in(channel, (=pcr_reset_request, nonce, pf_state));
    ΨΨlet new_state = resetPCR(pf_state,tpmAccess,reset_type) in
    ΨΨout(channel, (pcr_reset_response, nonce, new_state)).

    let TPM_EXTEND = let channel = os in !PCR_EXTEND_BOUND |
    ΨΨ let channel = cpu_tpm in !PCR_EXTEND_BOUND |
    ΨΨ !in(cpu_tpm, (=ext_channel, channel)); !PCR_EXTEND_BOUND.

    ΨΨ
    let PCR_EXTEND = in(channel, (=pcr_extend_request,nonce,pf_state,value));
    ΨΨ let new_state = extendPCR(pf_state,tpmAccess,value) in
    ΨΨ out(channel, (pcr_extend_response,nonce,new_state)).
    ΨΨ
    ΨΨ
    let PCR_EXTEND_BOUND =
    ΨΨ in(channel, (=pcr_extend_request,nonce,pf_state,value));
    ΨΨ let pcr  = getPCR(pf_state) in
    ΨΨ if isSMALL(pcr)=true then
    ΨΨ PCR_EXTEND_SMALL else PCR_EXTEND_BIG.

    let PCR_EXTEND_SMALL
    Ψ      = let new_state = extendPCR(pf_state,tpmAccess,value) in
    ΨΨout(channel, (pcr_extend_response,nonce,new_state)).

    let PCR_EXTEND_BIG
    Ψ      =
    Ψ      out(os,(pcr,val)); in(os,new_pcr);
                  if isBIG(new_pcr)=true then
                  let new_state = setPCR(pf_state,tpmAccess,new_pcr) in
    Ψ      out(channel, (pcr_extend_response,nonce,new_state)).
    ΨΨ
    let TPM_UNSEAL = in(os, (=tag_unseal, pf_state, blob));
    Ψ      Ψ let value = unseal(blob, getPCR(pf_state)) in
    ΨΨ if getLOCK(pf_state) = true then
    ΨΨ  (  let channel = tpm_ch(getPP(pf_state)) in
    ΨΨ     out(channel, (tag_plain, value)) )
    ΨΨ else
    ΨΨ     out(os, (tag_plain, value)).

    ΨΨ
    (* QUERIES *)ΨΨΨΨ
    (*A. THE EXPECTED STATE HAS BEEN REACHED *)
    query attacker:state(tpm(h((h((pd,(h(program(expected_init)),h(program(expected_stm))))),
    Ψ             h(program(expected_pp))))), cpu(true,x),
    ΨΨ      drt(program(expected_init),program(expected_pp),true),
    ΨΨ      smram(program(expected_stm),program(y))).
    (* QUERY RESULT: PROVERIF RETURNS AN ATTACK TRACE THAT CAN BE INSPECTED FOR VALIDITY *)

    (*B. THE PROTECTED PROGRAM SUCCESFULLY DECRYPTS THE PRIVATE
    MESSAGE USING THE SEALED KEY AND MAKES IT PUBLIC*)
    query attacker:hello_pp.ΨΨΨΨΨΨΨΨ
    (* QUERY RESULT: PROVERIF RETURNS AN ATTACK TRACE THAT CAN BE INSPECTED FOR VALIDITY *)
    ΨΨ
    (*C. WHENEVER THE EXPECTED PCR IS SET,
    THE PLATFORM HAS THE EXPECTED STATE *)
    query attacker:state( tpm(h((h((pd,(h(program(expected_init)),
                              h(program(expected_stm))))),h(program(expected_pp))))),
    ΨΨ      cpu(x,y),drt(xi,xp,true),
    ΨΨ      smram(xstm,xsmih))
    ΨΨ==> (xi,xp,xstm)=(program(expected_init),program(expected_pp),program(expected_stm)).
    ΨΨ
    (*QUERY RESULT: TRUE => THE ASSERTION IS VALID*)

    (*D. THE ATTACKER DOES NOT HAVE ACCESS TO THE SEALED KEY *)
    query attacker:k_pp.ΨΨΨΨ
    (* QUERY RESULT: TRUE => THE ATTACKER DOES NOT HAVE k_pp *)

    (* THE MAIN PROCESS *)
    free null.
    private fun expected_stm/0.
    private free k_pp.Ψ(* SECRET KEY WHICH SHOULD ONLY BE KNOWN BY THE PROTECTED PROGRAM *)
    private free hello_pp.Ψ(* PRIVATE MESSAGE ENCRYPTED WITH k_pp *)
    process (* ENCRYPTED PRIVATE MESSAGE FOR PP *)
    Ψout(os,senc(k_pp,hello_pp));
    Ψ(*ASSUME THAT THE BLOB SEALING THE SECRET KEY IS PUBLIC*)
    Ψout(os,seal(h((h((pd,(h(program(expected_init)),h(program(expected_stm))))),h(program(expected_pp)))),k_pp));
    Ψ
    Ψout(os, program(expected_stm));
    Ψ(* INITIAL STATE LOADED UPON A SYSTEM RESET *)
    Ψin(os,(xInitStm,xInitSmih));
    Ψout(os, state(tpm(ps),cpu(true,null),drt(null,null,false),smram(xInitStm,xInitSmih)));
    Ψ(* REQUESTING A DYNAMIC ROOT OF TRUST WITH ANY LOADED PROGRAMS *)
    Ψin(os, drt_init); in(os,drt_pp); in(os,pf_state);
    Ψout(os, (drt_request, drt_init, drt_pp, pf_state));
    Ψ(*EXECUTING THE DRT PROCESSES *)
            ( !DRT_CPU | !CACHE | !EXPECTED_INIT | !EXPECTED_PP | TPM)