Developing secure distributed systems is difficult, and
even harder when advanced cryptography must be used
to achieve security goals.
Following prior work, we advocate using secure program partitioning to
synthesize cryptographic applications:
instead of implementing a system of communicating processes,
the programmer implements a centralized, sequential program,
which is automatically compiled into a secure distributed version
that uses cryptography.

While this approach is promising, formal results for the security of such compilers
are limited in scope. In particular, no security proof yet simultaneously
addresses subtleties essential for robust, efficient applications:
multiple cryptographic mechanisms, malicious
corruption, and asynchronous communication.

In this work, we develop a compiler security proof that handles these subtleties.
Our proof relies on a novel unification of
simulation-based security, information-flow control, choreographic programming,
and sequentialization techniques for concurrent programs.
While our proof targets hybrid protocols, which abstract cryptographic
mechanisms as idealized functionalities, our approach offers a clear path toward
leveraging Universal Composability to obtain end-to-end, modular security
results with fully instantiated cryptographic mechanisms.

Finally, following prior observations about simulation-based security,
we prove that our result guarantees robust hyperproperty preservation,
an important criterion for compiler correctness that preserves
all source-level security properties in target programs.

§ INTRODUCTION

Ensuring security for modern distributed applications remains a difficult
challenge, as such systems can cross administrative boundaries and involve
parties that do not fully trust each other.
To defend their security policies, some applications employ sophisticated
mechanisms such as complex distributed protocols <cit.>,
trusted hardware <cit.>,
and advanced uses of cryptography.
These technologies add significant complexity to software
development and require expertise to use
successfully <cit.>.

To ease the development of secure distributed applications,
prior work leverages compilers that translate high-level programs into
distributed protocols that employ advanced security mechanisms.
Unfortunately, most compilers only target a single mechanism—such as multiparty computation <cit.>,
zero-knowledge proofs <cit.>,
or homomorphic encryption <cit.>—and thus do not support
secure combinations of mechanisms.
On the other hand, compilers that perform
secure program partitioning <cit.>
do combine mechanisms, but come with limited or informal correctness guarantees.

In this work, we give the first formal security result for program partitioning
that targets multiple cryptographic mechanisms, arbitrary corruption, and
adversarially controlled scheduling.
Our work proves the correctness of a reasonably faithful model of the compilation process used in the Viaduct compiler <cit.>.
We formalize our result in the simulation-based security framework, which establishes a modular foundation for cryptographic protocol security <cit.>.
Our security proof is primarily concerned with program partitioning itself, and
thus does not reason about the concrete instantiation of cryptographic mechanisms;
however, we discuss how to extend our results to reason about concrete

Our security proof incorporates multiple techniques for
simulationbased security:
informationflow type systems <cit.> to define the security policy
and to guide partitioning,
choreographies <cit.> to define global programs for
distributed executions,
and a novel informationflow guided technique for concurrent program
sequentialization <cit.>.

* We formalize a variant of Simplified Universal Composability (SUC) <cit.>
enriched with information flow, allowing us to capture distributed protocols
in the presence of adversarial scheduling and corruption.

* We show how to model secure program partitioning using
security-typed choreographies <cit.>.
The input to program partitioning is a sequential program
representing an idealized execution on a single, trusted security domain,
while the output is a distributed protocol with message-passing concurrency
between mutually distrusting agents.

* We prove simulation-based security for our model of program partitioning.
Informally, we show that any adversary interacting with the
compiled distributed program is no more powerful than a corresponding adversary
(a simulator) interacting with the source program.

* We show that, in our setting, simulation implies
robust hyperproperty preservation <cit.>,
a strong criterion for compiler correctness that ensures security conditions
of source programs are preserved in target programs.

This technical report is an expanded version of the corresponding
conference paper <cit.>. In particular, it includes
the proof details that had to be omitted for reasons of space, found
in Appendices A–G.

node distance=,
every node/.style=align=center,
program/.style=draw, rounded corners, text width=9em, minimum height=8ex,
transformation/.style=->, >=stealth', rounded corners=0.5mm,
[program] (1)
Sequential Source
$\source{\process}$, $\idealstepsto{}$;
[simulation] (12) [right=of 1]
[program] (2) [right=of 12]
$\corrupt{\process}$, $\realstepsto!{}$;
[simulation] (23) [right=of 2]
[program] (3) [right=of 23]
Hybrid Distributed
$\corrupt{\partition{\process}}$, $\realstepsto{}$;
[simulation] (34) [right=of 3]
[program] (4) [dashed, right=of 34]
Concrete Distributed;

– ++(0, )
-| node [pos=0.25, above] Protocol Synthesis ([xshift=-]2.north);

– ++(0, )
-| node [pos=0.25, above] Endpoint Projection ([xshift=-]3.north);

[transformation, dashed]
– ++(0, )
-| node [pos=0.25, above] Cryptographic Instantiation (4.north);

Overview of compilation and the correctness proof.
Left-to-right arrows are compilation steps; $\simulatedBy$ are proof steps.
Term is a choreography,
$\partition{\cdot}$ is endpoint projection,
$\source{\cdot}$ is the inverse of protocol synthesis,
and $\corrupt{\cdot}$ models corruption.
Dashed components represent proof sketches.

Source program with information-flow labels.
\(
\begin{program}
\slethead{a : \lalice}{\einputh{\alice}}
\\
\slethead{b : \lbob}{\einputh{\bob}}
\\
\slethead{x}{
\edeclassify
{\dendorse{a} < \dendorse{b}}
{\\ \hspace{9em} \iflabel{A \wedge B}}
{\iflabel{A \meet B}}}
\\
\eoutputh{x}{\alice}
\\
\eoutputh{x}{\bob}
\end{program}
\)

Choreography with explicit communication and synchronization.
\(
\begin{program}
\slethhead{a}{\alice}{\einput{\alice}}
\\
\smovehead{\alice}{a}{\MPCalicebob}{a'}
\\
\slethhead{b}{\bob}{\einput{\bob}}
\\
\smovehead{\bob}{b}{\MPCalicebob}{b'}
\\
\slethhead{x}{\MPCalicebob}{\\ \hspace{4em}\ddeclassify{(\dendorse{a'} < \dendorse{b'})}}
\\
\smovehead{\MPCalicebob}{x}{\alice}{x_1}
\\
\smovehead{\MPCalicebob}{x}{\bob}{x_2}
\\
\eoutputh{x_1}{\alice}
\\
\smovehead{\alice}{\vunit}{\bob}{\_}~\scomment{Sync outputs}
\\
\eoutputh{x_2}{\bob}
\end{program}
\)

Hybrid distributed program derived by projecting choreography.
\(
\begin{program}
\scomment{\alice}
\\
\slethead{a}{\einput{\alice}}
\\
\esend{a}{\MPCalicebob}
\\
\slethead{x_1}{\ereceive{\MPCshort}}
\\
\eoutput{x_1}{\alice}
\\
\esend{\vunit}{\bob}~\scomment{Sync}
\end{program}
\)
\(
\begin{program}
\scomment{\bob}
\\
\slethead{b}{\einput{\bob}}
\\
\esend{b}{\MPCalicebob}
\\
\slethead{x_2}{\ereceive{\MPCshort}}
\\
\slethead{\_}{\ereceive{\alice}}~\scomment{Sync}
\\
\eoutput{x_2}{\bob}
\end{program}
\)

\(
\begin{program}
\scomment{\MPCalicebob}
\\
\slethead{a'}{\ereceive{\alice}}
\\
\slethead{b'}{\ereceive{\bob}}
\\
\slethead{x}{\ddeclassify{(\dendorse{a'} < \dendorse{b'})}}
\\
\esend{x}{\alice}
\\
\esend{x}{\bob}
\end{program}
\)

Concrete distributed program derived by instantiating idealized hosts.
\(
\begin{program}
\scomment{\alice}
\\
\slethead{a}{\einput{\alice}}
\\
\scomment{Calls to MPC library}
\\
\eoutput{x_1}{\alice}
\\
\esend{\vunit}{\bob}~\scomment{Sync}
\end{program}
\)
\(
\begin{program}
\scomment{\bob}
\\
\slethead{b}{\einput{\bob}}
\\
\scomment{Calls to MPC library}
\\
\slethead{\_}{\ereceive{\alice}}~\scomment{Sync}
\\
\eoutput{x_2}{\bob}
\end{program}
\)

Compiling the Millionaires' Problem

§ OVERVIEW

We illustrate compilation via the classic Millionaires' Problem <cit.>,
expressed as the source program in <ref>.
Here, and learn who is richer without revealing their net
worth to each other.
To do so, the program collects inputs from and representing their net worth (lines 1 and 2);
compares these (line 3),
and outputs the result to and (lines 4 and 5).

§.§ Information Flow Control

Source programs prevent insecure information flows using a security type
system <cit.>, which assigns a label to every variable.
Labels track the confidentiality and integrity of data.
Our security type system follows prior work <cit.>
in using downgrading mechanisms—and expressions—to
selectively allow information flows that would otherwise be deemed insecure.
As in prior work <cit.>,
the type system constrains these downgrading mechanisms
to prevent improper usage. These constraints turn out to be crucial.

In <ref>, the expression explicitly allows revealing the
result of the comparison $a < b$ to and , which is by default disallowed
since the computation reads secrets from both parties.
Dually, the expressions allow untrusted data coming from
and to influence the output from the comparison,
which must be trusted since the value is output to both parties.

Downgrading require explicit source and target labels.
<Ref> suppresses these labels for the expressions, but shows the expression that moves from
$\iflabel{A \wedge B}$ to $\iflabel{A \sqcap B}$.
Label $\iflabel{A \wedge B}$ is too secret for either or to see the value; label $\iflabel{A \sqcap B}$ allows both parties
to see it.

§.§ Compilation

Source programs serve as specifications of intended behavior,
and correspond to ideal functionalities from Universal Composability <cit.>.
Source programs act as trusted third parties, perfectly and securely executing
the program on behalf of the involved hosts.
The source language is high-level by design, and its simple, sequential
semantics facilitate reasoning.
Our compiler generates a concurrent distributed program that correctly
implements the same behavior.

<Ref> gives an overview of the compilation pipeline.
First, protocol synthesis compiles the source program into
a choreography, a single, centralized program that represents a
distributed computation between many hosts.
In addition to parties such as and ,
choreographies may mention idealized hosts such as ,
which represents a maliciously secure multiparty computation protocol between
and .
Idealized hosts can perform computations that require high confidentiality
or integrity.
Next, endpoint projection,
a standard procedure in choreographic programming <cit.>,
partitions the choreography into a distributed program,
where hosts run in parallel and interact via message passing.
The distributed program still contains idealized hosts,
so it corresponds to a hybrid program in UC.
Finally, cryptographic instantiation replaces idealized hosts with
concrete cryptographic algorithms.

<Ref> shows a choreography where
and perform their respective and statements,
while does the comparison.
Explicit communication statements move data between hosts.
Choreographies have concurrent semantics, so
statements at different hosts may step out of program order.
The penultimate line
has synchronization between and : must
wait on an input from before delivering output.
This synchronization step is necessary for the distributed program to match the
sequential source program, in which 's output happens after 's.
<Ref> shows the distributed program obtained by
projecting the choreography in <ref>.
Endpoint projection converts communication statements
to /pairs,
and projects local computations to their corresponding hosts.
Finally, <ref> shows the result of cryptographic
Each /statement that interacts with is
replaced with a call to a cryptographic library.

§.§ Defining Correctness

Our main contribution is a proof that compilation is correct.
A correct compiler preserves properties of source programs in generated
target programs.
For generality, we demand that the compiler
preserve all hyperproperties <cit.> guaranteed by the source program.
Hyperproperties capture many common notions of security,
including secure information flow.

Formally, preserving all hyperproperties is defined via
robust hyperproperty preservation (RHP) <cit.>.
Following prior observations <cit.>,
we do not prove RHP directly, but instead prove simulation,
which we show implies RHP in our framework.
Simulation requires every attack by an adversary against the
target program to be possible against the source program.
Ideally, the source program is “obviously secure,”
meaning it has straightforward, sufficiently abstract semantics
and a narrow attack surface.
In contrast, the target program faithfully models
real code and has a realistic attack surface.

As with UC, our framework abstracts concrete cryptographic
mechanisms as idealized hosts, yielding an extensible
proof that is generic over the set of supported cryptographic mechanisms.
Indeed, we sketch how our framework may be embedded into UC
to leverage the UC composition theorem <cit.>;
using the composition theorem, we can instantiate idealized hosts with
cryptographic mechanisms proven secure separately.

Threat Model
Simulation demands we carefully define the capabilities of adversaries for
each language in the pipeline.

Adversaries are characterized by two sets of labels and representing public and untrusted labels.
These label sets induce a partitioning of hosts into three sets:
honest (secret and trusted),
semi-honest (public and trusted),
and malicious (public and untrusted).
Intuitively, malicious hosts are fully controlled by the adversary,
and semi-honest hosts follow the protocol
but leak all their data to the adversary <cit.>.

We say a host is dishonest if it is semi-honest or malicious,
and nonmalicious if it is honest or semi-honest.

Source programs are fully sequential, so adversaries do not control scheduling.
Moreover, adversaries cannot read or change intermediate data within a source
However, adversaries can read messages from /expressions
involving dishonest hosts,
read the results of expressions with public target labels,
and change the results of expressions with untrusted source labels.

Choreographies and hybrid distributed programs have the same semantics,
so their adversaries have equal power.
These programs are concurrent and the adversary controls all scheduling.
The adversary also fully controls malicious hosts
and can read messages involving at least one semi-honest host.
However, the adversary cannot carry out computational attacks,
since cryptographic mechanisms are modeled as idealized hosts.

The adversary can view all message headers (source and destination),
but not necessarily message content.
The adversary may not drop, duplicate, or modify messages.
This abstraction of secure channels can be realized by standard techniques,
such as TLS <cit.>.
In our model as in most models of cryptographic protocols <cit.>,
the adversary can exploit timing and progress channels
since it controls scheduling.
These channels make secret control flow insecure:
any discrepancy in timing or progress behavior between different
control-flow paths can be detected by the adversary.
Therefore, we only prove security for programs that make control flow
decisions based on public, trusted data.

§.§ Roadmap of Correctness Proof

To define and prove our compilation pipeline secure, we make use of
simulation (<ref>), which defines a relation $\simulates$
between semantic configurations. Intuitively, $\config_1 \leq \config_2$
means that any adversary against configuration $\config_1$ is no more powerful than
an equivalent adversary against $\config_2$. Crucially, the attacker often has more
choices in $\config_1$ (e.g., low-level scheduling decisions); the role of
simulation is to show that these extra choices are benign, and thus $\config_1$
is as secure as $\config_2$.

Our proof exploits the transitivity of simulation, using
multiple intermediate simulations depicted in
<Ref>. (To follow the flow of compilation, the figure
uses $\simulatedBy$, which is defined as expected.)

Correctness of Protocol Synthesis
We first prove in <ref> that
protocol synthesis is correct:
sequential source programs (e.g., <ref>)
are simulated by their choreographies (e.g., <ref>).

There is a wide semantic gap between source programs and choreographies:
while source programs are sequential and use /expressions
to interface with the adversary, choreographies are concurrent and allow the
adversary to read and corrupt data controlled by dishonest hosts.
To bridge this gap, we break the protocol synthesis proof itself into
three steps (<ref>).
These steps allow us to reason separately about the
semantic features of choreographies.

Aside from employing transitivity, each proof step $\config_1 \simulates \config_2$
requires us to define an appropriate simulator $\simulator(\cdot)$ such
that for any adversary $\adv$, $\config_1$ running alongside $\adv$ is identical
in behavior to $\simulator(\adv)$ running alongside $\config_2$.
Thus, after defining the simulator as a labeled transition system,
we show that the two resulting configurations are bisimilar using standard
information-flow arguments (e.g., by defining an appropriate notion of
low-equivalence between the configurations).

Correctness of Protocol Synthesis
Second, we prove in <ref> that choreographies are
simulated by their corresponding distributed programs (e.g.,
<ref>). Our proof (<ref>) largely follows
the choreographic programming literature <cit.>,
but deals with extra complications arising from an adversary who may corrupt hosts.

Cryptographic Instantiation
Finally, we sketch in <ref>
how hybrid distributed programs are simulated by concrete
distributed programs, which make use of actual cryptographic mechanisms.
In particular,
we show how to embed our framework in the SUC <cit.> framework,
which in turn embeds into the full UC framework.
We can then leverage the UC composition theorem to instantiate idealized hosts
one at a time, appealing to existing correctness proofs for cryptographic

§ SEMANTIC FRAMEWORK

[Endpoints]! = ,  ∪!
[Values]! = , …

Syntax of messages and actions.

We capture the semantics of programs using labeled transition systems (LTSs),
where labels are actions drawn from the grammar in
An action is either the input $\ainput{\msg}$ or the
output $\aoutput{\msg}$ of a message .
A message specifies the endpoints $\ch_1$ and $\ch_2$ of communication
and carries a value .
An endpoint is either a host , the adversary , or the external environment
Values are drawn from an arbitrary set !, which we assume contains
at least $\vfalse$.
We define $\actor{\action}$ as the host performing :
the sender performs output actions and the receiver performs input actions.
Internal steps are represented as self-communication $\aglobalinternal{\h}$,
which identifies a host making progress without requiring a new syntactic

Configurations and Parallel Composition

_1 ∥…∥_n

∀i _i  _i'

_1 ∥…∥_n

_1' ∥…∥_n'

_i  _i'

∀j ≠i _j  _j'

_1 ∥…∥_n

_1' ∥…∥_n'

Syntax and semantics of configurations.

A configuration, , is the parallel composition of a finite set of
processes $\process_i$, which are arbitrary LTSs.
Following prior work <cit.>, processes must be input-total:
for every state $\process$ and input message $\ainput{\msg}$,
there exists a state $\process'$ such that
$\process \stepsto{\ainput{\msg}} \process'$.
<Ref> gives the semantics of configurations.
A configuration steps with an input $\ainput{\msg}$ if all processes
in do, and steps with an output $\aoutput{\msg}$ if one of the
processes outputs , and the rest input .

As with processes, an adversary or is an arbitrary LTS.
The rules for running an adversary in parallel with a configuration
are the same as in <ref>.
In contrast to processes, adversaries are not input-total,
which enables adversaries to control scheduling:
to schedule an endpoint $\ch_1$, refuses to step with actions of the form
$\aglobalreceive{\ch_1'}{\ch_2}{\msg}$ where $\ch_1' \neq \ch_1$,
but accepts actions $\aglobalreceive{\ch_1}{\ch_2}{\msg}$.

Due to the definition of parallel composition,
a copy of every message from the configuration and the environment is delivered
to the adversary;
and any output of the adversary is delivered to the configuration and the

However, the adversary can only read a message if at least one endpoint is
dishonest, and can only forge messages from malicious hosts.

For all :

* If \( \ch_1 \) and \( \ch_2 \) are honest,
\( \adv \stepsto{\aglobalreceive{\ch_1}{\ch_2}{\val_1}} \adv' \)
if and only if
\( \adv \stepsto{\aglobalreceive{\ch_1}{\ch_2}{\val_2}} \adv' \)
for all \( \val_1 \) and \( \val_2 \).

* If
\( \adv \stepsto{\aglobalsend{\ch_1}{\ch_2}{\val}} \),
then either \( \ch_1 = \advprot \) or \( \ch_1 \) is malicious.

To match UC, the adversary must resolve all nondeterminism,
so that $\adv \parallel \config$ is deterministic.
We ensure determinism with the following restrictions.

* Configurations and adversaries are internally deterministic:
\( \process \stepsto{\action} \process_1 \)
\( \process \stepsto{\action} \process_2 \),
\( \process_1 = \process_2 \).

* Adversaries are output deterministic:
\( \adv \stepsto{\aoutput{\msg_1}} \)
\( \adv \stepsto{\aoutput{\msg_2}} \),
\( \msg_1 = \msg_2 \).

* Configurations are output deterministic per channel:
\( \process \stepsto{\aoutput{\msg_1}} \),
\( \process \stepsto{\aoutput{\msg_2}} \),
\( \actor{\aoutput{\msg_1}} = \actor{\aoutput{\msg_2}} \),
\( \msg_1 = \msg_2 \).

* Adversaries are channel selective:
\( \process \stepsto{\ainput{\msg_1}} \)
\( \process \stepsto{\ainput{\msg_2}} \),
\( \actor{\ainput{\msg_1}} = \actor{\ainput{\msg_2}} \).

Simulation determines when a configuration $\config_2$ securely realizes
configuration $\config_1$:
that is, if every adversary interacting with
$\config_2$ can be simulated by another adversary (with the same
interface) running against $\config_1$ <cit.>.
The latter adversary is called a simulator.

\( \config_1 \) is simulated by \( \config_2 \),
written \( \config_1 \simulatedBy \config_2 \),
when the two systems are indistinguishable to
any external environment:

\[
\forall \adv \centerdot
\exists \simulator \centerdot
\envtraces{\simulator \parallel \config_1}
\envtraces{\adv \parallel \config_2}
\]

Here, \( \envtraces{\config} \) is the set of traces of but
containing only the actions that communicate with the environment.
Given trace
$\tr = \action_1, \dots, \action_n$, we have
\(
\envtraces{\config}
\setdef{\restrict{\tr}{\envprot}}{\config \stepsto{\tr}}
\),
where restriction $\restrict{\tr}{\envprot}$ removes all actions in where
neither the source nor the destination is .

Our definition of simulation guarantees perfect
(i.e., informationtheoretic) security.
In <ref>, we discuss how to transfer our results to the SUC
framework, which is based on computational security.

§ SPECIFYING SECURITY POLICIES

To succinctly capture both security policies and the adversary's power,
we use a label model that can describe confidentiality
and integrity simultaneously <cit.>.

A security label $\lbl \in \lbl!$ is a pair of the form $\pair{\cc}{\ic}$
where and are elements of an arbitrary bounded distributive lattice !.
Here, describes confidentiality and describes integrity.
Elements of ! are called principals.
Principals can be thought of as negation-free boolean formulas over
a set $\set{\palice, \pbob, \pchuck, \dots}$ of atomic principals.

The acts-for relation ($\actsfor$) orders principals by authority,
and coincides with logical implication: for example,
$\p \wedge \q \actsfor \p$ and $\q \actsfor \p \vee \q$.
The most powerful principal is $\strongest$ and the least powerful,
$\weakest$, so we have $\strongest \actsfor \p \actsfor \weakest$
for any principal $\p$.

We lift $\wedge$, $\vee$, and $\actsfor$ to labels in the obvious pointwise manner.
Whenever appropriate, we write $\p$ for the security label $\pair{\p}{\p}$.
Confidentiality and integrity projections
$\confidentiality{\lbl}$ and $\integrity{\lbl}$
completely weaken the other component of a label:
\confidentiality{\pair{\cc}{\ic}}
\pair{\cc}{\weakest}
\integrity{\pair{\cc}{\ic}}
\pair{\weakest}{\ic}

As in FLAM <cit.>,
the authority ordering on principals defines secure information flow.
Flow policies become more restrictive as they become
more secret and less trusted:

\begin{align*}
\pair{\cc_1}{\ic_1}
\flowsto
\pair{\cc_2}{\ic_2}
\cc_2 \actsfor \cc_1
\text{ and }
\ic_1 \actsfor \ic_2
\\
\pair{\cc_1}{\ic_1}
\join
\pair{\cc_2}{\ic_2}
\pair{\cc_1 \wedge \cc_2}{\ic_1 \vee \ic_2}
\\
\pair{\cc_1}{\ic_1}
\meet
\pair{\cc_2}{\ic_2}
\pair{\cc_1 \vee \cc_2}{\ic_1 \wedge \ic_2}
\end{align*}

The least restrictive information flow policy is $\ifbottom$ (“public
trusted”), describing information that can be used anywhere, while
the most restrictive is $\iftop$ (“secret untrusted”).

Formally, an attack is specified by picking two sets of principals:
public principals $\p* \subseteq \p!$ and
untrusted principals $\q* \subseteq \p!$.
Some common-sense conditions must hold on the sets * and * <cit.>.
We state the conditions for * but they apply equally to *.
The adversary always controls the weakest principal,
but never controls the strongest:
$\weakest \in \p*$ and $\strongest \not\in \p*$.
If the adversary controls a principal, then it controls all weaker principals:
if $\p \in \p*$ and $\p \actsfor \q$, then $\q \in \p*$.
Attacking principals may collude:
if $\p, \q \in \p*$, then $\p \wedge \q \in \p*$.
Combining secret/trusted principals leads to secret/trusted principals:
if $\p \vee \q \in \p*$, then either $\p \in \p*$ or $\q \in \p*$.

Together, these conditions imply that * and * are sensible truth assignments
to elements !: sensible in the sense that they play nicely with $\wedge$ and
$\vee$.[For those familiar with order theory,
* and * must be prime filters of !.]

We can derive the set of public/secret and trusted/untrusted labels
from * and *:

= ! ∖

= ! ∖.

Additionally, we require that attacks compromise at least as much confidentiality
as integrity.

Attack \( \pair{\p*}{\q*} \) is valid if all untrusted principals are public:
\( \q* \subseteq \p* \).

§.§ Authority of Hosts

Protocol synthesis places computations on hosts that have enough authority
to securely execute them.
The authority of each host is captured with a label $\labelof{\h}$ <cit.>.
For our example, we take $\labelof{\alice} = \iflabel{A}$
and $\labelof{\bob} = \iflabel{B}$.
Following an insight from Viaduct <cit.>,
idealized hosts like $\MPCalicebob$ have a derived label that
conservatively approximates the
security guarantees of the cryptographic mechanism.
For maliciously secure MPC, a reasonable label is
\(
\labelof{\MPCalicebob}
\labelof{\alice} \wedge \labelof{\bob}
\iflabel{A \wedge B}
\),
meaning that may view secrets of and ,
and also has enough integrity to compute values for them.

§.§ Capturing Attacks with Labels

The power of the adversary is determined by partitioning labels ! across
the two axes: public/secret and trusted/untrusted;
we denote these sets as /and /, respectively.
We only consider sets that form valid attacks <cit.>.
Intuitively, a valid attack requires that all untrusted labels are public, so
that the adversary cannot modify secret data;
we define valid attacks formally in sec:ifc-details.
The rest of our development is parameterized over a valid partitioning of labels.

Recalling the threat model from <ref>,
an honest host has a secret, trusted label ($\honest{\h}$);
a semi-honest host has a public, trusted label ($\semihonest{\h}$);
and a malicious host has a public, untrusted label ($\malicious{\h}$).
A host with a secret, untrusted label does not make any sense:
an untrusted host is fully controlled by the adversary,
so it cannot hide information from the adversary.
We rule out such corruptions by requiring all host labels to be
uncompromised <cit.>.
A valid partitioning never classifies an uncompromised label as secret and

\( \lbl = \pair{\cc}{\ic} \) is uncompromised,
written \( \uncompromised{\lbl} \),
if it is at least as trusted as it is secret:
\( \ic \actsfor \cc \).

Under a valid attack, if \( \uncompromised{\lbl} \),
then we have \( \lbl \not\in \secret \cap \untrusted \).

\( \pair{\p*}{\q*} \) be a valid attack
\( \lbl = \pair{\p}{\q} \).
\( \uncompromised{\lbl} \)
\( \lbl \in \untrusted \).
By definition, we have \( \q \in \q* \).
Unfolding \( \uncompromised{\lbl} \),
we have \( \q \actsfor \p \), and since * is upward closed,
we have \( \p \in \q* \).
Finally, \( \p \in \q* \subseteq \p* \),
so \( \lbl \in \public \).

§ PROTOCOL SYNTHESIS

The first program transformation, protocol synthesis, takes a sequential
source program to a choreography.

§.§ Source Language

[Atomic Expr.]

[Buffers]! ×! →!^*

Syntax of the source language.

<Ref> gives the syntax of source programs.
The language supports an abstract set of operators over values.
We distinguish pure, atomic expressions from expressions that may have side effects.
The expression marks locations where
private data is explicitly allowed to flow to public data.
Similarly, marks where untrustworthy data may
influence trusted data.
The /expressions allow programs to interact with the external
environment <cit.>.

Statement $\sleth{\x}{\h}{\e}{\s}$ performs the local
computation at host , binds the result to variable ,
and continues as .
In source programs, is only relevant for and expressions:
we write
\(\dlethhead{\x}{\h}{\einput{\h}}\)
\(\dlethhead{\x}{\h}{\eoutput{\aexp}{\h}}\)
in contrast to our example in <ref>,
where we write
\(\dlethead{\x}{\einputh{\h}}\)
\(\dlethead{\x}{\eoutputh{\aexp}{\h}}\).
For all other expressions, is ,
a single fully trusted host.
Representing source programs with host annotations
allows smoothly extending the language later on.

A source-program configuration is a logically centralized process
The component ! indicates the process acts for all hosts.
The second component, , is a buffer mapping pairs of endpoints to
first-in-first-out queues of values.
Processes buffer input so that output on other processes
(the adversary and the environment) is nonblocking.

§.§ Choreography Language

* ⊆!

Syntax of choreographies as an extension to source syntax
The $\ksend/\kreceive$ expressions are only relevant for the
security proof.

Choreographies are centralized representations of distributed computations.
Unlike source programs, they make explicit the location of
computations, storage, and communication.

<Ref> gives the syntax of choreographies,
which we present as an extension of the source syntax.
Host annotations on and statements are no longer restricted to
and can be any host $\h \in \h!$.
The global communication statement $\smove{\h_1}{\aexp}{\h_2}{\x}{\s}$
represents host $\h_1$ sending the value of to $\h_2$,
which stores it in variable .
The selection statement $\sselect{\h_1}{\val}{\h_2}{\s}$
communicates control flow decisions,
and is used to establish knowledge of choice <cit.>.
We extend expressions with and ,
however, the compiler never generates choreographies with these expressions;
they are only used in proofs to model malicious corruption

As for source programs, configurations are single
processes $\proc{\h*}{\buffer}{\s}$, but * may be a strict subset of
! and does not contain the ideal process .

§.§ Operational Semantics of Choreographies

! '

! '

Select ideal, real, and concurrent stepping rules.

Following <ref>, we give operational semantics to programs
using labeled transition systems.
Since choreographies strictly extend the syntax of source programs,
it suffices to define a semantics for choreographies.

Following <ref>, we define two transition relations:
ideal stepping $\idealstepsto{}$ gives meaning to source programs
and to idealized choreographies (an intermediate language for our simulation proof),
and real stepping $\realstepsto{}$ gives meaning to choreographies
and distributed programs.
Additionally, we lift ideal and real stepping to concurrent versions,
written $\idealstepsto!{}$ and $\realstepsto!{}$,
to capture the concurrent semantics of choreographies.
<Ref> gives a selection of key rules;
we defer full definitions to sec:operational-semantics-details.

§.§.§ Ideal Semantics

We write $\h \says \e \idealstepsto{\action} \val$ to mean expression evaluates
to value at host with action .
We assume operators are total;
partial operators (like division) can be made total using defaults.
Formally, we give meaning to operator application assuming a denotation function
$\evaluate : \f! \times \val!^{*} \to \val!$.
We model and expressions as interactions with
the adversary endpoint .
When a value is declassified from a secret label to a public one,
the program outputs the value to .
Dually, when a value is endorsed from an untrusted label to a trusted one,
the program takes input from , and uses that value instead.
When the confidentiality/integrity of the value does not change,
these expressions act as the identity function and take internal steps.
The /expressions communicate with the environment endpoint ,
except on malicious hosts;
there, they step internally and always return .
In source programs and idealized choreographies,
/expressions only communicate with malicious hosts;
we suppress them (they take internal steps and always return )
to give less power to the adversary in the ideal setting.

For statements,
we write $\s \idealstepsto{\action} \s'$ to mean statement steps to $\s'$ with action .
Statement stepping rules are as expected:
statements step using substitution,
statements pick a branch based on their conditional,
and communication and selection statements step internally,
naming the “sending host” as the host performing the action.

§.§.§ Real Semantics

Real stepping rules modify ideal stepping rules.
The /expressions always step internally instead of
communicating with .
The /expressions communicate a value with the specified host.
Finally, communication and selection statements step with a visible action
instead of internally.

§.§.§ Concurrent Lifting for Choreographies

Concurrent stepping rules, written $\s \polystepsto!{\action} \s'$,
lift an underlying statement-stepping judgment
($\idealstepsto{}$ or $\realstepsto{}$).
Concurrent stepping allows choreographies to step statements at different hosts
out of program order as long as there are no dependencies between the hosts,
and is the standard way choreographies model the behavior of a
distributed system <cit.>.
The key rule allows skipping over statements to step a statement
in the middle of a program.
This rule requires the actor of the performed action to be different from the
hosts of the statements being skipped over,
matching the behavior of target programs where code running on a single
host is single-threaded.

Synchronous vs. Asynchronous Choreographies

When skipping over statements,
requiring only the actor to be missing from the context
leads to an asynchronous semantics <cit.>.
In a synchronous setting, the side condition would require both
endpoints to be missing:
$\hosts{\action} \cap \hosts{\ectx} = \emptyset$.
Consider the following program:

is waiting on an input,
so is not ready to receive from .
In a synchronous setting, these statements must execute in program order
since can only send if is ready to receive.
In an asynchronous setting, sends are nonblocking, so the second statement
can execute first.

§.§.§ Processes

A buffer behaves as a FIFO queue for each channel:
it can input a message by appending the received value at the end of the
corresponding queue,
and can output the value at the beginning of any queue.
Buffers guarantee in-order delivery within a single channel $\ch_1 \ch_2$,
but messages across different channels may be reordered.
A process forwards its input to its buffer if the message is
addressed to a relevant host; otherwise, discards the message.
A process takes an internal step when its buffer delivers a message to its statement,
and an output step when its statement outputs.

§.§ Compiling to Choreographies

= '

\[
\io{\e}
(\e = \einput{\h})
\vee
(\exists \aexp \centerdot \e = \eoutput{\aexp}{\h})
\]

Canonical source program from a choreography.

Instead of committing to a specific algorithm,
we give validity criteria for the output of protocol synthesis,
which generalizes our results to and beyond prior
work <cit.>.
Because a source program can be realized as many different choreographies,
protocol synthesis cannot be modeled as a function from source programs to
Instead, we capture a valid protocol synthesis as a
mapping from choreographies to source programs.

Choreography \( \s' \) is a valid result of protocol synthesis on
source program \( \s \) if
\( \source{\s'} = \s \),
\( \ssecure[\emptylist]{\s'} \),
\( \ssynched[\sctx]{\s'} \)
for some .

<Ref> defines the function $\source{\cdot}$,
which maps a choreography to its canonical source program
by removing communication and selection statements
and replacing all host annotations with (except those associated with and ).
The judgment $\ssecure{\s}$ denotes that choreography has secure information
flows, and $\ssynched{\s}$ denotes is well-synchronized.
We define these judgments next.

§.§.§ Information-Flow Type System

∀i _i

_1 _2

Information-flow typing rules for expressions and
statements in choreographies.

First, we give a type system for choreographies based on information-flow
control <cit.> which validates that
hosts have enough authority to execute their assigned statements.

<Ref> gives the typing rules.
A label context maps a variable to its host and label, as a
set of bindings $\csing{\x}{\h}{\lbl}$.
The judgment $\esecure{\e}{\lbl}$,
means that at host has label in the context .
<Ref> ensures hosts only use variables they own.
<Ref> enforce nonmalleable information
flow control (NMIFC) <cit.> by requiring source and target labels
to be uncompromised <cit.>.
NMIFC requires declassified data to be trusted, enforcing robust declassification,
and endorsed data to be public, enforcing transparent endorsement.
These restrictions prevent the adversary from exploiting downgrades.
Enforcing NMIFC is crucial for our simulation result, which we discuss in

In choreographies, /expressions model communication with
malicious hosts.
Choreographies exclude code for malicious hosts, which
exhibit arbitrary behavior;
thus, labels for /expressions must be approximated.

<Ref> ensures data coming from malicious hosts is considered
untrusted; it treats the data as fully public since we do not care about
preserving the confidentiality of malicious hosts.
<Ref> ensures secret data is not sent to malicious hosts;
it ignores integrity since malicious hosts are untrusted.

Statement checking rules have the form $\ssecure{\s}$;
they are largely standard <cit.>,
but do not track program counter labels since we require programs to only
branch on public, trusted values.
<Ref> check that the host storing a variable has
enough authority to do so.

This is the key condition governing secure host selection and prevents,
for example, 's secret data being placed on ,
or high-integrity data being placed on an untrusted host.
<Ref> ensures that if host $\h_1$ informs $\h_2$ of a
branch being taken, then $\h_1$ has at least as much integrity as $\h_2$.
So malicious hosts cannot influence control flow on nonmalicious hosts.
Finally, <ref> requires control flow to be public and trusted.

§.§.§ Synchronization Checking

= '
_1_2 = '

∀' (', ) ' ∨

, *

*, _2
(*, _2) ∧((*, _1) ∨_2)

Checking that a concurrent choreography has sequential behavior.

Next, we define a novel synchronization judgment, $\ssynched{\s}$,
which guarantees that all external actions in $\s$ happen in sequential
program order.
For example, any $\kendorse$ statement that happens after a $\kdeclassify$
must logically depend on the $\kdeclassify$. Since these statements
may be run on different hosts, the $\kdeclassify$ could happen before the
$\kendorse$, violating program order. To prevent this, we require that
the host running the $\kendorse$ synchronizes with the host running
the $\kdeclassify$.

Synchronization becomes more complex with corruption.
For example, if and synchronize through another host ($\alice \communicate \h \communicate \bob$)
and is malicious, might give the go-ahead before confirming with
We use integrity labels to ensure synchronization even under corruption.

<Ref> defines the synchronization-checking
judgment $\ssynched{\s}$.
Intuitively, a choreography is well-synchronized when for any
external (input or output) expression ,
a high-integrity communication path exists from to all
output expressions following in the program order.[Input expressions are and ;
output expressions are and .]
Integrity of a communication path
$\h_1 \communicate \cdots \communicate \h_n$
is determined by the hosts in the path:

\[
\labelof{\h_1 \communicate \cdots \communicate \h_n}
\integrity{\labelof{\h_1}}
\vee \dots \vee
\integrity{\labelof{\h_n}}
\]

Hosts can be malicious, so each host on the path weakens integrity,
which is captured by disjunction ($\vee$).
Multiple paths between the same hosts increase integrity,
which we capture by taking the conjunction ($\wedge$) of path labels:

\[
\labelof{\paths{\h_1}{\h_2}}
\bigwedge_{\cpath \in \paths{\h_1}{\h_2}}{
\labelof{\cpath}
\]

We track the integrity of paths using the context , which maps pairs of hosts
$\sctx(\h_1, \h_2)$ to the integrity label $\labelof{\paths{\h_1}{\h_2}}$.

<Ref> checks a statement that executes an external
expression on .
The continuation is checked under a context where the label of all paths
from to any other host are set to $\weakest$
(this corresponds to removing the paths),
since these hosts now need to synchronize with .
Also, if is an output expression, must be synchronized
with all hosts through the following condition, which ensures that if
neither $\h_1$ nor $\h_2$ is malicious, a communication path exists from
$\h_1$ to $\h_2$ that could not have been influenced by the adversary:

\begin{equation}
\label{def:is-synched}
\labelof{\paths{\h_1}{\h_2}}
\flowsto
\labelof{\h_1} \vee \labelof{\h_2}
\end{equation}

<Ref> update using
The function captures that a path from some $\h$ to $\h_1$ implies
there is a path from $\h$ to $\h_2$ that goes through $\h_1$.
Further, all existing paths are still valid.

§.§ Modeling Malicious Corruption

= '

_1, _2

_1, _2

= '
* =

Modeling malicious corruption.
We write \( \istrusted{\h} \) for \( \nonmalicious{\h} \).

Malicious hosts are fully controlled by the adversary.
Following UC <cit.>, we entirely remove processes that correspond to
malicious hosts in hybrid distributed programs,
and allow the adversary to forge arbitrary messages in their stead.
This is reflected in choreographies by rewriting them to elide statements
that involve malicious hosts.

<Ref> defines the corruption $\corrupt{\s}$
of a choreography .
The operation considers each statement in turn.
If all hosts involved in a statement are nonmalicious,
the statement stays as is.
If all hosts involved in a statement are malicious,
the statement is removed entirely.
Otherwise, only some involved hosts are malicious,
and we rewrite the statement.
Communication statements become either a or a ,
depending on whether the sending or the receiving host is nonmalicious.
Selection statements are similar,
except we cannot have a malicious sending host and a nonmalicious receiving
host (<ref>).
Similarly, statements cannot be at a malicious host since we require
trusted control flow (<ref>).

Ideal stepping rules for expressions and statements.

= (, n)

i =
if  ≠ then

Real stepping rules for expressions and statements.
These override the rules in <ref>.

_1_2↦, …

Concurrent lifting of ideal/real stepping rules.

! '

! '

_1 ! _1'

_2 ! _2'

= *

[Evaluation Contexts]

_1, _2

_1, _2

Ideal, real, and concurrent stepping rules for expressions
and statements.

_1 _2*
_1 _2*

_1 _2*
_1 _2*

_1 ∉*

_2 ∈*

_1 ∈*
∨_2 ∉*

_1_2 '

_1_2 '

Stepping rules for buffers and processes.

<Ref> gives the full set ideal, real, and concurrent
stepping rules for expressions and statements.
<Ref> gives buffer and process stepping rules.
Concurrent stepping rules refer to evaluation contexts—statements
containing a single hole—and the function $\hosts{\cdot}$,
which returns the set of hosts that appear in an evaluation context.
<Ref> allows skipping over , communication, and selection
statements to step a statement in the middle of a program.
<Ref> allows stepping the body of an statement without
resolving the conditional as long as both branches step with the same action.
Both rules require the actor of the performed action to be different from the
hosts of the statements being skipped over,
matching the behavior of target programs where code running on a single
host is single-threaded.

§ PROPERTIES OF THE CHOREOGRAPHY LANGUAGE

§.§ Typing and Synchronization

Typing ensures robust declassification and transparent endorsement,
which guarantee that declassified values are always trusted,
and that endorsed values are always public.

\(\esecure{\edeclassify{\aexp}{\fromlbl}{\tolbl}}{\lbl}\),
\(\issecret{\fromlbl}\),
\(\ispublic{\tolbl}\),
\(\istrusted{\fromlbl}\).

\(\esecure{\eendorse{\aexp}{\fromlbl}{\tolbl}}{\lbl}\),
\(\isuntrusted{\fromlbl}\),
\(\istrusted{\tolbl}\),
\(\ispublic{\fromlbl}\).

Typing has standard properties.

* \( \ctx_1 \flowsto \ctx_2 \)
\( (\csing{\x}{\h}{\lbl_2}) \in \ctx_2 \)
\( (\csing{\x}{\h}{\lbl_1}) \in \ctx_1 \)
for some \( \lbl_1 \) such that
\( \lbl_1 \flowsto \lbl_2 \).

* \( \sctx_1 \flowsto \sctx_2 \)
\( \sctx_1(\h_1 h_2) \flowsto \sctx_2(h_1 h_2) \)
for all \( h_1, \h_2 \in \h* \).

We have

* If
\( \esecure[\ctx]{\e}{\lbl} \),
\( \ctx' \flowsto \ctx \),
\( \lbl \flowsto \lbl' \),
\( \esecure[\ctx']{\e}{\lbl'} \).

* If
\( \ssecure[\ctx]{\s} \)
\( \ctx' \flowsto \ctx \),
\( \ssecure[\ctx']{\s} \).

* If
\( \ssynched[\sctx]{\s} \)
\( \sctx' \flowsto \sctx \),
\( \ssynched[\ctx']{\s} \).

Substitution preserves typing:

* If
\( \esecure[(\ctx \munion \csing{\x}{\h'}{\lbl'})]{\e}{\lbl} \),
\( \esecure{\subst{\x}{\val}{\e}}{\lbl} \).

* If
\( \ssecure[(\ctx \munion \csing{\x}{\h}{\lbl})]{\s} \),
\( \ssecure[\ctx]{\subst{\x}{\val}{\s}} \).

A well-typed program remains well typed under execution and all corruption.

\( \ssecure{\s} \)
\( \s \stepsto{\action} \s' \),
\( \ssecure{\s'} \).

\( \ssecure{\s} \),
\( \ssecure{\corrupt{\s}} \).

A well-synchronized program remains well synchronized under execution and
all corruption.

\( \ssynched{\s} \)
\( \s \stepsto{\action} \s' \),
\( \ssynched{\s'} \).

\( \ssynched{\s} \),
\( \ssynched{\corrupt{\s}} \).

A host can only output if it is synchronized with all previous external actions.

\( \ssynched[\sctx]{\s} \)
\( \s \stepsto{\aoutput{\msg}} \)
with \( \msg \) external, then
\( \hissynched[\sctx]{\h} \).

§.§ Operational Semantics

Below, we write $\stepsto{}$ to stand for any of
$\idealstepsto{}$, $\realstepsto{}$, $\idealstepsto!{}$, or $\realstepsto!{}$.

Processes never refuse input.

For all \( \process \) and \( \msg \),
there exists \( \process' \) such that
\( \process \stepsto{\ainput{\msg}} \process' \).

The stepping judgments are nondeterministic since inputs are externally
controlled (different input values lead to different states),
and, for concurrent judgments,
outputs and internal actions are independent across hosts.
However, processes are fully deterministic when the action is fixed.

\( \process \stepsto{\action} \process_1 \)
\( \process \stepsto{\action} \process_2 \),
\( \process_1 = \process_2 \).

\( \process \stepsto{\aoutput{\msg_1}} \process_1 \),
\( \process \stepsto{\aoutput{\msg_2}} \process_2 \),
\( \actor{\aoutput{\msg_1}} = \actor{\aoutput{\msg_2}} \),
\( \msg_1 = \msg_2 \).

These results lift to configurations as long as the configuration does
not contain duplicate hosts.

§ CORRECTNESS OF PROTOCOL SYNTHESIS

node distance=,
every node/.style=align=center,
program/.style=draw, rounded corners, text width=8.5em, minimum height=8ex,
transformation/.style=->, >=stealth', rounded corners=0.5mm,
[program] (1)
Sequential Source
$\source{\process}$, $\idealstepsto{}$;
[simulation] (12) [right=of 1]
[program] (2) [right=of 12]
Sequential Choreography
$\corrupt{\process}$, $\idealstepsto{}$;
[simulation] (23) [right=of 2]
[program] (3) [right=of 23]
Ideal Choreography
$\corrupt{\process}$, $\idealstepsto!{}$;
[simulation] (34) [right=of 3]
[program] (4) [right=of 34]
$\corrupt{\process}$, $\realstepsto!{}$;

– ++(0, )
-| node [pos=0.25, above] Protocol Synthesis
(<ref>) (4.north);

Intermediate simulation steps for proving the correctness of protocol

We prove the correctness of protocol synthesis by demonstrating
a simulation between source programs and their corresponding choreographies.
For $\process = \proc{\h*}{\buffer}{\s}$,
we write $\ssecure{\process}$ and $\ssynched{\process}$ if
$\ssecure{\s}$ and $\ssynched{\s}$, respectively,
and define $\source{\process} = \proc{\h*}{\buffer}{\source{\s}}$.

\( \ssecure[\emptylist]{\process} \),
\( \ssynched[\sctx]{\process} \) for some \( \sctx \),
\(
\using{\source{\process}}{\idealstepsto{}}
\simulatedBy
\using{\corrupt{\process}}{\realstepsto{}}
\).

We prove <ref> through a series of intermediate
simulations, following <ref> from left to right.
First, in <ref>,
we show idealized, sequential choreographies simulate their canonical source
Then, we show in <ref> that our synchronization
judgment ensures all externally visible actions happen in program order.
Finally, in <ref>, we move from
the ideal semantics $\idealstepsto!{}$ to the real semantics $\realstepsto!{}$.

For each simulation, we define a simulator that emulates the adversary
“in its head”.
We ensure that the emulated adversary's view is the same as the real adversary
even though the simulator only has access to public information.
Concretely, we establish a (weak) bisimulation relation <cit.>
between the ideal world (simulator running against ideal configuration)
and the real world (adversary running against real configuration).

§.§ Correctness of Host Selection

we show that the original source program is simulated by the sequential

\( \ssecure[\emptylist]{\process} \),
\(
\using{\source{\process}}{\idealstepsto{}}
\simulatedBy
\using{\corrupt{\process}}{\idealstepsto{}}
\).

This is shown via two simpler simulations.
First, we add host annotations and explicit communication to the source program:

\( \ssecure[\emptylist]{\process} \),
\(
\using{\source{\process}}{\idealstepsto{}}
\simulatedBy
\using{\process}{\idealstepsto{}}
\).

Statements removed by $\source{\cdot}$ only produce internal actions,
which the simulator can recreate.
Host annotations affect program behavior only by changing the source
and destination of internal actions and actions generated by
the simulator must recover the original host names before forwarding messages
from/to the adversary.

The simulator maintains a public view of and runs the
adversary against this view.
When the adversary steps , the simulator steps $\source{\process}$
only if the statement is preserved by $\source{\cdot}$; it does nothing
To handle ,
whenever the simulator receives a message of the form
the simulator inspects its copy of to determine the sending
host , and sends $\mglobal{\h}{\advprot}{\val}$ to the adversary instead.
Similarly, to handle ,
the simulator replaces $\h$ with $\idealprot$ in messages
$\mglobal{\advprot}{\h}{\val}$ from the adversary.

Second, we add corruption, obtaining a choreography which steps sequentially:

\( \ssecure[\emptylist]{\process} \),
\(
\using{\process}{\idealstepsto{}}
\simulatedBy
\using{\corrupt{\process}}{\idealstepsto{}}
\).

Corruption only removes statements at malicious hosts,
however, these statements only generate internal actions:
/expressions always step internally using ideal rules,
and typing ensures /expressions step internally.
This means $\corrupt{\process}$ and $\process$ have the same external behavior,
except $\process$ takes extra internal steps.
The simulator follows the control flow and acts like the adversary,
but whenever the adversary schedules $\corrupt{\process}$,
the simulator schedules $\process$ multiple times until the head statement
is at a nonmalicious host; then, it schedules $\process$ again.

A small caveat: in $\corrupt{\process}$, all data from
malicious hosts is explicitly replaced with ,
whereas malicious hosts may store arbitrary data in $\process$.
Since data from malicious hosts is untrusted, our type system ensures
this data does not influence trusted data,
which includes all output messages.
Formally, we only require and maintain that $\corrupt{\process}$
and $\process$ agree on trusted values.

§.§ Correctness of Sequentialization

Next, we show that if the choreography is wellsynchronized,
then the choreography stepping sequentially is simulated by itself
stepping concurrently:

\( \ssecure[\emptylist]{\process} \),
\( \ssynched[\sctx]{\process} \) for some \( \sctx \),
\(
\using{\corrupt{\process}}{\idealstepsto{}}
\simulatedBy
\using{\corrupt{\process}}{\idealstepsto!{}}
\).

The adversary, interacting with the concurrent version of the choreography,
can schedule a statement that is not next in program order.

If the statement produces an externally visible action,
the simulator must schedule the same statement.
Since the simulator interacts with the sequential version,
it must “unwind” the choreography by scheduling every statement leading up
to the desired statement.
Synchronization ensures unwinding does not fail due to a statement blocked on
input (or ), or a statement that performs a different visible
action (or ).

The concurrent and sequential choreographies necessarily fall out of sync
during simulation:
the adversary may schedule steps for the concurrent choreography that the
simulator cannot immediately match,
and the simulator might schedule steps for the sequential choreography while
unwinding, steps the adversary did not schedule.
Nevertheless, the two choreographies remain joinable:
they can reach a common choreography via only internal actions.
We prove choreographies are confluent <cit.>,
which ensures joinable processes remain joinable throughout the simulation.

The simulator maintains a public view of the concurrent process,
and runs the adversary against this view.
When the adversary schedules an output, the simulator schedules
the sequential process until it performs the same output;
the simulator does nothing for input and internal actions.
Well-synchronization guarantees the sequential program can perform the output.
The primary invariant, that the concurrent and sequential processes
remain joinable, is ensured by confluence.
See sec:correctness-of-sequentialization-details for details.

We write
\( \joinable{\process_1}{\process_2} \)
if there exist traces
\( \tr_1 \) and \( \tr_2 \)
containing only internal actions such that
\( \process_1 \idealstepsto!{\tr_1} \process \)
\( \process_2 \idealstepsto!{\tr_2} \process \)
for some \( \process \).

\[
\begin{tikzcd}
\process_1
\sarrow![dr, dotted, "{\tr_1}"]
\process_2
\sarrow![dl, dotted, "{\tr_2}"']
\\
& \exists \process
\end{tikzcd}
\]

We prove confluence through a diamond lemma,
which allows reordering independent actions.

Actions \( \action_1 \) and \( \action_2 \) are independent,
written \( \aindep{\action_1}{\action_2} \),
if one is an input while the other is an output,
or they are on different channels.
We write
\( \aindep{\tr_1}{\tr_2} \)
\( \aindep{\action_1}{\action_2} \)
for all \( \action_1 \in \tr_1 \) and \( \action_2 \in \tr_2 \).

\( \process \idealstepsto!{\tr_1} \process_1 \),
\( \process \idealstepsto!{\tr_2} \process_2 \),
\( \aindep{\tr_1}{\tr_2} \),
\( \process_1 \idealstepsto!{\tr_2} \process' \)
\( \process_2 \idealstepsto!{\tr_1} \process' \)
for some \( \process' \).

\[
\begin{tikzcd}
\process
\sarrow![dl, "{\tr_1}"']
\sarrow![dr, "{\tr_2}"]
\\
\process_1
\sarrow![dr, dotted, "{\tr_2}"']
& &
\process_2
\sarrow![dl, dotted, "{\tr_1}"]
\\
\exists \process'
\end{tikzcd}
\]

<Ref> does the heavy lifting when proving multiple
confluence results below, and requires quite a bit of work to show.
We first prove a diamond lemma for statements,
and then lift it to processes.

\( \s \idealstepsto{\action_1} \s_1 \),
\( \s \idealstepsto!{\action_2} \s_2 \),
\( \aindep{\action_1}{\action_2} \),
\( \s_1 \idealstepsto!{\action_2} \s' \)
\( \s_2 \idealstepsto{\action_1} \s' \)
for some \( \s' \).

By case analysis on
\( \s \idealstepsto!{\action_2} \s_2 \).

Contradicts \( \aindep{\action_1}{\action_2} \).

By case analysis on the evaluation context followed by inversion
on \( \s \idealstepsto{\action_1} \s_1 \).
The step for $\action_1$ involves only the head statement and
ignores all future statements, whereas the step for $\action_2$
ignores the head statement and involves only a statement in the future.
Thus, they can be performed in sequence in either order without changing
the end result.

The step for $\action_2$ steps both branches of the statement,
whereas the step for $\action_1$ selects a branch.
They can be performed in sequence in either order.

\( \s \idealstepsto!{\action_1} \s_1 \),
\( \s \idealstepsto!{\action_2} \s_2 \),
\( \aindep{\action_1}{\action_2} \),
\( \s_1 \idealstepsto!{\action_2} \s' \)
\( \s_2 \idealstepsto!{\action_1} \s' \)
for some \( \s' \).

By induction on the derivations of both stepping judgments.
If either is by <ref>,
we conclude by <ref>.
Otherwise, both steps ignore the head of using the same delay rule.
We appeal to the induction hypothesis,
and use the same delay rule to get a complete derivation.

We prove the statement when $\tr_1$ and $\tr_2$ are single actions;
the more general statement follows straightforwardly by induction on
$\tr_1$ followed by induction on $\tr_2$.

We proceed by case analysis on both stepping judgments.

* Both steps are input (<ref>).
Since $\aindep{\tr_1}{\tr_2}$,
the input messages are added at the end of two different queues.
Both actions can be performed in either order without affecting
the end result.

* One step is input, the other is by <ref>.
The input step adds a message to a queue,
while <ref> pops a message from a queue and feeds it
to the choreography.
The queues must be different since $\aindep{\tr_1}{\tr_2}$,
so the steps are independent.

* One step is input, the other is by <ref>.
The input step only affects the queue,
and the output step only affects the choreography,
so the steps are independent.

* Both steps are output (<ref>).
If either step is by <ref>,
then we use $\aindep{\tr_1}{\tr_2}$ as before to show we pull messages
out of different queues.
This allows reordering changes to the buffer.
<Ref> finishes the proof.

The proof of <ref> reasons generically about buffers,
and appeals to a diamond lemma for statements in a black-box manner.
This means we can generalize <ref> to arbitrary
(combinations of) stepping relations without extra work
as long as a diamond property for the same relations holds for statements.

Assume the diamond property holds for statements with stepping relations
\( \stepsto{}_1 \)
\( \stepsto{}_2 \).
\( \process \stepsto{\tr_1}_1 \process_1 \),
\( \process \stepsto{\tr_2}_2 \process_2 \),
\( \aindep{\tr_1}{\tr_2} \),
\( \process_1 \stepsto{\tr_2}_2 \process' \)
\( \process_2 \stepsto{\tr_1}_1 \process' \)
for some \( \process' \).

Same as the proof of <ref>.

Processes remain joinable after taking internal or matching steps.

\( \joinable{\process_1}{\process_2} \)
\( \process_1 \idealstepsto!{\action} \process_1' \)
for \( \action \) internal,
\( \joinable{\process_1'}{\process_2} \).

\[
\begin{tikzcd}
\process_1
\sarrow![d, "{\action}"']
\sarrow![dr, "{\tr_1}"]
\process_2
\sarrow![dl, "{\tr_2}"']
\arrow[d, equal]
\\
\process_1'
\sarrow![dr, dotted, "{\tr_1'}"']
\process
\process_2
\sarrow![dl, dotted, "{\tr_2'}"]
\\
\exists \process'
\end{tikzcd}
\]

Since $\process_1$ and $\process_2$ are joinable,
there exist $\process$ and internal $\tr_1, \tr_2$ such that
\( \process_1 \idealstepsto!{\tr_1} \process \)
\( \process_2 \idealstepsto!{\tr_2} \process \).
We case on whether
\( \aindep{\action}{\tr_1} \).

\( \aindep{\action}{\tr_1} \)
<Ref> gives $\process'$ such that
\( \process_1' \idealstepsto!{\tr_1} \process' \)
\( \process \idealstepsto!{\action} \process' \).
Since $\action$ and $\tr_2$ are internal, so is $\tr_2 \append \action$.
\( \joinable{\process_1'}{\process_2} \)
through $\tr_1$ and $\tr_2 \append \action$.

\[
\begin{tikzcd}
\process_1
\sarrow![dl, "{\action}"']
\sarrow![dr, "{\tr_1}"]
\process_2
\sarrow![dl, "{\tr_2}"]
\\
\process_1'
\sarrow![dr, dotted, "{\tr_1}"']
\arrow[rr, phantom, "\text{\Cref{thm:diamond-process}}" description]
\process
\sarrow![dl, dotted, "{\action}"]
\\
\exists \process'
\end{tikzcd}
\]

\( \anindep{\action}{\tr_1} \)
Let $\action_1$ be the first action in $\tr_1$ such that
\( \anindep{\action}{\action_1} \), that is,
\( \tr_1 = \tr_1' \append \action_1 \append \tr_1'' \)
\( \aindep{\action}{\tr_1'} \).
We have,
\(
\process_1
\idealstepsto!{\tr_1'}
\process'
\idealstepsto!{\action_1}
\process''
\idealstepsto!{\tr_1''}
\process
\).
<Ref> gives $\process_1''$ such that
\( \process_1' \idealstepsto!{\tr_1'} \process_1'' \)
\( \process' \idealstepsto!{\action} \process_1'' \).
We now have
\( \process' \idealstepsto!{\action} \process_1'' \)
\( \process' \idealstepsto!{\action} \process'' \),
the stepping judgment is deterministic on dependent internal actions,
thus <ref> gives
\( \process_1'' = \process'' \).[
More specifically, $\action$ and $\action_1$ are internal actions,
which are represented as outputs.
\( \anindep{\action}{\action_1} \),
we have
\( \actor{\action} = \actor{\action_1} \),
so <ref> applies.
\( \joinable{\process_1'}{\process_2} \)
through $\tr_1' \append \tr_1''$ and $\tr_2$.

\[
\begin{tikzcd}
\process_1
\sarrow![dl, "{\action}"']
\sarrow![dr, "{\tr_1'}"]
\process_2
\sarrow![dddlll, "{\tr_2}"']
\\
\process_1'
\sarrow![dr, dotted, "{\tr_1'}"]
\arrow[rr, phantom, "\text{\Cref{thm:diamond-process}}" description]
\process'
\sarrow![dl, dotted, "{\action}"']
\sarrow![dr, "{\action_1}"]
\\
\exists \process_1''
\arrow[rr, equal, "\text{\Cref{thm:output-determinism}}"]
\process''
\sarrow![dr, "{\tr_1''}"]
& &
\\
& & & &
\process
\end{tikzcd}
\]

\( \joinable{\process_1}{\process_2} \),
\( \process_1 \idealstepsto!{\action} \process_1' \),
\( \process_2 \idealstepsto!{\action} \process_2' \),
\( \joinable{\process_1'}{\process_2'} \).

\[
\begin{tikzcd}
\process_1
\sarrow![d, "{\action}"']
\sarrow![dr, "{\tr_1}"]
\process_2
\sarrow![dl, "{\tr_2}"']
\sarrow![d, "{\action}"]
\\
\process_1'
\sarrow![dr, dotted, "{\tr_1'}"']
\process
\process_2'
\sarrow![dl, dotted, "{\tr_2'}"]
\\
\exists \process'
\end{tikzcd}
\]

Since $\process_1$ and $\process_2$ are joinable,
there exist $\process$ and internal $\tr_1, \tr_2$ such that
\( \process_1 \idealstepsto!{\tr_1} \process \)
\( \process_2 \idealstepsto!{\tr_2} \process \).
If $\action$ is internal, then the result follows by two applications of
\( \aindep{\action}{\tr_1} \)
\( \aindep{\action}{\tr_2} \).
The result follows from two applications of <ref>,
and one application of <ref>:

\[
\begin{tikzcd}
\process_1
\sarrow![dl, "{\action}"']
\sarrow![dr, "{\tr_1}"]
\process_2
\sarrow![dl, "{\tr_2}"']
\sarrow![dr, "{\action}"]
\\
\process_1'
\sarrow![dr, dotted, "{\tr_1}"']
\arrow[rr, phantom, "\text{\Cref{thm:diamond-process}}" description]
\process
\sarrow![dl, dotted, "{\action}"]
\sarrow![dr, dotted, "{\action}"']
\process_2'
\sarrow![dl, dotted, "{\tr_2}"]
\arrow[ll, phantom, "\text{\Cref{thm:diamond-process}}" description]
\\
\exists \process_1''
\arrow[rr, equal, "\text{\Cref{thm:internal-determinism}}"]
\exists \process_2''
\end{tikzcd}
\]

If a well-typed, well-synchronized program can take an output step concurrently,
then it can take the same step sequentially
(after taking the series of internal steps leading up to the output).
We write
$\process \idealstepsto*{\aoutput{\msg}} \process'$
$\process \idealstepsto{\tr \append \aoutput{\msg}} \process'$
for some internal .

\( \ssecure[\emptylist]{\process} \),
\( \ssynched{\process} \),
\( \process \idealstepsto!{\aoutput{\msg}} \)
for \( \msg \) external,
\( \process \idealstepsto*{\aoutput{\msg}} \).

By induction on the stepping relation.
If the step is by <ref>,
then $\process \idealstepsto{\aoutput{\msg}}$ and we are done.
Otherwise, it must be by <ref>.
We need to show that we can take a sequential internal step by casing on the
evaluation context $\ectx$.
Note that the top statement in must be internal,
otherwise we get a contradiction by <ref>.
Since $\process$ has no free variables, it can take an internal step.

\( \process_1 \idealstepsto!{\action_1} \process_2 \idealstepsto{\action_2} \),
then either
\( \process_1 \idealstepsto{\action_1} \process_2 \),
\( \process_1 \idealstepsto{\action_2} \)
\( \aindep{\action_1}{\action_2} \).

Assume the first step cannot be done sequentially
(otherwise we are done).
Then, the first step uses a delay rule (<ref>),
which ignores the head statement of $\process_1$.
The second step is sequential so it only depends on the head statement
of $\process_2$, which is the same as the head statement of $\process_1$,
thus, $\process_1$ can step with $\action_2$.
We get that
\( \aindep{\action_1}{\action_2} \)
from the side conditions on delay rules,
which require \( \actor{\action_1} \) to be different from
\( \actor{\action_2} \).

\( \process_1 \idealstepsto!{\action} \process_2 \idealstepsto*{\aoutput{\msg}} \)
for \( \action \) internal,
\( \process_1 \idealstepsto*{\aoutput{\msg}} \).

Unfolding the definition of $\idealstepsto*{}$ gives
\(
\process_2 \idealstepsto{\tr} \process_3 \idealstepsto{\aoutput{\msg}}
\)
for some $\tr$ and $\process_3$.
We proceed by induction on .
In either case, we are done if
\( \process_1 \idealstepsto{\action} \process_2 \),
so assume $\process_1$ cannot perform $\action$ sequentially.

$\tr = \emptylist$
We have
\( \process_1 \idealstepsto!{\action} \process_2 \idealstepsto{\aoutput{\msg}} \).
<Ref> gives
\( \process_1 \idealstepsto{\aoutput{\msg}} \),
and thus
\( \process_1 \idealstepsto*{\aoutput{\msg}} \).

$\tr = \action' \append \tr'$
We have
\(
\process_1
\idealstepsto!{\action}
\process_2
\idealstepsto{\action'}
\process_3
\idealstepsto{\tr'}
\process_4
\idealstepsto{\aoutput{\msg}}
\).
<Ref> gives
\( \process_1 \idealstepsto{\action'} \process_2' \)
for some $\process_2'$.
<Ref> with <ref>
then gives
\(
\process_1
\idealstepsto{\action'}
\process_2'
\idealstepsto!{\action}
\process_3'
\)
for some $\process_3'$,
and <ref> shows $\process_3' = \process_3$.
We use the induction hypothesis on
\(
\process_2'
\idealstepsto!{\action}
\process_3
\idealstepsto{\tr'}
\process_4
\idealstepsto{\aoutput{\msg}}
\)
to get
\(
\process_2'
\idealstepsto*{\aoutput{\msg}}
\),
and combined with
\(
\process_1
\idealstepsto{\action'}
\process_2'
\),
we get
\(
\process_1
\idealstepsto*{\aoutput{\msg}}
\).

Diagrammatically (we use tails to denote sequential steps):

\[
\begin{tikzcd}
\process_1
\sarrow![dl, "{\action}"']
\sarrow[dr, dotted, "{\action'}~\text{(\Cref{thm:concurrent-then-sequential})}"]
\\
\process_2
\sarrow[dl, "{\action'}"']
\sarrow[dr, "{\action'}"]
\arrow[rr, phantom, "\text{\Cref{thm:general-diamond-process}}" description]
\exists \process_2'
\sarrow![dl, dotted, "{\action}"']
\sarrow*[d, dotted, "{\aoutput{\msg}}~\text{(IH)}"]
\\
\process_3
\sarrow[d, "{\tr'}"']
\arrow[rr, equal, "\text{\Cref{thm:internal-determinism}}"]
\exists \process_3'
\phantom{\process_3''}
\\
\process_4
\sarrow[d, "{\aoutput{\msg}}"']
\\
\phantom{\process_5}
\end{tikzcd}
\]

If two processes are joinable and one of them can concurrently perform an
output action, then the other can perform the same action sequentially
(after unwinding).

Let \( \process_1 \) and \( \process_2 \) be such that
\( \joinable{\process_1}{\process_2} \),
\( \ssecure[\emptylist]{\process_2} \),
\( \ssynched{\process_2} \).
\( \process_1 \idealstepsto!{\aoutput{\msg}} \)
for \( \msg \) external,
\( \process_2 \idealstepsto*{\aoutput{\msg}} \).

Since $\process_1$ and $\process_2$ are joinable,
there exist $\process$ and internal $\tr_1, \tr_2$ such that
$\process_1 \idealstepsto!{\tr_1} \process$
$\process_2 \idealstepsto!{\tr_2} \process$.
Because $\msg$ is external and $\tr_1$ is internal,
we have $\aindep{\aoutput{\msg}}{\tr_1}$,
so <ref> gives
$\process \idealstepsto!{\aoutput{\msg}}$.
Now we have
\( \process_2 \idealstepsto!{\tr_2 \append \aoutput{\msg}} \),
and we want to show
\( \process_2 \idealstepsto*{\aoutput{\msg}} \).
We proceed by induction on $\tr_2$.
When $\tr_2$ is empty, <ref> completes the proof.
When $\tr_2 = \action \append \tr_2'$,
the induction hypothesis gives
\( \process_2 \idealstepsto!{\action} \process_2' \idealstepsto*{\aoutput{\msg}} \),
and <ref> gives the desired result.

The simulator maintains a public view of the concurrent process,
and runs the adversary against this view.
When the adversary schedules an output action, the simulator schedules
the sequential process until it performs the same output;
the simulator does nothing for input and internal actions.
<Ref> guarantees the sequential program can perform
the output.
The primary invariant, that the concurrent and sequential processes
remain joinable, is ensured by

More formally, we show UC simulation as follows.

The simulator has the form
\( \simof{\process_1'}{\process_2'} \)
where $\process_1'$ is the public view of the concurrent process,
and $\process_2'$ is the public view of the sequential process.
When the simulator receives an input from the environment
or a message from the sequential process,
it feeds the message to , $\process_1'$, and $\process_2'$.
When the adversary outputs a value
(for the environment or for an expression),
the simulator feeds it to $\process_1'$ and $\process_2'$,
and outputs the same value.
When the simulator receives an internal message from the sequential
process (which indicates the sequential process has taken a step),
it steps $\process_2'$.
The simulator only allows an output step for the sequential process
if $\process_1'$ can perform same output.

\(
\adv \parallel \process_1
\rel
\simof[\adv']{\process_1'}{\process_2'} \parallel \process_2
\)

\( \adv = \adv' \)

\( \process_1 \publiceq \process_1' \)

\( \process_2 \publiceq \process_2' \)

\( \joinable{\process_1}{\process_2} \)

\( \ssecure[\emptylist]{\process_2} \)
\( \ssynched{\process_2} \)
for some .

We claim $\rel$ is a weak bisimulation.

<Ref> ensure
<ref> is applicable,
which in turn ensures the external behavior of both systems
is the same.

<Ref> is preserved since $\process_1'$ is an
accurate public view of $\process_1$ (<ref>).
<Ref> are preserved
since messages from are sufficient to maintain a
public view.
ensure <ref> is preserved.
ensure <ref> is preserved.

§.§ Correctness of Ideal Execution

Finally, we move from a concurrent choreography stepping with ideal rules
to a concurrent choreography stepping with real rules:

\( \ssecure[\emptylist]{\process} \),
\(
\using{\corrupt{\process}}{\idealstepsto!{}}
\simulatedBy
\using{\corrupt{\process}}{\realstepsto!{}}
\).

The main difference between the two semantics is the interface with the
In the real semantics,
dishonest hosts actively leak data to the adversary
(through expressions and communication statements),
and the adversary controls all data coming from malicious hosts
(through ).
In contrast, the ideal semantics interacts with the adversary
only via and .
In effect, the ideal semantics causes leakage and corruption to become
Additionally, by eliminating all blocking expressions
(which communicate with the adversary), the ideal semantics can make
progress in a manner independent of the adversary;
this aids the sequentialization proof in <ref>.

To bridge the gap between the real and ideal semantics,
we show that the simulator can use expressions
to recreate all data no longer leaked through communication,
and expressions to corrupt all data no longer corruptible through
This is possible because our type system ensures secrets are not
directly sent to dishonest hosts (<ref>),
and data from malicious hosts cannot directly influence trusted data

The simulator maintains a public view of the real process,
and runs the adversary against this view.
The simulator flips the input/output behavior of and expressions:
when the ideal process outputs data through a expression,
the simulator inputs this data instead.
Similarly, the simulator outputs data with expressions,
which it sends to the ideal process.
The key invariant is that the simulator's version of the process
matches the real one on public values,
and the ideal process matches the real one on trusted values.

This invariant is strong enough to witness simulatability.
Since the simulator's version of the process matches the real one on public values,
the adversary in the real configuration has a view identical to the adversary
running inside of the simulator
(the adversary only sees public data).
Similarly, since the real process matches the ideal one on trusted values,
the environment has the same view in both
(the environment is only sent trusted data).

Next, we argue that our simulator can preserve the invariant.
For the simulator to have an accurate view of public values in the real process,
the ideal process must output values through expressions that
match the values in the real process.
The information-flow type system provides necessary restrictions.
Robust declassification <cit.> guarantees only trusted values
are declassified.
Since the ideal process matches the real one on trusted values,
data coming from expressions is accurate.
Dually, when the simulator sends data to the ideal process
through expressions, the values must match the ones in the real process.
Transparent endorsement <cit.> guarantees only public values
are endorsed.
Thus, the result follows from the simulator holding accurate public values.
See sec:correctness-of-ideal-execution-details for details.

Consider choreography and its corruption $\corrupt{\process}$
when is malicious:

'+ 1

'+ 1

The function $\corrupt{\cdot}$
erases all code on (the first statement) since a malicious
host does not follow the choreography and has arbitrary behavior.
Additionally, it replaces all communication statements involving with /statements,
capturing the fact that need not use the variables specified in the
choreography (and $\x'$).
In particular, even though the original choreography specifies sends
the same value to and , a malicious can send
different values.
Giving the power to equivocate in this manner can compromise
for instance, could cause and to disagree on control flow
if is used as a conditional guard.
Information-flow checking prevents from exploiting this power.

Information-flow checking ensures untrusted data (from malicious hosts)
cannot influence trusted data (of nonmalicious hosts).
We formalize this intuition by erasing all data from malicious hosts in
the ideal semantics:
instead of receiving the value of from (i.e., the adversary),
simply assigns to (does the same for ).
The adversary cannot possibly have any control over trusted data if all data
coming from the adversary is replaced with .
Note that erasing untrusted data can change the adversary's view.
In the example, sends $\y' = \y + 1$ to ,
which is different from sending $\vunit + 1$.
The simulator can compute the correct value in this case since comes from the
adversary (which the simulator has access to), and $1$ is a fixed constant.
In the general case, the simulator can compute all public values, and
our type system ensures only public values are sent to dishonest hosts

In addition to preventing the adversary from corrupting trusted values,
we must prevent the adversary from learning secrets.
In the real semantics, the adversary witnesses all communication
and can read any message if at least one endpoint is dishonest.
Information-flow checking ensures the adversary does not learn anything new by
reading these messages.
We formalize this intuition by erasing communication:
in the ideal semantics, communication statements step internally.
The simulator must again recreate these hidden messages for the adversary,
which is possible since our type system ensures the messages the adversary
can read are public.

Simply discarding all untrusted data and hiding all secret data weakens
the adversary in the ideal semantics too much.
We bridge the gap between the real and ideal semantics through downgrade
An expression indicates that some untrusted data should be treated as
trusted, so in the ideal semantics, an inputs data from the adversary.
Dually, a expression indicates some secret data should be treated
as public, so a outputs data to the adversary.
Explicit /expressions capture programmer intent.
Going back to the example,
our type system requires and to before using it
in a trusted context.
If and separately , then they might get two different
If there is only one (e.g., a separate trusted host performs the and shares the result),
then there can only be one value.

The core of the simulation result is showing that the simulator can
use expressions to recreate all data no longer leaked
through communication,
and expressions to influence all data no longer corruptible through
For this to work, we need to ensure the ideal choreography outputs the correct
value to the simulator when performing a ,
and we need to ensure the simulator can input the correct value to the ideal
choreography for an .
For example, when the ideal choreography performs $\ddeclassify{\x}$,
we must ensure the value of is the same in the real and ideal choreographies.
This is nontrivial since the ideal semantics replaces all untrusted data with
Robust declassification requires only trusted data is declassified,
and type checking ensures untrusted data does not influence trusted data.
Thus, is trusted and erased values cannot influence its value.
Similarly, when the ideal choreography performs $\dendorse{\x}$,
the simulator must compute the value would have in the real choreography
and send that to the ideal choreography.
Transparent endorsement requires only public data is endorsed,
and the simulator can recreate all public data.

Stepping rules used internally by the simulator.
These override <ref>.

The simulator maintains a public view of the real process,
and runs the adversary against this view.
It uses the rules in <ref>,
which flip the roles of and .
We maintain the invariant that the simulator's version of the choreography
matches the real one on public values,
and the ideal choreography matches the real one on trusted values.
Next, we define what it means for two terms to agree on public/trusted values.

A closing substitution
\( \csecure{\cs}{\ctx} \)
is a mapping from variables to values
\( \cs : \dom(\ctx) \to \val! \).

A channel's label derives from the labels of its endpoints:

_1 _2
_1 ∨_2

We let
\( \labelof{\advprot} = \ifbottom \)
\( \labelof{\envprot} = \strongest \),
which leads to
\(
\labelof{\envprot\, \ch}
\labelof{\ch\, \envprot}
\labelof{\ch}
\)
\(
\labelof{\advprot\, \ch}
\labelof{\ch\, \advprot}
\integrity{\labelof{\ch}}
\)
(communication with the adversary is public,
and is trusted only if the other endpoint is).

For a set of labels \( \lbl* \subseteq \lbl! \),
define \( \equalsat{\lbl*} \) as follows.

* \(
\mglobal{\ch_1}{\ch_2}{\val_1}
\equalsat{\lbl*}
\mglobal{\ch_1}{\ch_2}{\val_2}
\)
\( \labelof{\ch_1 \ch_2} \in \lbl* \)
\( \val_1 = \val_2 \).

* \( \ainput{\msg_1} \equalsat{\lbl*} \ainput{\msg_2} \)
\( \aoutput{\msg_1} \equalsat{\lbl*} \aoutput{\msg_2} \)
\( \msg_1 \equalsat{\lbl*} \msg_2 \).

* \( \s_1 \equalsat{\lbl*} \s_2 \)
if there exist
\( \ctx_1 \), \( \ctx_2 \), and with
\( \ssecure[(\ctx_1 \munion \ctx_2)]{\s} \),
and substitutions \( \csecure{\cs_1, \cs_2}{\ctx_2} \) such that
\( \cs_1(\s) = \s_1 \)
\( \cs_2(\s) = \s_2 \).
Additionally, for
\( (\csing{\x}{\lbl}{\h}) \in (\ctx_1 \munion \ctx_2) \),
we require
\( \labelof{\h} \actsfor \lbl \),
and for
\( (\csing{\x}{\lbl}{\h}) \in \ctx_2 \),
we require
\( \lbl \not\in \lbl* \).

* \( \buffer_1 \equalsat{\lbl*} \buffer_2 \)
\( \buffer_1(\ch_1 \ch_2) = \buffer_2(\ch_1 \ch_2) \)
for all \( \ch_1 \) and \( \ch_2 \) such that
\( \labelof{\ch_1 \ch_2} \in \lbl* \).

* \(
\proc{\h*}{\buffer_1}{\s_1}
\equalsat{\lbl*}
\proc{\h*}{\buffer_2}{\s_2}
\)
\( \buffer_1 \equalsat{\lbl*} \buffer_2 \)
\( \s_1 \equalsat{\lbl*} \s_2 \).

We instantiate <ref> with $\lbl* = \public$
for agreement on public values,
and with $\lbl* = \trusted$ for agreement on trusted values.
<Ref> requires the two terms to have the same structure,
but allows some values $\val \in \val!$ (those with labels not in *)
to differ between them.
For example, two messages can only be equivalent if they are on the same channel.
Additionally, they must carry the same value if the channel is public and we
are considering public equality ($\publiceq$);
they are allowed to carry different values otherwise.
Action and buffer equivalence simply lift the definition for messages.
Equivalence for statements demands further explanation.

Values are fixed constants and can be assigned any label.
It is therefore not immediate which values should be allowed to differ
between statements.
For example, consider the following statements that have the
same structure but differ in the value of :

\( \s_1 \)

\( \s_2 \)

The intuition behind <ref> is that $\s_1$ and $\s_2$
are equivalent if can be treated as secret/untrusted.
To check that, <ref> abstracts out values where the two
statement differ to find a common statement,
and type-checks the generalized statement in a context where all introduced
variables are marked as secret/untrusted.
For example, we could pick as follows

\( \s \)

along with substitutions
\( \cs_1 = \set{ \x' \mapsto \vfalse } \)
\( \cs_2 = \set{ \x' \mapsto \vtrue } \).
If can be typed under a context where $\x'$ is considered secret,
then $\s_1 \publiceq \s_2$.
However, if has a public label (is dishonest), for example,
then there is no such context.

<Ref> splits the context into $\ctx_1$ and $\ctx_2$,
with the substitutions only assigning values for variables in $\ctx_2$.
Context $\ctx_1$ is added to allow relating open terms,
which is needed for inductive cases of some proofs.

For the rest of this section,
we assume $\lbl* = \public$ or $\lbl* = \trusted$.
Moreover, whenever $\ereceive{\h}$ or $\esend{\aexp}{\h}$ appears in a
program, we assume $\malicious{\h}$
(which is ensured by $\corrupt{\cdot}$).[
Our results hold for more general *, but we do not need this generality.

Equivalent choreographies remain equivalent given equivalent inputs
and after producing outputs on the same host.

\( \s_1 \equalsat{\lbl*} \s_2 \)
\( \s_1 \realstepsto!{\action_1} \s_1' \)
without using <ref> or <ref>.

* If
\( \action_1 = \ainput{\msg_1} \),
\( \s_2 \realstepsto!{\ainput{\msg_2}} \s_2' \)
\( \s_1' \equalsat{\lbl*} \s_2' \)
for all
\( \msg_2 \equalsat{\lbl*} \msg_1 \).

* If
\( \action_1 = \aoutput{\msg_1} \),
\( \s_2 \realstepsto!{\aoutput{\msg_2}} \s_2' \)
\( \s_1' \equalsat{\lbl*} \s_2' \)
for some \( \msg_2 \) with
\( \actor{\aoutput{\msg_2}} = \actor{\aoutput{\msg_1}} \).

By <ref>,
there exists such that
\( \ssecure[\ctx]{\s} \),
\( \cs_1(\s) = \s_1 \),
\( \cs_2(\s) = \s_2 \)
for some $\ctx = (\ctx_1 \munion \ctx_2)$
and $\csecure{\cs_1, \cs_2}{\ctx_2}$.
We proceed by induction on the stepping judgment.
In all cases, stepping on $\s_1$ forces certain atomic expressions to be values (as opposed to variables );
the same expressions in $\s_2$ must also be values since $\cs_2$ substitutes
for the same variables as $\cs_1$.
We appeal to this fact implicitly.

We have

with $\actor{\action_1} = \actor{\action_2} = \h$.
Inversion on \( \ssecure{\s} \) gives

In each case, we either prove $\val_1 = \val_2$ or $\lbl \not\in \public$.
When $\val_1 = \val_2$, we define
\( \s' = \subst{\x}{\val}{\s''} \).
We then have
\( \ssecure[\ctx]{\s'} \) by <ref>,
\( \cs_1(\s') = \subst{\x}{\val}{\s_1''} = \s_1' \),
\( \cs_2(\s') = \subst{\x}{\val}{\s_2''} = \s_2' \),
\( \s_1' \equalsat{\lbl*} \s_2' \).

When $\lbl \not\in \public$, we define
\( \ctx_2' = (\ctx_2 \munion \csing{\x}{\h}{\lbl}) \),
\( \cs_1' = \cs_1 \cup \set{\x \mapsto \val_1} \),
\( \cs_2' = \cs_2 \cup \set{\x \mapsto \val_2} \),
which ensures
\( \cs_1'(\s'') = \subst{\x}{\val_1}{\s_1''} = \s_1' \)
\( \cs_2'(\s'') = \subst{\x}{\val_2}{\s_2''} = \s_2' \).
Note that $\ctx_2$ satisfies the requirements of <ref>,
and $\csecure{\cs_1', \cs_2'}{\ctx_2'}$,
\( \s_1' \equalsat{\lbl*} \s_2' \).

We case on the expression stepping relation to show one of the requirements.

We have

_1^1, …, _1^n

_2^1, …, _2^n

^1, …, ^n

If all $\aexp^i$ are values, then $\aexp_1^i = \aexp^i = \aexp_2^i$
and $\val_1 = \val_2$.
Otherwise, let $\aexp^i = \x^i$.
Inversion on $\esecure{\e}{\lbl}$ gives
\( (\csing{\x^i}{\h}{\lbl'}) \in \ctx_2 \)
for $\lbl' \not\in \lbl*$ and $\lbl' \flowsto \lbl$,
which implies $\lbl \not\in \lbl*$.

Deliberately excluded;
handled by <ref>.

Same as the case for <ref>.

Deliberately excluded;
handled by <ref>.

Same as the case for <ref>.

We have

Assume $\lbl \in \lbl*$ since we are done otherwise.
Inversion on $\esecure{\e}{\lbl}$ gives
\( \labelof{\h} \flowsto \lbl \),
so \( \labelof{\h} \in \lbl* \),
which means
\( \labelof{\envprot \h} = \labelof{\h} \in \lbl* \).
\(
\aglobalreceive{\envprot}{\h}{\val_1}
\action_1
\action_2
\aglobalreceive{\envprot}{\h}{\val_2}
\)
\( \val_1 = \val_2 \).

We have $\val_1 = \vunit = \val_2$.

We have $\val_1 = \vunit = \val_2$.

We have $\val_1 = \vunit = \val_2$.

We have

We have $\malicious{\h'}$ by assumption,
and $\ispublic{\labelof{\h'}}$ by <ref>.

If $\lbl* = \public$, then
$\labelof{\h'} \in \lbl*$ so $\labelof{\h' \h} \in \lbl*$.
This gives
\(
\aglobalreceive{\h'}{\h}{\val_1}
\action_1
\action_2
\aglobalreceive{\h'}{\h}{\val_2}
\),
so $\val_1 = \val_2$.

If $\lbl* = \trusted$, then
inversion on $\esecure{\e}{\lbl}$ gives
\( \integrity{\labelof{\h'}} \flowsto \lbl \).
Since $\labelof{\h'} \not\in \trusted = \lbl*$,
we have $\lbl \not\in \lbl*$.

We have $\val_1 = \vunit = \val_2$.

We have

By inversion on \( \ssecure{\s} \), we have

We case on .
If $\aexp = \val$ for some , then
$\val_1 = \cs_1(\val) = \val = \cs_2(\val) = \val_2$.
\( \ssecure[\ctx]{\subst{\x}{\val}{\s''}} \)
by <ref>,
\( \cs_1(\subst{\x}{\val}{\s''}) = \subst{\x}{\val}{\s_1''} \),
\( \cs_2(\subst{\x}{\val}{\s''}) = \subst{\x}{\val}{\s_2''} \),
\( \subst{\x}{\val_1}{\s_1''} \equalsat{\lbl*} \subst{\x}{\val_2}{\s_2''} \).

Otherwise, $\aexp = \x'$ for some $\x' \in \dom(\ctx_2)$.
By inversion on
\( \aesecure{\aexp}{\lbl}[\h_1] \),
we have $(\csing{\x}{\h_1}{\lbl'}) \in \ctx_2$
for some $\lbl' \flowsto \lbl$.
Since $\lbl' \not\in \lbl*$ and $\lbl' \flowsto \lbl$,
we have $\lbl \not\in \lbl*$.
\( \ctx_2' = (\ctx_2 \munion \csing{\x}{\h_2}{\lbl}) \),
\( \cs_1' = \cs_1 \cup \set{\x \mapsto \val_1} \),
\( \cs_2' = \cs_2 \cup \set{\x \mapsto \val_2} \),
which ensures
\( \cs_1'(\s'') = \subst{\x}{\val_1}{\s_1''} \)
\( \cs_2'(\s'') = \subst{\x}{\val_2}{\s_2''} \).
Note that $\ctx_2$ satisfies the requirements of <ref>,
and $\csecure{\cs_1', \cs_2'}{\ctx_2'}$,
\( \subst{\x}{\val_1}{\s_1''} \equalsat{\lbl*} \subst{\x}{\val_2}{\s_2''} \).

We have

$\ssecure{\s'}$ (by inversion on $\ssecure{\s}$),
$\cs_1(\s') = \s_1'$,
$\cs_2(\s') = \s_2'$,
$\s_1' \equalsat{\lbl*} \s_2'$.

We have

Inversion on \( \ssecure{\s} \)
(which must be by <ref>)
\( \aesecure{\aexp}{\ifbottom}[\h] \).
$\cs_1(\aexp)$ and $\cs_2(\aexp)$ are values,
so $\freevars{\aexp} \subseteq \ctx_2$,
\( \aesecure[\ctx_2]{\aexp}{\ifbottom}[\h] \).
Since $\ifbottom \in \lbl*$ for all attacks
(recall <ref>),
and $\ctx_2$ only contains variables with labels not in *,
$\aexp$ must be a value,
that is, $\aexp = \val$ for some $\val$.
$\val_1 = \cs_1(\val) = \val = \cs_2(\val) = \val_2$,
so $i = j$.
Finally, we have
$\s_1^i \equalsat{\lbl*} \s_2^j$
$\ssecure{\s_i}$ (by inversion on $\ssecure{\s}$),
$\cs_1(\s^i) = \s_1^i$,
$\cs_2(\s^i) = \s_2^i = \s_2^j$.

Impossible by inversion on \( \ssecure{\s} \).

Immediate by the induction hypothesis.

We have

_1” ! _1”'

_2” ! _2”'

Note that
\( \ssecure[(\ctx_1 \munion \ctx_1' \munion \ctx_2)]{\s''} \)
where $\ctx_1'$ are the variables defined by (which must be the same as the ones defined by $\ectx_1$ and $\ectx_2$).
\( \s_1'' \equalsat{\lbl*} \s_2'' \)
through $\s''$, $\cs_1$, and $\cs_2$,
and we can apply induction hypothesis to get
\( \s_1''' \equalsat{\lbl*} \s_2''' \).
This then gives
\(
\s_1'
\ectxof[\ectx_1]{\s_1'''}
\equalsat{\lbl*}
\ectxof[\ectx_2]{\s_2'''}
\s_2'
\).

Using the induction hypotheses similar to <ref>.

Public-equivalent choreographies produce public-equivalent outputs.

\( \s_1 \publiceq \s_2 \),
\( \s_1 \realstepsto!{\aoutput{\msg_1}} \),
\( \s_2 \realstepsto!{\action_2} \)
\( \actor{\aoutput{\msg_1}} = \actor{\action_2} \),
\( \aoutput{\msg_1} \publiceq \action_2 \).

By <ref>,
there exists such that
\( \ssecure[\ctx]{\s} \),
\( \cs_1(\s) = \s_1 \),
\( \cs_2(\s) = \s_2 \)
for some $\ctx = (\ctx_1 \munion \ctx_2)$
and $\csecure{\cs_1, \cs_2}{\ctx_2}$.
We proceed by induction on the two stepping judgments,
which must be by the same rule since $\s_1$ and $\s_2$ have the same structure.

Cases for <ref> follow from the
induction hypotheses.
Cases for <ref>
are immediate since both actions are internal, i.e.,
\( \aoutput{\msg_1} = \aglobalinternal{\h} = \action_2 \)
for some , which implies
\( \aoutput{\msg_1} \publiceq \action_2 \).
We detail the remaining cases.

We have

Inversion on \( \ssecure{\s} \) gives
\( \esecure{\e}{\lbl} \) for \( \labelof{\h} \actsfor \lbl \).
We case on the expression stepping relations.

We have \( \ch = \envprot \), \( \nonmalicious{\h} \), and

If \( \labelof{\h} \not\in \public \),
\(
\aoutput{\msg_1}
\aglobalsend{\h}{\envprot}{\val_1}
\publiceq
\aglobalsend{\h}{\envprot}{\val_2}
\action_2
\)
immediately, so assume \( \ispublic{\labelof{\h}} \).
Inversion on \( \esecure{\e}{\lbl} \) gives
\( \aesecure{\aexp}{\labelof{\h}} \).
Since \( \labelof{\h} \in \public \),
$\aexp = \val$ for some , meaning
\( \val_1 = \cs_1(\aexp) = \val = \cs_2(\aexp) = \val_2 \),
\(
\aoutput{\msg_1}
\aglobalsend{\h}{\envprot}{\val}
\aglobalsend{\h}{\envprot}{\val}
\action_2
\),
\(
\aoutput{\msg_1}
\publiceq
\action_2
\).

We have \( \ch = \h' \) and

If $\aexp = \val$ for some , then $\val_1 = \val_2$ and
we are done, so assume $\aexp = \x'$ for some $\x'$.
Inversion on \( \esecure{\e}{\lbl} \) gives
\( \aesecure{\aexp}{\confidentiality{\labelof{\h'}}} \).
We then have
\( (\csing{\x'}{\lbl'}{\h}) \in \ctx_2 \)
$\labelof{\h} \actsfor \lbl'$,
$\lbl' \not\in \public$,
$\lbl' \flowsto \confidentiality{\labelof{\h'}}$.

\begin{align*}
\lbl' \not\in \public
\wedge
\labelof{\h} \actsfor \lbl'
\labelof{\h} \not\in \public
\\
\lbl' \flowsto \confidentiality{\labelof{\h'}}
\wedge \lbl' \not\in \public
\implies
\confidentiality{\labelof{\h'}} \not\in \public
\labelof{\h'} \not\in \public
\end{align*}

\( \labelof{\h \h'} \not\in \public \)
\(
\aoutput{\msg_1}
\aglobalsend{\h}{\h'}{\val_1}
\publiceq
\aglobalsend{\h}{\h'}{\val_2}
\action_2
\).

We have

By inversion on \( \ssecure{\s} \), we have

We case on .
If $\aexp = \val$ for some , then
$\val_1 = \cs_1(\val) = \val = \cs_2(\val) = \val_2$.
$\action_1 = \aglobalsend{\h_1}{\h_2}{\val} = \action_2$
$\action_1 \publiceq \action_2$.

Otherwise, $\aexp = \x'$ for some $\x' \in \dom(\ctx_2)$.
By inversion on
\( \aesecure{\aexp}{\lbl}[\h_1] \),
we have $(\csing{\x}{\h_1}{\lbl'}) \in \ctx_2$
for some $\lbl' \flowsto \lbl$.

\begin{align*}
\lbl' \not\in \public
\wedge \lbl' \flowsto \lbl
\lbl \not\in \public
\\
\lbl' \not\in \public
\wedge \labelof{\h_1} \actsfor \lbl'
\labelof{\h_1} \not\in \public
\\
\lbl \not\in \public
\wedge \labelof{\h_2} \actsfor \lbl
\labelof{\h_2} \not\in \public
\\
\labelof{\h_1} \not\in \public
\wedge \labelof{\h_2} \not\in \public
\labelof{\h_1 h_2} \not\in \public
\end{align*}

Since $\labelof{\h_1 h_2} \not\in \public$,
\(
\action_1
\aglobalsend{\h_1}{\h_2}{\val_1}
\publiceq
\aglobalsend{\h_1}{\h_2}{\val_2}
\action_2
\).

We have

Note that selection statements do not allow variables to be communicated,
so sending (rather than ) is not a mistake.
Thus, we have
$\val_1 = \cs_1(\val) = \val = \cs_2(\val) = \val_2$,
which means
$\action_1 = \aglobalsend{\h_1}{\h_2}{\val} = \action_2$,
which in turn means
$\action_1 \publiceq \action_2$.

Trusted-equivalent choreographies produce trusted-equivalent outputs
for the environment.
The statement does not apply to intermediate messages between hosts
because untrusted values can be sent on trusted channels
(e.g., a trusted third party can process untrusted values from other hosts).

\( \s_1 \publiceq \s_2 \),
\( \s_1 \realstepsto!{\aglobalsend{\h}{\envprot}{\val_1}} \),
\( \s_2 \realstepsto!{\action_2} \)
\( \actor{\action_2} = \h \),
\( \aglobalsend{\h}{\envprot}{\val_1} \publiceq \action_2 \).

By induction on the stepping relations.
Inductive cases are handled similarly to <ref>.
The only other relevant case is under <ref>
with <ref>.
The argument is similar to the case in <ref>,
but holds because only trusted values can be to nonmalicious hosts.

The simulator's view of the real choreography stays accurate on public values.

\( \s_1 \publiceq \s_2 \)
\( \s_1 \realstepsto!{\action_1} \s_1' \)
without using <ref> or <ref>.

* If
\( \action_1 = \ainput{\msg_1} \),
\( \s_2 \simstepsto!{\ainput{\msg_2}} \s_2' \)
\( \s_1' \publiceq \s_2' \)
for all
\( \msg_2 \publiceq \msg_1 \).

* If
\( \action_1 = \aoutput{\msg_1} \),
\( \s_2 \simstepsto!{\aoutput{\msg_2}} \s_2' \)
\( \s_1' \publiceq \s_2' \)
for some
\( \msg_2 \publiceq \msg_1 \).

In addition, the statement holds with the roles of \( \realstepsto!{} \) and
\( \simstepsto!{} \) reversed
(excluding <ref> instead).

Follows immediately from
since \( \simstepsto!{} \) is equivalent to \( \realstepsto!{} \) except for
which we exclude.

The ideal choreography stays accurate to the real choreography on trusted values.

\( \s_1 \trustedeq \s_2 \)
\( \s_1 \realstepsto!{\action_1} \s_1' \)
without using <ref> or <ref>.

* If
\( \action_1 = \aglobalreceive{\envprot}{\h}{\val_1} \),
\( \s_2 \idealstepsto!{\action_2} \s_2' \)
\( \s_1' \trustedeq \s_2' \)
for all
\( \action_2 \trustedeq \action_1 \).

* If
\( \action_1 = \aglobalsend{\h}{\envprot}{\val_1} \),
\( \s_2 \idealstepsto!{\action_2} \s_2' \)
\( \s_1' \trustedeq \s_2' \)
for some
\( \action_2 \trustedeq \action_1 \).

* Otherwise,
\( \s_2 \idealstepsto!{\aglobalinternal{\h}} \s_2' \)
\( \s_1' \trustedeq \s_2' \)
\( \actor{\action_1} = \h \).

In addition, the statement holds with the roles of \( \realstepsto!{} \) and
\( \idealstepsto!{} \) reversed
(excluding <ref> instead).

Follows from
judgment \( \realstepsto!{} \) behaves the same as \( \realstepsto!{} \)
except it replaces some output messages with internal steps.
Since this does not affect the resulting choreographies (only the actions),
<ref> applies and shows that the resulting
choreographies are equivalent.
The one exception to this <ref>,
where the ideal choreography proceeds with instead of receiving a value;
this value is treated as untrusted so the choreographies still agree on
trusted values as required.

Assume the simulator's view agrees with the real choreography on public values,
and the ideal choreography agrees with the real choreography on trusted values.
If the ideal choreography declassifies a value and we feed that value to
the simulator, then all three choreographies remain in agreement.
Only trusted values are declassified,
so the ideal choreography outputs the correct value to the simulator.

\( \s_1 \publiceq \s_2 \)
\( \s_1 \trustedeq \s_3 \).
\( \s_1 \realstepsto!{\aglobalinternal{\h}} \s_1' \),
\( \s_2 \simstepsto!{\aglobalreceive{\h}{\advprot}{\val}} \s_2' \),
\( \s_3 \idealstepsto!{\aleak{\h}{\val}} \s_3' \),
\( \s_1' \publiceq \s_2' \)
\( \s_1' \trustedeq \s_3' \).

By <ref>,
there exist $\pe{\s}$ and $\te{\s}$ such that
\( \ssecure[\pe{\ctx}]{\pe{\s}} \),
\( \cs_1(\pe{\s}) = \s_1 \),
\( \cs_2(\pe{\s}) = \s_2 \),
\( \ssecure[\te{\ctx}]{\te{\s}} \),
\( \cs_2'(\te{\s}) = \s_2 \),
\( \cs_3(\te{\s}) = \s_3 \)
\( \pe{\ctx} = (\ctx_1 \munion \ctx_2) \),
\( \csecure{\cs_1, \cs_2}{\ctx_2} \),
\( \te{\ctx} = (\ctx_3 \munion \ctx_4) \),
\( \csecure{\cs_2', \cs_3}{\ctx_4} \).

We proceed by induction on the stepping relations.
Inductive cases (<ref>) are handled
similarly to <ref>.
The only remaining case is when the steps are by
We have

where $\issecret{\fromlbl}$ and $\ispublic{\tolbl}$, and

We claim $\val_1 = \val$
($\val_2$ is ignored by $\s_2$, so it is irrelevant).
By <ref> and inversion on
\( \ssecure[\te{\ctx}]{\te{\s}} \),
we have $\istrusted{\fromlbl}$.
Assume for contradiction that $\te{\aexp} = \te{\x}$ for some $\te{\x}$.
Then, $(\csing{\te{\x}}{\h}{\lbl}) \in \ctx_4$ for
$\lbl \flowsto \fromlbl$.
However, $\lbl \not\in \trusted$ so $\fromlbl \not\in \trusted$,
which is a contradiction.
Thus, $\te{\aexp} = \te{\val}$ for some $\te{\val}$.
\(
\val_1
\cs_2'(\te{\aexp})
\cs_2'(\te{\val})
\te{\val}
\cs_3(\te{\val})
\cs_3(\te{\aexp})
\val
\).

Finally, let
\( \pe{\s}' = \subst{\x}{\val}{\pe{\s}''} \)
\( \te{\s}' = \subst{\x}{\val}{\te{\s}''} \).
We have
\( \s_1' \publiceq \s_2' \)
\( \ssecure[\pe{\ctx}]{\pe{\s}'} \)
(inversion on
\( \ssecure[\pe{\ctx}]{\pe{\s}} \)
followed by <ref>),
\( \cs_1(\pe{\s}') = \s_1' \),
\( \cs_2(\pe{\s}') = \s_2' \);
and we have
\( \s_2' \trustedeq \s_3' \)
\( \ssecure[\te{\ctx}]{\te{\s}'} \)
(inversion on
\( \ssecure[\te{\ctx}]{\te{\s}} \),
then <ref>),
\( \cs_2'(\te{\s}') = \s_2' \),
\( \cs_3(\te{\s}') = \s_3' \).

Similarly, if the simulator recreates a value that the ideal choreography
endorses, all three choreographies remain in agreement.
Only public values are endorsed,
so the simulator outputs the correct value to the ideal choreography.

\( \s_1 \publiceq \s_2 \)
\( \s_1 \trustedeq \s_3 \).
\( \s_1 \realstepsto!{\aglobalinternal{\h}} \s_1' \),
\( \s_2 \simstepsto!{\aglobalsend{\advprot}{\h}{\val}} \s_2' \),
\( \s_3 \idealstepsto!{\amaul{\h}{\val}} \s_3' \),
\( \s_1' \publiceq \s_2' \)
\( \s_1' \trustedeq \s_3' \).

Dual to <ref>,
but focusing on \( \s_1 \publiceq \s_2 \)
and using <ref>.

<Ref> straightforwardly lift from
choreographies to processes .
<Ref> needs an additional condition on buffer equivalence:
\( \buffer_1 \publiceq \buffer_2 \),
we require
\( \sizeof{\buffer_1(\ch_1 \ch_2)} = \sizeof{\buffer_2(\ch_1 \ch_2)} \)
\( \labelof{\ch_1 \ch_2} \not\in \public \).
That is, the buffers must agree exactly on public channels,
and agree on the number of messages on secret channels.
This condition allows the simulator to keep track of messages on secret channels
even though it cannot read message contents.

We prove simulation as follows.

The simulator has the form \( \simof{\process} \)
where is a public view of the real process.
The simulator runs against for all internal messages.
The simulator forwards inputs from to and ,
and forwards messages from destined for to .
When the ideal process outputs data through a expression,
the simulator inputs this data to .
Similarly, when outputs data through an expressions,
the simulator forwards this data to the ideal process.[
The simulator needs to step the ideal process an additional time
so that the ideal process pulls the message from its buffer.
This is due to how we define operational rules for processes.
This extra step forces us to use weak bisimulation instead of strong

We maintain the invariant that the simulator's version of the process
matches the real one on public values,
and the ideal process matches the real one on trusted values.
More concretely, we define
\(
\adv \parallel \process_1
\rel
\simof[\adv']{\process} \parallel \process_2
\)

\( \adv = \adv' \)

\( \process_1 \publiceq \process \)

\( \process_1 \trustedeq \process_2 \)

We claim $\rel$ is a weak bisimulation.

Since the simulator's version of the process matches the real one on public
values (<ref>),
the adversary in the real configuration has a view identical to the
adversary running inside of the simulator
(the adversary only sees public data).
Similarly, since the real process matches the ideal one on trusted values,
the environment has the same view in both
(the environment is only sent trusted data).

<Ref> is preserved since $\process$ is an
accurate public view of $\process_1$ (<ref>).
When there are no downgrade actions,
<ref> ensures <ref> is preserved,
and <ref> ensures <ref> is
<Ref> cover
the cases with downgrades.

§ ENDPOINT PROJECTION

The second stage of compilation, endpoint projection,
transforms a choreography into a distributed program.

§.§ Hybrid Distributed Language

Hybrid distributed syntax as an extension to source

As for choreographies, <ref> specifies the syntax of
hybrid distributed programs by extending the syntax of source programs.
Hybrid distributed programs are configurations containing multiple
processes, with each
process acting on behalf of a single host $\h \in \h!$.
These processes communicate data via /and agree on control flow via and .
The statement, on receiving a value on the expected channel,
steps to the specified branch.

*Operational Semantics

Each process transitions using the real stepping rules ($\realstepsto{}$),
and the distributed configuration steps using the parallel composition rules in

§.§ Compiling to Distributed Programs

Given a choreography and a host , the endpoint projection $\project[\h]{\s}$
defines the local program that should run.
The distributed system $\partition{\s}$ is derived by independently projecting
onto each host in the choreography.

Our notion of endpoint projection is entirely standard,
so we defer the formal definition to
Our proof is agnostic to how endpoint projection is defined,
and only relies on its soundness and completeness,
properties extensively studied in prior work <cit.>.

[] = '

' =

_1 =

_2 =

_1 =

_2 =

' =

_1_2 =

_1_2↦__∈*_1 ∪*_2

$\val*_1$ and $\val*_2$ disjoint

_1 = _1'
_2 = _2'

[] = '
= '

\begin{align*}
\projectH{\buffer}(\ch_1 \ch_2)
\begin{cases}
\buffer(\ch_1 \ch_2) & \ch_1 \neq \h \wedge \ch_2 = \h
\\
\emptylist & \text{otherwise}
\end{cases}
\\
\projectH{\proc{\h*}{\buffer}{\s}}
\proc{\h* \cap \set{\h}}{\projectH{\buffer}}{\projectH{\s}}
\end{align*}

Endpoint projection: statements, buffers, processes.

<Ref> formalizes projecting onto a host .
Projection keeps statements assigned to ,
and removes ones assigned to other hosts.
Communication statements become a or a , or are entirely removed
depending on whether is the sending host, the receiving host, or neither.
Selection statements follow the same logic,
but are projected as a expression
or a statement with a single branch.

The most interesting case is statements.
If the statement is placed at ,
we perform the as usual and project the branches.
Otherwise, does not store the conditional and cannot determine which
branch should be taken.
In this case, the projections of the two branches must be compatible,
formalized by a merge function.
Merging requires the two branches to have the same syntactic structure,
but allows statements to have disjoint branches,
which are combined into one.
We elide most cases of the merge function,
since the proof is agnostic to the details.

We lift projection to processes:
projecting a buffer onto keeps only messages destined for ,
and projecting processes is done componentwise.
The projection $\partition{\process}$ of process $\process$
is the configuration formed by projecting onto each host in $\process$:

\[
\partition{\process = \proc{\h*}{\_}{\_}}
\bigparallel_{\h \in \h*}{\project[\h]{\process}}
\]

§.§ Correctness of Endpoint Projection

Let $\corrupt{\config}$ remove from $\config$ all processes for
malicious hosts.

\( \ssecure[\emptylist]{\process} \),
\(
\using{\corrupt{\process}}{\realstepsto!{}}
\simulatedBy
\using{\corrupt{\partition{\process}}}{\realstepsto{}}
\).

A choreography and its endpoint projection match each other action-for-action;
once we prove this fact, showing simulation is trivial since we can pick
$\simulator = \adv$.
This perfect correspondence between a choreography and its projection is studied
extensively in the literature <cit.>,
and formalized as soundness and completeness
of endpoint projection.
However, the standard methods of proving soundness and completeness must
be modified to handle malicious corruption and asynchronous communication.
Existing work relates $\process$ to $\partition{\process}$,
which we must extend to relate $\corrupt{\process}$ to $\corrupt{\partition{\process}}$.
This is trivial since
$\corrupt{\partition{\process}} = \partition{\corrupt{\process}}$.

The presence of asynchrony breaks the perfect correspondence between
the projected program and the choreography:
a /pair reduces in two steps in a projected program,
but the corresponding communication statement reduces in
only one.
We follow prior work <cit.> and add syntactic forms
to choreographies for partially reduced /pairs:
messages that have been sent and buffered but not yet received.
These run-time terms exist only to restore the correspondence,
and are never generated by the compiler.
An additional, simple simulation then shows that a choreography
with these run-time terms simulates one without,
removing the need to reason about run-time terms in other proof steps.
For details, see sec:correctness-of-projection-details.

A choreography and its endpoint projection match each other action-for-action;
once we prove this fact, showing simulation is trivial since we can pick
$\simulator = \adv$.
The choreographic programming literature <cit.>
extensively studies this perfect correspondence between a choreography and
its projection, and formalizes the correspondence as strong bisimulation.

To prove that a choreography is bisimilar to its endpoint projection
$\partition{\process}$, we must define a relation $\rel$ between an arbitrary
configuration and process, $\config_1 \rel \process_2$,
and show that $\rel$ is a bisimulation.
The obvious approach is to define
\( \config_1 \rel \process_2 \)
\( \config_1 = \partition{\process_2} \),
but this idea fails because $\rel$ is not preserved under stepping.

\( \config_1 \rel \process_2 \)
\( \config_1 = \partition{\process_2} \).
We claim \( \rel \) is not a bisimulation.

Consider the following choreography and its projection:

_2 =

[]_2 =

[]_2 =

Let $\config_1 = \partition{\process_2}$;
we have $\config_1 \rel \process_2$.
Now, host can reduce the statement with an internal step in both
$\config_1$ and $\process_2$, which gives:

_2' =

_1'() =

_1'() =

Note that the process for in $\config_1'$ does not match
$\project[\bob]{\process_2'}$, which is

\[
\project[\bob]{\process_2'}
\scase{\alice}{\bob}{
\set{
\vtrue \mapsto \project[\bob]{\s_1}
\]

(there is no case for $\vfalse$).

Thus, we have
\( \config_1 \rel \process_2 \),
\( \config_1 \stepsto{\aglobalinternal{\alice}} \config_1' \),
\( \process_2 \stepsto{\aglobalinternal{\alice}} \process_2' \),
but it is not the case that \( \config_1' \rel \process_2' \).
<Ref> implies $\config_1'$ is uniquely determined,
so there is no other $\config_1''$ related to $\process_2'$ that $\config_1$
can step to.
Therefore, $\rel$ is not a bisimulation.

Intuitively, when a choreography reduces an statement,
the branch that is not taken disappears in one step for all hosts.
However, in the projected program,
each host reduces its corresponding statement separately,
which results in extraneous dead branches during simulation.
This is a known issue in the choreography literature <cit.>,
and it does not break bisimilarity, but
we need to be smarter about how to define $\rel$.

The solution to the issue raised by <ref>
is to ignore extraneous branches when defining $\rel$.
Even though the configuration $\config_1'$ has “leftover” branches
that projecting the choreography $\process_2'$ does not create,
we know that these branches will never be taken.
So we can ignore these branches when defining $\rel$.

Following <cit.>,
we define $\process_1 \refinedby \process_2$
if $\process_1$ and $\process_2$ are structurally identical,
except $\process_1$ has at least as many branches in statements as $\process_2$.
We lift $\refinedby$ pointwise to configurations.
Now, we define
\( \config_1 \rel \process_2 \)
\( \config_1 \refinedby \partition{\process_2} \).
We claim $\rel$ is a bisimulation.
the proof is split into showing the soundness and completeness
of endpoint projection.

\( \config \refinedby \partition{\process} \)
\( \process \realstepsto!{\action} \process' \),
\( \config \realstepsto{\action} \config' \)
for some \( \config' \refinedby \partition{\process'} \).

\( \config \refinedby \partition{\process} \)
\( \config \realstepsto{\action} \config' \),
\( \process \realstepsto!{\action} \process' \),
for some \( \process' \) with
\( \config' \refinedby \partition{\process'} \).

§.§ Handling Asynchronous Communication

The syntax of asynchronous choreographies
(extends <ref>).

Stepping rules for asynchronous choreographies.
These override the rules for $\realstepsto{}$ in <ref>.

We follow prior work <cit.> and add syntactic forms
to choreographies to represent partially reduced /pairs
given in <ref>.
We extend endpoint projection so that the new syntactic forms are projected
as a statement and a message on the receiver's buffer.
For example, while
\( \smove{\alice}{\val}{\bob}{\x}{\s} \)
becomes a on and a on ,
\( \smovepartial{\alice}{\val}{\bob}{\x}{\s} \)
becomes a on and a message (from ) in 's buffer.
We update the stepping rules for communication and selection statements
so that they reduce to the corresponding run-time terms,
which in turn reduce to their continuations.
<Ref> gives the updated rules.

These run-time terms are sufficient to restore perfect correspondence,
and make <ref> go through.
We refer to <cit.> for details.

\( \ssecure[\emptylist]{\process} \),
\(
\using{\corrupt{\process}}{\asyncstepsto!{}}
\simulatedBy
\using{\corrupt{\partition{\process}}}{\realstepsto{}}
\).

Let \( \simulator = \adv \).
<Ref> immediately
give a strong bisimulation.

§.§ Restoring Original Choreography Syntax

<Ref> proves the correctness of endpoint projection
for extended choreographies that have run-time terms.
Next, we show a simple simulation that a choreography
with run-time terms simulates one without,
removing the need to reason about run-time terms in other proof steps.

\( \ssecure[\emptylist]{\process} \),
\(
\using{\corrupt{\process}}{\realstepsto!{}}
\simulatedBy
\using{\corrupt{\process}}{\asyncstepsto!{}}
\).

The simulator follows the control flow by maintaining a public view of
the extended choreography
\( \using{\corrupt{\process}}{\asyncstepsto!{}} \)
and runs the adversary against this view.
The simulator behaves the same as the adversary,
except when the adversary schedules a run-time term,
the simulator takes an internal step
(and does not schedule the original choreography).

By <ref>
using the transitivity of UC simulation.

§ CRYPTOGRAPHIC INSTANTIATION

Our simulation result is a necessary and novel first step toward constructing a verified,
secure compiler for distributed protocols that use cryptography.
We have abstracted all cryptographic mechanisms into idealized hosts
(e.g., ); thus, to achieve a full end-to-end security proof,
these idealized hosts must be securely instantiated with cryptographic subprotocols (e.g.,
BGW <cit.> for multiparty computation).
Such an instantiation would imply UC security for all compiled programs,
in contrast to existing formalization efforts for individual protocols <cit.>.

To this end, we show how the distributed protocols arising from
our compilation correspond to hybrid protocols in the Simplified Universal
Composability (SUC) framework <cit.>.
Then, we show how to take advantage of the composition theorem
in SUC to obtain secure, concrete instantiations of cryptographic

Simplified UC

Let $\s$ be a choreography with partitioning $\partition{\s}$.
We construct a corresponding SUC protocol $\SUC{\s}$
which behaves identically to the partitioned choreography, with minor differences due
to the differing computational models.
Each host in $s$ is either a local host (e.g., ), or an idealized
host standing in for cryptography, such as . Local hosts
map onto SUC parties, while idealized hosts map onto ideal functionalities in SUC.

Protocol execution in SUC happens through
activations scheduled by the adversary: a party runs for some steps,
delivers messages to a central router, and cedes execution to the
adversary. To faithfully capture the behavior of host in $\partition{\s}$,
the party/functionality for in $\SUC{\s}$ is essentially a wrapper
around the projected host $\project{\s}$, who steps $\project{s}$ accordingly
and forwards correct messages to the router.

Each wrapper needs to explicitly model corruption, which our
framework captures by labels: if host $\h$ is semi-honest
($\semihonest{\h}$), the wrapper for $\h$ allows the adversary to query
$\h$ for its current message transcript so far. Similarly, if $\h$ is malicious
($\malicious{\h}$), the wrapper for $\h$ should enable the adversary to
take complete control over $\h$.
By using labels to model corruption, we model static security in SUC.

Communication Model

In SUC, all messages between local hosts are fully public, while messages
between hosts and functionalities contain public headers (e.g., the
source/destination addresses) and private content (the message payload).
In our system, we do not stratify message privacy along the
party/functionalities axis, but rather along the information flow lattice:
the adversary can read the messages intended for semi-honest hosts, and can forge
messages from malicious hosts.
Indeed, information flow policies allow
more flexible security policies for communication.

However, we can encode our communication model into SUC with the aid of
additional functionalities.
To do so, we make use of a secure channel functionality $\mathcal{R}_\mathsf{sec}$,
which guarantees in-order message delivery and enables secret communication between
honest hosts.
We can realize $\mathcal{R}_\mathsf{sec}$ in SUC via a standard subprotocol using
a public key infrastructure.

For ideal functionalities in $\SUC{\s}$, we need to
ensure that they only communicate with local hosts, and not with other ideal
This property is preserved by compilation, so we only need to
ensure that host selection produces a choreography $\s$ that has this property.
Indeed, our synchronization judgment $\ssynched{\s}$ makes it possible for
choreographies to stay well-synchronized, even when the ideal hosts do not
communicate with each other.

Adversaries and Environments

In our framework, we prove perfect security against non-probabilistic
However, allowing the adversary to use probability (as in SUC) does not weaken
our simulation result.[
The dummy adversary theorem <cit.> implies that security against
non-probabilistic adversaries guarantees security against probabilistic
Additionally, in UC/SUC, the environment is given by a concurrently running
process that outputs a decision bit, whereas our model uses a trace
semantics to model the environment.
Security for the latter easily implies the
former, since our simulation result proves equality of environment views between
the two worlds.

Finally, UC (and SUC) require all parties—the adversary,
environment, simulator, and hosts—to run in polynomial time since
cryptographic schemes can be broken given enough time.
Since our simulators query the adversary
and emulate source and target programs in a straightforward manner,
all simulators we define run in time bounded by a polynomial
in the run times of the adversary and the source and target programs.

§.§ Secure Instantiation of Cryptography

To securely instantiate cryptographic mechanisms, we appeal
to the composition theorem in SUC, which says that ideal
SUCfunctionalities $\mathcal{F}$ may be substituted for SUC protocols that
securely realize them. Concrete cryptographic protocols are
obtained by applying this theorem iteratively to each ideal host.

Ideal hosts in our model correspond closely to the broad class of
reactive, deterministic
straight-line functionalities in SUC, including MPC <cit.> and
Zero-Knowledge Proofs (ZKP) <cit.>.
The main difference is that our model allows the
adversary to corrupt ideal functionalities (both semi-honestly and maliciously),
while SUC functionalities are incorruptible.
However, we guarantee that the adversary does not gain more power in our model by
restricting the possible corruption models via authority labels for ideal hosts.

For example, we have has label $\iflabel{A \wedge B}$,
meaning that
is semi-honest (resp. malicious) only if both and
are semi-honest (resp. malicious). Thus, any power the adversary gains in
corrupting can be instead achieved using and alone.
Similar security concerns for label-based host
selection have been discussed for Viaduct <cit.>.
We can formalize this intuition via a simulation of the form
$\using{\config}{\idealstepsto{}} \simulates \using{\config}{\idealstepsto{}'}$,
where $\config$ uses $\MPCalicebob$, and $\idealstepsto{}'$ is modified so that
corruption of $\MPCalicebob$ is impossible.

§ SECURITY PRESERVATION

We use simulation to define the correctness of compilation, and show
that it corresponds to a well-studied correctness criterion,
robust hyperproperty preservation (RHP) <cit.>.
RHP states that hyperproperties <cit.> satisfied by source programs
under any context are also satisfied by target programs under any context.
RHP is important because common notions of information-flow
security such as termination-insensitive noninterference, observational
determinism <cit.>, and nonmalleable information flow control <cit.>
are hyperproperties.
With a compiler that satisfies RHP, one only needs to prove
security of source programs; security of target programs immediately

Let $\compile{}$ be a compiler from a source program to a target program,
$\progcompose$ be an operator that composes a program with its context,
and $\behavior$ be a behavior function that returns the set of possible
traces generated from a whole program (i.e., a program composed with a
Then $\compile{}$ satisfies RHP
over source program set $\prog!$, source context set !,
and target context set ! when,
given program $\prog \in \prog!$,
for all $\targetctx \in \targetctx!$
there exists $\srcctx \in \srcctx!$ such that
$\behavior(\srcctx \progcompose \prog)
= \behavior(\targetctx \progcompose \compile{\prog})$.[
This is the “property-free” definition of RHP as given by <cit.>.
An equivalent but more direct definition is that $\compile{}$ satisfies RHP
given that if for some hyperproperty HP it is the case that
$\behavior(\srcctx \progcompose \prog) \in \mathrm{HP}$
for any $\srcctx \in \srcctx!$,
then $\behavior(\targetctx \progcompose \compile{\prog}) \in \mathrm{HP}$
for any $\targetctx \in \targetctx!$.

previously observed a correspondence between
UC simulation and robust hyperproperty preservation;
it also holds for our notion of simulation.

Define \(\adv \progcompose \config = \adv \parallel \config\).
Then given behavior function $\behavior(\cdot) = \envtraces{\cdot}$
and an operator \(\compile{}\) between configurations such that
\(\compile{\config} \simulates \config\) for any configuration
\(\config \in \config!\), we have that
\(\compile{}\) satisfies RHP over source program set ! and
source and target context set \(\set{\adv}\).

The function
$\lambda \process. \using{\corrupt{\partition{\process}}}{\realstepsto{}}$
satisfies RHP over source and target context set $\set{\adv}$ and
source program set

\[
\{ \using{\source{\process}}{\idealstepsto{}} \mid
\ssecure[\emptylist]{\process}, \ssynched[\sctx]{\process} \}
\]

<Ref> follows from <ref>.
<Ref> follows from

§ RELATED WORK

§.§.§ Secure Program Partitioning and Compilers for Secure Computation

Prior work on secure program partitioning <cit.>
focuses largely on the engineering effort of compiling security-typed
source programs to distributed code with the aid of cryptography.
does give an informal UC simulation proof of a compiler, but it
is limited to two party semi-honest MPC and oblivious RAM, and they do not
consider integrity.

There is also a large literature on compilers for secure computation
that target specific cryptographic mechanisms such as
MPC <cit.>,
ZKP <cit.>,
and homomorphic encryption <cit.>.
Again, the focus of this literature is efficient implementations, not formal

A long line of work <cit.>
focuses on enforcing computational noninterference for information-flow typed
programs by using standard cryptographic mechanisms, such as encryption.
However, computational noninterference guarantees little
in the presence of downgrading.
In contrast, our compiler enjoys simulation-based security,
which guarantees preservation of all hyperproperties, even
for programs using declassification and endorsement.

Our compilation model is closest to that of Viaduct <cit.>,
which like this work also approximates security guarantees of cryptographic
mechanisms with information-flow labels.
However, this work differs from Viaduct, and from most of the literature
on secure program partitioning and compilers for secure computation, in that our
goal is to provide a model of a secure end-to-end compilation process,
not to provide an implementation of an actual compiler.
Our model currently does not analyze a source language with functions, loops, or
mutable arrays, which Viaduct supports.
Additionally, our model does not capture some minor subtleties of Viaduct, such
as allowing secret-dependent conditionals whenever they may be eliminated via
multiplexing the two branches.
An interesting research direction would be to close the gap between our model
and existing compilers by providing a verified compiler implementation akin to
CompCert <cit.>.

§.§.§ Simulation-based Security

Simulation-based cryptographic frameworks, such as
Universal Composability <cit.>,
Reactive Simulatability <cit.>, and
Constructive Cryptography <cit.>,
allow modular proofs of distributed cryptographic protocols,
and <cit.> give a core language for formalizing UC protocols.
We abstract away concrete cryptography, so
we do not explicitly model some subtleties of these systems:
probability, computational complexity, and cryptographic
hardness assumptions. But
our approach should be compatible with these frameworks.

Prior verification efforts <cit.>
show simulation-based security for concrete
cryptographic mechanisms.
Our work is orthogonal: simulation-based
security for compiler correctness, rather than
proofs for individual protocols.

§.§.§ Secure Compilation

Standard notions of compiler correctness
are derived from full abstraction and hyperproperty preservation <cit.>.
argue that robust hyperproperty preservation
and Universal Composability are directly analogous.
We affirm this hypothesis by proving that our simulation-based security result
guarantees RHP.
To our knowledge, we are the first to make this connection formally.

§.§.§ Choreographies

The use of choreographies is central to our compilation process
and to the proof of its correctness. The primary concern in the
extensive literature on choreographies <cit.>,
is proving deadlock freedom;
very little prior work considers security <cit.>.
Our extension of choreographies with an information-flow type system,
modeling semi-honest and malicious corruption, is novel.

§ CONCLUSION AND FUTURE WORK

This work presents a novel simulation-based security result for
a compiler from sequential source programs to distributed programs,
using idealizations of cryptographic mechanisms.
Our simulation result guarantees that the security properties
of source programs are preserved in the compiled protocols.

We believe this work opens up many opportunities for future research;
in particular, it gives a clear path toward building a fully verified
cryptographic compiler.
Aside from adding more language features (e.g., subroutines, loops, and mutable arrays)
to our source language to better match real-world cryptographic compilers,
the remaining verification effort largely consists of verifiably instantiating
all abstract components we assume.
For example, we model protocol selection via abstract judgments on
choreographies; in turn, outputs of a concrete protocol selection algorithm must satisfy these
Additionally, we assume that parties communicate over secure channels, and use
ideal functionalities for performing cryptography; these
assumptions can be eliminated using cryptographic instantiations verified in the Simplified UC framework.

Our security result holds for a strong attacker that knows when
communication occurs between hosts and controls its scheduling,
but secret control flow is therefore precluded.
To improve expressive power, weaker attacker models should be explored.

We have focused on confidentiality and integrity properties; however,
some protocols also explicitly address availability <cit.>,
which would be another interesting direction for exploration.

§ ACKNOWLEDGMENTS

This work was supported by the
National Science Foundation under
NSF grant 1704788. Any opinions, findings, conclusions or recommendations
are those of the authors and do not necessarily reflect the views of
any of these funders.
We thank the reviewers for their thoughtful suggestions.
We also thank
Silei Ren,
Ethan Cecchetti,
Drew Zagieboylo,
and Suraaj Kannawadi
for discussions and feedback.