# Logical Relations for Session-Typed Concurrency

Stephanie Balzer  Carnegie Mellon UniversityUSA ,  Farzaneh Derakhshan
Illinois Institute of TechnologyUSA ,  Robert Harper  Carnegie Mellon
UniversityUSA and  Yue Yao  Carnegie Mellon UniversityUSA

###### Abstract.

Program _equivalence_ is the fulcrum for reasoning about and proving
properties of programs. For noninterference, for example, program equivalence
up to the secrecy level of an observer is shown. A powerful enabler for such
proofs are _logical relations_. Logical relations only recently were adopted
for session types—but exclusively for terminating languages. This paper scales
logical relations to _general recursive session types_. It develops a logical
relation for progress-sensitive noninterference (PSNI) for intuitionistic
linear logic session types (ILLST), tackling the challenges non-termination
and concurrency pose, and shows that logical equivalence is _sound and
complete_ with regard to closure of weak bisimilarity under parallel
composition, using a _biorthogonality_ argument. A distinguishing feature of
the logical relation is its stratification with an _observation index_ (as
opposed to a step or unfolding index), a crucial shift to make the logical
relation closed under parallel composition in a concurrent setting. To
demonstrate practicality of the logical relation, the paper develops an
information flow control (IFC) _refinement type system_ for ILLST, with
support of secrecy-polymorphic processes, and shows that well-typed programs
are self-related by the logical relation and thus enjoy PSNI. The refinement
type system has been implemented in a type checker, featuring local security
theories to support secrecy-polymorphic processes.

Logical relations, step-indexing, biorthogonality, intuitionistic linear logic
session types, progress-sensitive noninterference

††ccs: Theory of computation Linear logic††ccs: Security and privacy Logic and
verification††ccs: Theory of computation Process calculi††ccs: Theory of
computation Type theory

##  1\. Introduction

Whether two programs are _equivalent_ is at the heart of many program
verification problems, such as proofs of parametricity, compiler correctness,
and noninterference. Noninterference is a security property that guarantees
that a program’s confidential data cannot be leaked to a (malicious) observer.
This paper develops a _logical relation_ to reason about program equivalence
of _session-typed processes_ , proves soundness and completeness of the
relation via a _biorthogonality_ argument, and instantiates it on
_noninterference_.

##### Message-passing concurrency

Message-passing is a prevalent concurrency paradigm, rooted in process calculi
(Hoare, 1985; Milner, 1980, 1989) and adopted by practical languages such as
Erlang, Go, and Rust. A program in this setting amounts to a number of
_processes_ connected by _channels_ , which compute by exchanging _messages_
along these channels. The $\pi$-calculus (Milner, 1999; Sangiorgi and Walker,
2001), among these calculi, sets itself apart in its support of _higher-order_
channels, admitting channels themselves to be sent as messages over channels.
This feature is equally empowering as daunting because it allows the process
topology to be changed dynamically. Conceived as an untyped calculus (Milner,
1999), the $\pi$-caluclus has gradually been enriched with types (Sangiorgi
and Walker, 2001) to prescribe the kinds of messages that can be exchanged
over a channel. More advanced type systems for the $\pi$-caluclus additionally
assert correctness properties, such as deadlock freedom and data race freedom
(Kobayashi, 1997; Igarashi and Kobayashi, 2001, 2004; Kobayashi, 2006).

To prescribe not only the types of exchanged messages but also the _protocol_
underlying the exchange, _session types_ (Honda, 1993; Honda et al., 1998)
were introduced. Session types rely on a _linear_ treatment of channels to
model the state transitions induced by a protocol. This foundation is
substantiated by a Curry-Howard correspondence between linear logic and the
session-typed $\pi$-calculus (Caires and Pfenning, 2010; Wadler, 2012),
resulting in two families of session type languages: _intuitionistic linear
logic session types (ILLST)_ (Caires and Pfenning, 2010; Toninho et al., 2013;
Caires et al., 2016) and _classical linear logic session types (CLLST)_
(Wadler, 2012; Lindley and Morris, 2015, 2016). Due to their logical
foundation both ILLST and CLLST guarantee that well-typed processes are free
of data races and deadlocks (a.k.a., progress) and protocol-compliant (a.k.a.,
preservation).

This paper studies logical relations for ILLST-typed processes. ILLST reject
linear negation and distinguish the provider side from the client side of a
channel. Run-time configurations of processes will thus give raise to a
_rooted tree_ , with a child node as the provider and a parent node the
client.

##### Program equivalence

Today’s predominant techniques for reasoning about program equivalence of
stateful programs are Kripke logical relations (KLRs) (Pitts and Stark, 1998;
Ahmed et al., 2009; Dreyer et al., 2010; Neis et al., 2011; Hur and Dreyer,
2011; Thamsborg and Birkedal, 2011) and bisimulations (Koutavas and Wand,
2006; Sumii and Pierce, 2007; Støvring and Lassen, 2007; Sangiorgi et al.,
2007). KLRs tend to be used for sequential, ML-like languages, bisimulations
for process calculi, i.e., concurrent languages. KLRs are naturally phrased by
structural induction on the types of the underlying language, bisimulations by
coinduction in terms of the functional associated to the bisimulation
(Sangiorgi, 2012). Hur et al. (2012) note that KLRs and bisimulations offer /
suffer from complementary advantages / limitations. Whereas KLRs easily
support higher-order features thanks to extensionality, but struggle with
recursive types, bisimulations easily support recursive features thanks to
coinduction, but struggle with higher-order features. Support of recursive
types in KLRS necessitates step-indexing (Appel and McAllester, 2001; Ahmed,
2004, 2006) to stratify the logical relation. Step-indexed KLRs, however,
challenge transitivity of the logical relation (Hur et al., 2012).

This paper scales logical relations to session-typed concurrency in the
presence of general recursive types, contributing a _recursive session logical
relation (RSLR)_. In contrast to KLRs with recursive types, RSLRs use an
_observation index_ to stratify the logical relation. An observation index is
associated with the free channels connecting a program with the outside world
and bounds the number of messages exchanged along these channels. Associating
the index with an externally observable event, i.e., a message being sent,
rather than an internal computation step, naturally ensures _transitivity_ of
RSLRs and _closure_ under parallel composition. We show that RSLRs are _sound
and complete_ with regard to closure of weak _bisimilarity_ under parallel
composition, using a _biorthogonality_ argument à la Pitts (2000). The
inherent _duality_ of session types establishes a natural connection to
biorthogonality.

##### Noninterference

A property naturally phrased as a program equivalence is _noninterference_.
Noninterference states that an observer cannot infer any secrets from made
observations. To prove noninterference one has to show that a program $P$ is
related to itself, $P=_{\xi}P$, up to the secrecy level of the observer $\xi$.
The ”up to” part of the equality means that only outcomes of level
$\sqsubseteq\xi$ can be discriminated, whereas outcomes of level
$\not\sqsubseteq\xi$ are trivially related. It may be helpful to pause a
moment to understand why noninterference is stated as a program equivalence.
After all, observations can only be made about the execution of _one_ program.
What is being related are different executions of a program, accounting for
the possibility that an observer can make different observations when a
program branches on a secret. For example, consider a scenario in which, when
branching on a secret bit, the message “left” is sent along an observable
channel $x$ when the bit is true, and the message “right” otherwise. Assuming
that an observer of $x$ has access to the source code of the program, seeing
either “left” or “right” in this scenario is sufficient to deduce that the
secret bit is true or false, resp.

The question of equivalence becomes subtle in the presence of divergence,
leading to different definitions of noninterference. If divergence is a
possible outcome, _progress-sensitive_ noninterference (PSNI) only allows
equating a divergent program run with another diverging one, whereas
_progress-insensitive_ noninterference (PINI) allows equating a divergent
program run with any other outcome (Heidin and Sabelfeld, 2011). PSNI provides
a stronger guarantee, especially in a concurrent setting, where the
_termination channel_ (Sabelfeld and Myers, 2003) can be scaled to many
parallel computations, each leaking “just” one bit (Stefan et al., 2012;
Alpernas et al., 2018).

This paper instantiates the developed logical relation on noninterference,
yielding a RSLR for PSNI. Moreover, the paper develops an information flow
control refinement type system for ILLST, facilitating proof of PSNI by type
checking.

##### Information flow control

Type systems for _information flow control (IFC)_ assert noninterference by
type checking (Volpano et al., 1996; Smith and Volpano, 1998; Sabelfeld and
Myers, 2003). Given a lattice over security levels and labeling of observables
(e.g., output, locations, channels) with these levels, typing prevents ”flows
from high to low”. _Flow-sensitive_ IFC type system additionally track the
current level of information obtained up to the current program point,
accounting for a program’s control flow and yielding a more fine-grained
analysis.

This paper contributes a flow-sensitive IFC type system as a _refinement_ of
ILLST, extended with general recursive types. Using the RSLR developed in this
paper, we prove that well-typed processes in this refinement type system enjoy
PSNI. The refinement type system has been implemented in a type checker,
featuring local security theories to support secrecy-polymorphic processes.

##### Contributions

  * •

_Recursive session logical relation (RSLR)_ , a logical relation for progress-
sensitive program equivalence for ILLST with general recursion. A
distinguishing feature of the RSLR is an _observation index_ , facilitating a
more extensional definition of the term interpretation, in which internal
computations do not advance the index.

  * •

Proof that the RSLR is _closed_ under _parallel composition_ and induces a
_logical equivalence_.

  * •

Soundness and completeness of the RSLR with regard to _asynchronous
bisimilarity_.

  * •

Biorthogonal ($\top\top$-) closure of induced logical equivalence with regard
to closure of weak bisimilarity under parallel composition.

  * •

Instantiation of RSLR for PSNI, for an IFC refinement type system with
secrecy-polymorphic process definitions, with a type checker implementation
and metatheory.

##### Supplementary material

We provided the formalization with proofs in a technical report (Balzer et
al., 2023).

##  2\. Foundations and application

This section familiarizes with ILLST (Caires and Pfenning, 2010; Toninho et
al., 2013; Caires et al., 2016) and information flow concerns using a banking
example.

###  2.1. Running example

Let’s assume that our bank has two customers, Alice and Bob, with accounts
each. In a secure system, we expect that Alice’s account can only be queried
by Alice or the bank, but neither by Bob or any walk-in customer (”guest”).
The same must hold for Bob. We can express this policy by defining
corresponding secrecy levels and a lattice over them:

$\mathbf{guest}\sqsubseteq\mathbf{alice}\sqsubseteq\mathbf{bank}\qquad\mathbf{guest}\sqsubseteq\mathbf{bob}\sqsubseteq\mathbf{bank}$

Fig. 1 (a) shows two process configurations for our example, before and after
a message exchange. The process configuration on the left consists of the
$\mathsf{Bank}$ process, the customer processes $\mathsf{Alice}$ and
$\mathsf{Bob}$, along with their bank account processes $\mathsf{aAcc}$ and
$\mathsf{bAcc}$, resp., and corresponding processes for authentication. The
latter comprise, per customer, an authorization process ($\mathsf{\\_Auth}$),
which provides access to a customer’s bank account ($\mathsf{\\_Acc}$), given
successful authentication by a verifier process ($\mathsf{\\_Ver}$) using the
customer’s PIN ($\mathsf{\\_Pin}$). The process configuration on the right
shows the configuration after Alice’s authorization process has sent Alice’s
PIN to Alice’s verifier ($\mathbf{send}\,u\,x$) for authentication. The
message being sent is a channel, which is treated _linearly_ in ILLST. As a
result, the exchange alters the connectivity structure of the configuration.

Figure 1. Running example: (a) pre-/post-state of process configurations, (b)
session types.

The session types governing the banking example are shown in Fig. 1 (b). In
this paper, we use the language SESSION, which is an ILLST language in the
spirit of (Toninho, 2015), extended with general recursive types. Table 1
provides an overview of SESSION’ types and terms. A crucial—and probably
unusual—characteristics of session-typed processes is that a process _changes_
its type along with the messages it exchanges. As a result, a process’ type
always reflects the current protocol state. Table 1 lists state transitions
caused by a message exchange in the first and second column and corresponding
process terms in the third and fourth column. The fifth column describes the
computational behavior of a type and the last column its polarity. Positive
types have a sending semantics, negative types a receiving semantics. SESSION
supports recursive type definitions of the form $Y=A$ where $Y$ is a type
variable that occurs in $A$. Recursive types must be _contractive_ (Gay and
Hole, 2005), demanding a message exchange before recurring, and _equi-
recursive_ (Crary et al., 1999), avoiding explicit (un)fold messages and
relating types up to their unfolding.

Table 1. Overview of SESSION language constructs. Upper half: types and terms (before and after exchange), computational behavior, and polarity. Lower half: terms and computational behavior of judgmental rules. Session type (b/a) | Process term (b/a) |  Description (provider, client) | polarity
---|---|---|---
$x{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in L}$ | $x{:}A_{k}$ | $x.k;P$ | $P$ |  pr sends label $k$ along $x$, continues with $P$ | $+$
|  | $\mathbf{case}\,x(\ell{\Rightarrow}Q_{\ell})_{\ell\in L}$ | $Q_{k}$ |  cl receives label $k$ along $x$, continues with $Q_{k}$
$x{:}\&\\{\ell{:}A_{\ell}\\}_{\ell\in L}$ | $x{:}A_{k}$ | $\mathbf{case}\,x(\ell{\Rightarrow}P_{\ell})_{\ell\in L}$ | $P_{k}$ |  pr receives label $k$ along $x$, continues with $P_{k}$ | $-$
|  | $x.k;Q$ | $Q$ |  cl sends label $k$ along $x$, continues with $Q$
$x{:}A\otimes B$ | $x{:}B$ | $\mathbf{send}\,y\,x;P$ | $P$ |  pr sends channel $y{:}A$ along $x$, continues with $P$ | $+$
|  | $z{\leftarrow}\mathbf{recv}\,x;Q_{z}$ | ${Q_{y}}$ |  cl receives channel $y{:}A$ along $x$, continues with $Q_{y}$
$x{:}A\multimap B$ | $x{:}B$ | $z{\leftarrow}\mathbf{recv}\,x;P_{z}$ | ${P_{y}}$ |  pr receives channel $y{:}A$ along $x$, continues with $P_{y}$ | $-$
|  | $\mathbf{send}\,y\,x;Q$ | $Q$ |  cl sends channel $y{:}A$ along $x$, continues with $Q$
$x{:}1$ | - | $\mathbf{close}\;x$ | - |  pr sends “$\mathsf{end}$” along $x$ and terminates | $+$
|  | $\mathbf{wait}\;x{Q}$ | $Q$ |  cl receives “$\mathsf{end}$” along $x$, continues with Q
$x{:}Y$ | $x{:}A$ | - | - |  recursive type definition $Y=A$ ($Y$ occurs in $A$)
Judgmental rules | Description
$x\leftarrow X[\gamma]\leftarrow\Delta;Q_{x}$ |  spawn $X$ along $x$ with arguments $\Delta$ and substitution $\gamma$, continue with $Q_{x}$
$x\leftarrow y$ |  forward $x{:}A$ to $y{:}A$

The session types in our banking example dictate the following protocol: When
a customer opens an account with the bank, the bank sends them a PIN and
authorization process ($\mathsf{customer}$). A customer can now repeatedly
query their account’s balance ($\mathit{high}$, $\mathit{med}$,
$\mathit{low}$), preceding authentication. To authenticate themselves, a
customer sends their PIN to the authorization process. The authorization
process goes ahead and sends the received PIN to the verifier. If the
authentication by the verifier is successful, the verifier sends the message
$\mathit{succ}$ to the authorization process, otherwise the message
$\mathit{fail}$. In either case, the verifier returns the PIN to the
authorization process. The latter relays the outcome of the authentication to
the customer, yielding the bank account in case of $\mathit{succ}$ and the PIN
in case of $\mathit{fail}$. Once done, a customer returns the account to the
authorization process and receives their PIN, allowing them to start over.

###  2.2. ILLST type system

Before showing code that implements any of the processes in our example, we
provide a brief overview of SESSION’s statics, which is standard. The term
typing rules are given in Fig. 2, phrased as an _intuitionistic sequent
calculus_. Terms are typed using the sequent

$\Omega\vdash_{\Sigma}P::x{:}A$

to be read as “process $P$ provides a session of type $A$ along channel
variable $x$, given the typing of sessions offered along channel variables in
$\Omega$”. $\Omega$ is a _linear_ context that consists of a finite set of
assumptions of the form $y_{i}{:}B_{i}$, indicating for each channel variable
$y_{i}$ its session type $B_{i}$. Bound channel variables are subject to
$\alpha$-variance and capture-avoiding substitution, as usual. They are
substituted with channels that are created at run-time upon process spawning.
When the distinction is clear from the context we refer to either as “channel”
for brevity. ILLST rejects linear negation, allowing the singleton right-hand
side to be interpreted as the type of the _providing_ process, which,
conversely, is the _client_ of the sessions in $\Omega$. Although both
endpoints of a channel in ILLST are typed from the view of the provider, the
_duality_ in behavior is expressed by defining both _right_ and _left_ rules
per connective. Right rules define a communication from the point of view of
the provider, left rules from the point of view of the client. In case of a
positive connective, the provider sends, and the client receives, in case of a
negative connective, the provider receives, and the client sends.
Computationally, intuitionism translates into a _rooted tree_ of processes, as
evident in Fig. 1, where providers are child nodes and clients parent nodes.

$\displaystyle\displaystyle{\hbox{\hskip
46.21912pt\vbox{\hbox{\hskip-46.2191pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}P::x{:}A_{k}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in
L$}}}}\vbox{}}}\over\hbox{\hskip
50.95726pt\vbox{\vbox{}\hbox{\hskip-50.95724pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}x.k;P::x{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in
L}$}}}}}}$ $\oplus R$ $\displaystyle\displaystyle{\hbox{\hskip
53.80963pt\vbox{\hbox{\hskip-53.80963pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x{:}A_{k}\vdash_{\Sigma}Q_{k}::y{:}C\quad\forall
k\in L$}}}\vbox{}}}\over\hbox{\hskip
80.3172pt\vbox{\vbox{}\hbox{\hskip-80.31718pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x{:}\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L}\vdash_{\Sigma}\mathbf{case}\,x(\ell\Rightarrow Q_{\ell})_{\ell\in
L}::y{:}C$}}}}}}$ $\oplus L$

$\displaystyle\displaystyle{\hbox{\hskip
57.10121pt\vbox{\hbox{\hskip-57.10121pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}Q_{k}@c::x{:}A_{k}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall k\in
L$}}}}\vbox{}}}\over\hbox{\hskip
72.39075pt\vbox{\vbox{}\hbox{\hskip-72.39073pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}\mathbf{case}\,x(\ell\Rightarrow
Q_{\ell})_{\ell\in I}::x{:}\&\\{\ell:A_{\ell}\\}_{\ell\in L}$}}}}}}$ $\&R$
$\displaystyle\displaystyle{\hbox{\hskip
54.12495pt\vbox{\hbox{\hskip-54.12494pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x{:}A_{k}\vdash_{\Sigma}P::y{:}C$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in
L$}}}}\vbox{}}}\over\hbox{\hskip
61.34248pt\vbox{\vbox{}\hbox{\hskip-61.34247pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x{:}\&\\{\ell:A_{\ell}\\}_{\ell\in
I}\vdash_{\Sigma}x.k;P::y{:}C$}}}}}}$ $\&L$

$\displaystyle\displaystyle{\hbox{\hskip
25.04501pt\vbox{\hbox{\hskip-25.04501pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}P::x{:}B$}}}\vbox{}}}\over\hbox{\hskip
59.97319pt\vbox{\vbox{}\hbox{\hskip-59.97318pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,z{:}A\vdash_{\Sigma}\mathbf{send}\,z\,x;P::x{:}A\otimes
B$}}}}}}$ $\otimes R$ $\displaystyle\displaystyle{\hbox{\hskip
43.11649pt\vbox{\hbox{\hskip-43.11649pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,z{:}A,x{:}B\vdash_{\Sigma}P::y{:}C$}}}\vbox{}}}\over\hbox{\hskip
64.5759pt\vbox{\vbox{}\hbox{\hskip-64.57588pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x{:}A\otimes
B\vdash_{\Sigma}z\leftarrow\mathbf{recv}\,x;P::y{:}C$}}}}}}$ $\otimes L$

$\displaystyle\displaystyle{\hbox{\hskip
33.96065pt\vbox{\hbox{\hskip-33.96065pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,z{:}A\vdash_{\Sigma}P::x{:}B$}}}\vbox{}}}\over\hbox{\hskip
57.42006pt\vbox{\vbox{}\hbox{\hskip-57.42006pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}z\leftarrow\mathbf{recv}\,x;P::x{:}A\multimap
B$}}}}}}$ $\multimap R$ $\displaystyle\displaystyle{\hbox{\hskip
34.20085pt\vbox{\hbox{\hskip-34.20085pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x{:}B\vdash_{\Sigma}P::y{:}C$}}}\vbox{}}}\over\hbox{\hskip
71.12903pt\vbox{\vbox{}\hbox{\hskip-71.12903pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,z{:}A,x{:}A\multimap
B\vdash_{\Sigma}\mathbf{send}\,z\,x;P::y{:}C$}}}}}}$ $\multimap L$

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
33.48877pt\vbox{\vbox{}\hbox{\hskip-33.48877pt\hbox{\hbox{$\displaystyle\displaystyle\cdot\vdash_{\Sigma}\mathbf{close}\;x::x:1$}}}}}}$
$1R$ $\displaystyle\displaystyle{\hbox{\hskip
27.28334pt\vbox{\hbox{\hskip-27.28334pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}Q::y:C$}}}\vbox{}}}\over\hbox{\hskip
51.55212pt\vbox{\vbox{}\hbox{\hskip-51.55211pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,x:1\vdash_{\Sigma}\mathbf{wait}\,x;Q::y:C$}}}}}}$
$1L$

$\displaystyle\displaystyle{\hbox{\hskip
56.01851pt\vbox{\hbox{\hskip-56.0185pt\hbox{\hbox{$\displaystyle\displaystyle
Y=A\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash_{\Sigma}P::x{:}A$}}}}\vbox{}}}\over\hbox{\hskip
25.51845pt\vbox{\vbox{}\hbox{\hskip-25.51845pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash_{\Sigma}P::x{:}Y$}}}}}}$
$\mbox{\sc TVar}_{R}$ $\displaystyle\displaystyle{\hbox{\hskip
65.09724pt\vbox{\hbox{\hskip-65.09724pt\hbox{\hbox{$\displaystyle\displaystyle
Y=A\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,x{:}A\vdash_{\Sigma}P::z{:}C$}}}}\vbox{}}}\over\hbox{\hskip
34.5972pt\vbox{\vbox{}\hbox{\hskip-34.59718pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,x{:}Y\vdash_{\Sigma}P::z{:}C$}}}}}}$
$\mbox{\sc TVar}_{L}$

$\displaystyle\displaystyle{\hbox{\hskip
137.03804pt\vbox{\hbox{\hskip-137.03802pt\hbox{\hbox{$\displaystyle\displaystyle\Omega^{\prime}_{1}\vdash
X=P::x^{\prime}{:}A\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Omega_{1},x{:}A\Vdash\gamma::\Omega^{\prime}_{1},x^{\prime}{:}A$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Omega_{2},x{:}A\vdash_{\Sigma}Q::y{:}C$}}}}}\vbox{}}}\over\hbox{\hskip
66.98654pt\vbox{\vbox{}\hbox{\hskip-66.98653pt\hbox{\hbox{$\displaystyle\displaystyle\Omega_{1},\Omega_{2}\vdash_{\Sigma}(x\leftarrow
X[\gamma]\leftarrow\Omega_{1});Q_{x}::y{:}C$}}}}}}$ Spawn

$\displaystyle\displaystyle{\hbox{\hskip
147.14749pt\vbox{\hbox{\hskip-147.14749pt\hbox{\hbox{$\displaystyle\displaystyle
z^{\prime}:C\vdash F_{Y}=\mathtt{Fwd}_{C,y^{\prime}\leftarrow
z^{\prime}}::y^{\prime}{:}C\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle Y=C\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
z^{\prime}{:}C,y^{\prime}{:}C\Vdash\gamma::z{:}C,y{:}C$}}}}}\vbox{}}}\over\hbox{\hskip
35.5005pt\vbox{\vbox{}\hbox{\hskip-35.5005pt\hbox{\hbox{$\displaystyle\displaystyle
z{:}Y\vdash_{\Sigma}F_{Y}[\gamma]::y{:}C$}}}}}}$ D-Fwd

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
17.59502pt\vbox{\vbox{}\hbox{\hskip-17.59502pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma}(\cdot)\;\mathbf{sig}$}}}}}}$
$\Sigma_{1}$ $\displaystyle\displaystyle{\hbox{\hskip
44.37057pt\vbox{\hbox{\hskip-44.37056pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma}A\mathbf{contr}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma}\Sigma^{\prime}\mathbf{sig}$}}}}\vbox{}}}\over\hbox{\hskip
30.52554pt\vbox{\vbox{}\hbox{\hskip-30.52553pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma}Y=A,\Sigma^{\prime}\mathbf{sig}$}}}}}}$
$\Sigma_{2}$ $\displaystyle\displaystyle{\hbox{\hskip
49.31898pt\vbox{\hbox{\hskip-49.31898pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\vdash_{\Sigma}P::x{:}A$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma}\Sigma^{\prime}\mathbf{sig}$}}}}\vbox{}}}\over\hbox{\hskip
52.40022pt\vbox{\vbox{}\hbox{\hskip-52.40022pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma}\Omega\vdash_{\Sigma}X=P::x{:}A,\Sigma^{\prime}\mathbf{sig}$}}}}}}$
$\Sigma_{3}$

Figure 2. Process term typing rules and signature checking rules of SESSION.

We briefly comment on the rules. Cut reduction in the sequent calculus invites
a computational, bottom-up reading of the rules, where the type of the
conclusion denotes the protocol state of the provider before the message
exchange and the type of the premise the protocol state after the message
exchange. For example, in case of an _internal choice_ , the right rule
$\oplus R$ chooses the $k$-th summand and then transitions to offering the
session $A_{k}$. The converse is true for the left rule $\&L$ of an _external
choice_ , where the client makes the choice. For $\otimes R$ and $\multimap L$
we chose _free outputs_ over _bound outputs_ (Sangiorgi and Walker, 2001) for
convenience; bound outputs stand in direct correspondence to intuitionistic
linear logic and computationally amount to spawning a new process and sending
the resulting channel. Our rules are derivable from the latter by spawning and
sending a forwarding process. To support general recursive types, SESSION
provides a top-level _signature_ $\Sigma$ of type definitions $Y=A$ and
process definitions $\Omega\vdash X=P::x{:}A$, and process term typing is
carried out relative to this signature. The rules $\Sigma_{1}$, $\Sigma_{2}$,
and $\Sigma_{3}$ type check the signature itself. Rule $\Sigma_{3}$ type
checks the body $P$ of a process definition $X$, whose existence is assumed
when spawning the process in rule Spawn. Rule Spawn requires a mapping
$\gamma$ of variables provided as arguments to the call ($\Omega_{1}$) to the
local variables of the process definition ($\Omega_{1}^{\prime}$). Rule D-Fwd
is phrased for a forwarder variable $F_{Y}$ with a type variable
$Y=C\in\Sigma$, assuming that $F_{Y}$ is defined in the signature as
$z^{\prime}:C\vdash F_{Y}=\mathtt{Fwd}_{C,y^{\prime}\leftarrow
z^{\prime}}::y^{\prime}{:}C$. A corresponding forwarder
$\mathtt{Fwd}_{C,y^{\prime}\leftarrow z^{\prime}}$ of type $C$ is defined by
structural induction on the type of every user-provided type definition,
amounting to an _identity expansion_ , and can be automatically generated. In
combination with rule D-Fwd, we get a coinductive definition. (see Def.
LABEL:APX:apx:def:fwder on page LABEL:APX:apx:def:fwder in the Appendix for
further details). As a result, Table 1 admits the forwarder-agnostic syntax
$y\leftarrow z$, which will be replaced internally by the forwarder for the
corresponding type.

###  2.3. Information flow

It’s now time to look at some code! Fig. 3 shows, on the left, the process
definitions $\mathsf{aVerifier}$ and $\mathsf{aPin}$ of types $\mathsf{ver}$
and $\mathsf{pin}$, resp., for Alice. A process definition consists of typing
and variable binding (first two lines) and body (after $=$). The first line
indicates the typing of channel variables used by the process (left of
$\vdash$) and the type of the providing channel variable (right of $\vdash$).
The former are going to be child nodes of the process. The second line binds
the channel variables. In SESSION, $\leftarrow$ generally denotes variable
bindings. Both $\mathsf{aVerifier}$ and $\mathsf{aPin}$ are leaves and thus do
not have any variables occurring on the left of $\vdash$. We leave it to the
reader to convince themselves, consulting Table 1 and Fig. 2, that the code in
the body of the two processes execute the protocol defined by their session
types. A tail call is syntactic sugar for a spawn combined with a forward;
i.e., $u\leftarrow\mathsf{aPin}\leftarrow\cdot$ desugars to
$u^{\prime}\leftarrow\mathsf{aPin}\leftarrow\cdot;u\leftarrow u^{\prime}$.

$\cdot\vdash\mathsf{aVerifier}::x{:}\mathsf{ver}$
---
$x\leftarrow\mathsf{aVerifier}\leftarrow\cdot=(u\leftarrow\mathbf{recv}\,x$
|  // $u{:}\mathsf{pin}\vdash
x{:}\oplus\\{\mathit{succ}:\mathsf{pin}\otimes\mathsf{ver},\mathit{fail}{:}\mathsf{pin}\otimes\mathsf{ver}\\}$
| $\mathbf{case}\,u\,($ | $\mathit{tok}_{j}\Rightarrow x.\mathit{succ};\mathbf{send}\,u\,x;x\leftarrow\mathsf{aVerifier}\leftarrow\cdot$
|  |  $\mid\mathit{tok}_{i\neq j}\Rightarrow x.\mathit{fail};\mathbf{send}\,u\,x;x\leftarrow\mathsf{aVerifier}\leftarrow\cdot))$
$\cdot\vdash\mathsf{aPin}::u{:}\mathsf{pin}$
$u\leftarrow\mathsf{aPin}\leftarrow\cdot=(u.\mathit{tok_{j}};u\leftarrow\mathsf{aPin}\leftarrow\cdot)$

$y{:}\mathsf{observer}\vdash\mathsf{SneakyVerifier}::x{:}\mathsf{ver}$
---
$x\leftarrow\mathsf{SneakyVerifier}\leftarrow y=(u\leftarrow\mathbf{recv}\,x$
| $\mathbf{case}\,u\,($ |  $\mathit{tok}_{j}\Rightarrow$ |  $x.\mathit{succ};y.\mathit{s};\mathbf{send}\,u\,x;$
|  |  | $x\leftarrow\mathsf{SneakyVerifier}\leftarrow y$
|  |  $\mid\mathit{tok}_{i\neq j}\Rightarrow$ | $x.\mathit{fail};y.\mathit{f};\mathbf{send}\,u\,x;$
|  |  |  $x\leftarrow\mathsf{SneakyVerifier}\leftarrow y))$
$\mathsf{observer}=\&\\{\mathit{s}{:}\mathsf{observer},\mathit{f}{:}\mathsf{observer}\\}$

Figure 3. Two implementations of the verifier process: (left) secure version,
(right) insecure version.

While session types ensure that messages are exchanged at run-time according
to the protocol specified by the session type, they leave unconstrained the
propagation of secret information. For example, a villain verifier could send
a customer’s PIN to an observer, amounting to a _direct_ leak of information.
More subtle forms of information leaks are _indirect_ , exploiting branching
to convey secret information. This strategy is taken by process
$\mathsf{SneakyVerifier}$, shown on the right in Fig. 3. It signals to an
observer whether the customer authenticated themselves successfully or not by
either sending the label $\mathit{s}$ or $\mathit{f}$, resp. While the above
example leaks by virtue of sending an actual message, the _absence_ of a
message due to non-termination can also be exploited for leaking confidential
information. Especially in a concurrent setting, this _termination covert
channel_ (Sabelfeld and Myers, 2003) can be scaled to many parallel
computations, each leaking “just” one bit (Stefan et al., 2012; Alpernas et
al., 2018) (see Sect. LABEL:APX:subsec:leaking-example on page
LABEL:APX:subsec:leaking-example in the Appendix for further examples).

###  2.4. ILLST configuration typing and asynchronous dynamics

To prevent information leakage, we develop a logical relation for program
equivalence in the next section. We then instantiate the relation for
noninterference in § 4, with the goal to ensure that our
$\mathsf{SneakyVerifier}$ is not self-related. Before introducing the logical
relation, we review the configuration typing and dynamics of SESSION, as it
allows us to convey some subtle points about linearity, relevant to the
subsequent sections.

The configuration typing rules of SESSION are given in Fig. 4, the dynamics in
Fig. 5. The latter is _asynchronous_ and phrased as multiset rewriting rules
(Cervesato and Scedrov, 2009). Multiset rewriting rules express the dynamics
as state transitions between configurations and are _local_ in that they only
mention the parts of a configuration they rewrite. Configurations consist of a
set of processes of the form $\mathbf{proc}(y_{\alpha},\hat{\delta}(P))$ and a
set of message processes of the form $\mathbf{msg}(M)$. The metavariable
$y_{\alpha}$ in $\mathbf{proc}(y_{\alpha},\hat{\delta}(P))$ denotes the
process’ providing channel and the metavariable $P$ the process’ source code.
Run-time channels $y_{\alpha}$ can be distinguished from channel variables $y$
by their generation subscript $\alpha$, whose meaning we clarify shortly. The
substitution mapping $\delta$ maps variables to channels; $\hat{\delta}(P)$
thus yields the term being executed at run-time.

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
30.61787pt\vbox{\vbox{}\hbox{\hskip-30.61786pt\hbox{\hbox{$\displaystyle\displaystyle
x_{\alpha}{:}A\Vdash\cdot::(x_{\alpha}{:}A)$}}}}}}$ $\mathbf{emp}_{1}$
$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
15.25002pt\vbox{\vbox{}\hbox{\hskip-15.25pt\hbox{\hbox{$\displaystyle\displaystyle\cdot\Vdash\cdot::(\cdot)$}}}}}}$
$\mathbf{emp}_{2}$ $\displaystyle\displaystyle{\hbox{\hskip
52.772pt\vbox{\hbox{\hskip-52.77199pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{0}\Vdash\mathcal{C}::\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta^{\prime}_{0}\Vdash\mathcal{C}_{1}::x_{\alpha}{:}A$}}}}\vbox{}}}\over\hbox{\hskip
42.02197pt\vbox{\vbox{}\hbox{\hskip-42.02197pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{0},\Delta^{\prime}_{0}\Vdash\mathcal{C},\mathcal{C}_{1}::\Delta,x_{\alpha}{:}A$}}}}}}$
$\mathbf{comp}$

$\displaystyle\displaystyle{\hbox{\hskip
119.37585pt\vbox{\hbox{\hskip-119.37584pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{0}\Vdash\mathcal{C}::\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta^{\prime}_{0},\Delta,x_{\alpha}{:}A\vdash\delta::\Omega^{\prime}_{0},\Omega,x{:}A$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Omega^{\prime}_{0},\Omega\vdash_{\Sigma}P::x{:}A$}}}}}\vbox{}}}\over\hbox{\hskip
60.37526pt\vbox{\vbox{}\hbox{\hskip-60.37524pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{0},\Delta^{\prime}_{0}\Vdash\mathcal{C},\mathbf{proc}(x_{\alpha},\hat{\delta}(P))::x_{\alpha}{:}A$}}}}}}$
$\mathbf{proc}$

$\displaystyle\displaystyle{\hbox{\hskip
62.11824pt\vbox{\hbox{\hskip-62.11823pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{0}\Vdash\mathcal{C}::\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta^{\prime}_{0},\Delta\vdash
M::x_{\alpha}{:}A$}}}}\vbox{}}}\over\hbox{\hskip
49.14322pt\vbox{\vbox{}\hbox{\hskip-49.14322pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{0},\Delta^{\prime}_{0}\Vdash\mathcal{C},\mathbf{msg}(M)::x_{\alpha}{:}A$}}}}}}$
$\mathbf{msg}$ $\displaystyle\displaystyle{\hbox{\hskip
11.04689pt\vbox{\hbox{\hskip-11.04689pt\hbox{\hbox{$\displaystyle\displaystyle
k\in L$}}}\vbox{}}}\over\hbox{\hskip
56.405pt\vbox{\vbox{}\hbox{\hskip-56.405pt\hbox{\hbox{$\displaystyle\displaystyle
y_{\alpha+1}{:}A_{k}\vdash
y_{\alpha}.k::y_{\alpha}{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in L}$}}}}}}$
$\mathbf{m}_{\oplus R}$

$\displaystyle\displaystyle{\hbox{\hskip
11.04689pt\vbox{\hbox{\hskip-11.04689pt\hbox{\hbox{$\displaystyle\displaystyle
k\in L$}}}\vbox{}}}\over\hbox{\hskip
65.01091pt\vbox{\vbox{}\hbox{\hskip-65.01091pt\hbox{\hbox{$\displaystyle\displaystyle
x_{\alpha}{:}\&\\{\ell:A_{\ell}\\}_{\ell\in I}\vdash
x_{\alpha}.k;P::x_{\alpha+1}{:}A_{k}$}}}}}}$ $\mathbf{m}_{\&L}$
$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
65.89449pt\vbox{\vbox{}\hbox{\hskip-65.89447pt\hbox{\hbox{$\displaystyle\displaystyle
z_{\beta}{:}A,y_{\alpha+1}{:}B\vdash\mathbf{send}\,z_{\beta}\,y_{\alpha}::y_{\alpha}{:}A\otimes
B$}}}}}}$ $\mathbf{m}_{\otimes R}$

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
68.50696pt\vbox{\vbox{}\hbox{\hskip-68.50694pt\hbox{\hbox{$\displaystyle\displaystyle
z_{\beta}{:}A,x_{\alpha}{:}A\multimap
B\vdash\mathbf{send}\,z_{\beta}\,x_{\alpha}::x_{\alpha+1}{:}B$}}}}}}$
$\mathbf{m}_{\multimap L}$ $\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip 0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
30.23456pt\vbox{\vbox{}\hbox{\hskip-30.23454pt\hbox{\hbox{$\displaystyle\displaystyle\cdot\vdash\mathbf{close}\,y_{\alpha}::y_{\alpha}{:}1$}}}}}}$
$\mathbf{m}_{1R}$

Figure 4. Configuration typing rules of SESSION. Spawn |  $\mathbf{proc}(y_{\alpha},(x\leftarrow X[\gamma]\leftarrow\Delta_{1});Q){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}$ $(\Delta^{\prime}_{1}\vdash X=P::x^{\prime}:B\in\Sigma)$
---|---
|
$\mathbf{proc}(x_{0},\hat{\gamma}(P))\;\mathbf{proc}(y_{\alpha},[x_{0}/x]Q)$
$(\Delta^{\prime}_{1},x^{\prime}\Vdash\gamma:\Delta_{1},x_{0},\,\,x_{0}\,\mathit{fresh})$
D-Fwd |  $\mathbf{proc}(y_{\alpha},F_{Y}[\gamma]){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}$ $(x^{\prime}:{C}\vdash F_{y}=\mathtt{Fwd}_{C,y^{\prime}\leftarrow x^{\prime}}::y^{\prime}:C\in\Sigma)$
|  $\mathbf{proc}(y_{\alpha},\mathtt{Fwd}_{C,y_{\alpha}\leftarrow x_{\beta}})$
$(x^{\prime},y^{\prime}\Vdash\gamma:x_{\beta},y_{\alpha})$
$1_{\mathsf{snd}}$ |  $\mathbf{proc}(y_{\alpha},(\mathbf{close}\,y_{\alpha})){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{msg}(\mathbf{close}\,y_{\alpha})$
$1_{\mathsf{rcv}}$ |  $\mathbf{msg}(\mathbf{close}\,y_{\alpha})\;\mathbf{proc}(x_{\beta},(\mathbf{wait}\,y_{\alpha};Q)){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(x_{\beta},Q)$
$\oplus_{\mathsf{snd}}$ |  $\mathbf{proc}(y_{\alpha},y_{\alpha}.k;P){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(y_{\alpha+1},([y_{\alpha+1}/y_{\alpha}]P))\;\mathbf{msg}(y_{\alpha}.k)$
$\oplus_{\mathsf{rcv}}$ |  $\mathbf{msg}(y_{\alpha}.k))\;\mathbf{proc}(u_{\gamma},\mathbf{case}\,y_{\alpha}((\ell\Rightarrow P_{\ell})_{\ell\in L})){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(u_{\gamma},([y_{\alpha+1}/y_{\alpha}]P_{k}))$
$\&_{\mathsf{snd}}$ |  $\mathbf{proc}(y_{\alpha},(x_{\beta}.k;P)){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{msg}(x_{\beta}.k)\;\mathbf{proc}(y_{\alpha},([x_{\beta+1}/x_{\beta}]P))$
$\&_{\mathsf{rcv}}$ |  $\mathbf{proc}(y_{\alpha},(\mathbf{case}\,y_{\alpha}(\ell\Rightarrow P_{\ell})_{\ell\in L}))\;\mathbf{msg}(y_{\alpha}.k){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(y_{\alpha+1},([y_{\alpha+1}/y_{\alpha}]P_{k}))$
$\otimes_{\mathsf{snd}}$ |  $\mathbf{proc}(y_{\alpha},(\mathbf{send}\,x_{\beta}\,y_{\alpha};P)){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(y_{\alpha+1},([y_{\alpha+1}/y_{\alpha}]P))\;\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})$
$\otimes_{\mathsf{rcv}}$ |  $\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})\;\mathbf{proc}(u_{\gamma},(w\leftarrow\mathbf{recv}\,y_{\alpha};P)){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(u_{\gamma},([x_{\beta}/w][y_{\alpha+1}/y_{\alpha}]P))$
$\multimap_{\mathsf{snd}}$ |  $\mathbf{proc}(y_{\alpha},(\mathbf{send}\,x_{\beta}\,u_{\gamma};P)){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,u_{\gamma})\;\mathbf{proc}(y_{\alpha},([u_{\gamma+1}/u_{\gamma}]P))$
$\multimap_{\mathsf{rcv}}$ |  $\mathbf{proc}(y_{\alpha},(w\leftarrow\mathbf{recv}\,y_{\alpha};P))\;\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha}){\color[rgb]{0,0.6,0}\;\;\mapsto\;\;}\mathbf{proc}(y_{\alpha+1},([x_{\beta}/w][y_{\alpha+1}/y_{\alpha}]P))$
Figure 5. Asynchronous dynamics of SESSION.

Message processes $\mathbf{msg}(M)$ are an artifact of SESSION’s asynchronous
semantics, which implements sends by spawning off a message process that
carries the sent message $M$. For example, in rule $\otimes_{\mathsf{snd}}$,
the provider
$\mathbf{proc}(y_{\alpha},(\mathbf{send}\,x_{\beta}\,y_{\alpha};P))$ generates
the message $\mathbf{send}\,x_{\beta}\,y_{\alpha}$, indicating that the
channel $x_{\beta}$ is sent over channel $y_{\alpha}$. Since sends are non-
blocking, the provider steps to its continuation
$\mathbf{proc}(y_{\alpha+1},([y_{\alpha+1}/y_{\alpha}]P))$, generating a new
_generation_ $\alpha+1$ of its providing channel $y_{\alpha}$. The receiving
client process of the message
$\mathbf{proc}(u_{\gamma},(w\leftarrow\mathbf{recv}\,y_{\alpha};P))$ will then
increment the channel generation of the carrier channel $y_{\alpha}$ upon
receipt in its continuation
$\mathbf{proc}(u_{\gamma},([x_{\beta}/w][y_{\alpha+1}/y_{\alpha}]P))$ as well
(see rule $\otimes_{\mathsf{rcv}}$). Generations are a convenient way of
allocating new names, while guaranteeing proper linkage between a message and
the sender’s continuation. Like bound variables, bound channels are subject to
$\alpha$-variance and capture-avoiding substitution, as usual (Sangiorgi and
Walker, 2001), with the understanding that only the base $y$ of a channel
$y_{\alpha}$ can be renamed, but its generation.

The configuration typing rules (see Fig. 4) use the judgment
$\Delta_{0}\Vdash\mathcal{C}::\Delta$ to type configurations. We allow
configurations to have _free channels_ , which amount to $\Delta_{0}$ and
$\Delta$ for the given judgment. The channels in $\Delta$ comprise the
channels for which there exist providing processes in the configuration
$\mathcal{C}$, the channels in $\Delta_{0}$ comprise the channels for which
there exist client processes in the configuration $\mathcal{C}$. It may be
surprising that we refer to these channels as free, given that they occur in
$C$. Would linearity not imply that they occur “exactly once”, and thus must
be bound? It is more fruitful to think of channels as shared resources, like
memory locations, that are _shared_ among processes. ILLST then ensures that
at most two processes, a provider and a client, share a channel at any point
in time, where each ”owns” one endpoint of (i.e., a reference to) the channel.
The careful accounting of “resources” is visible in the configuration typing
rules. For example, rule $\mathbf{proc}$ insists that for all the channel
endpoints used by process $\mathbf{proc}(x_{\alpha},\hat{\delta}(P))$ there
exists either a provider in the sub-configuration $\mathcal{C}$, making the
channel bound, or the endpoint is free and occurs in
$\Delta^{\prime}_{0},\Delta$.

##  3\. Recursive session logical relation (RSLR)

This section develops a logical relation for ILLST with general recursive
types (§ 3.1), shows that the logical relation is closed under parallel
composition (§ 3.2), amounts to an equivalence relation (§ 3.3), and is
sound and complete with regard to an asynchronous bisimilarity (§ 3.4). The
main result obtained via a biorthogonality argument, soundness and
completeness of the logical relation with regard to closure of weak
bisimilarity under parallel composition, is presented in § 3.5.

###  3.1. Logical relation

Logical relations have only recently been developed for session types (Pérez
et al., 2012; Caires et al., 2013; Pérez et al., 2014; DeYoung et al., 2020;
Derakhshan et al., 2021), with an emphasis on unary logical relations and
exclusively for ILLST _without_ recursion (neither term-level nor type-level).
We contribute a logical relation for ILLST with support of _general recursive
types_. In devising the resulting _recursive session logical relation (RSLR)_
, we had to tackle the following challenges:

  * •

_Well-foundedness:_ Recursive types mandate use of a measure like step-
indexing or later modalities (Appel and McAllester, 2001; Ahmed, 2006; Dreyer
et al., 2009) to keep the logical relation well-founded. Our logical relation
makes use of a more _extensional_ notion, an _observation index_ , which
bounds the number of messages exchanged with the outside world along the free
channels of a configuration. The observation index facilitates proofs of
various results shown in this section.

  * •

_Non-termination:_ In the presence of general recursive types, divergence is a
possible outcome. Our logical relation is _progress-sensitive_ with regard to
divergence in that it equates a divergent program only with another diverging
one.

  * •

_Nondeterminism:_ Although ILLST enjoy confluence, processes run
_concurrently_. As a result, the logical relation has to account for
relatedness of messages that are possibly not being sent simultaneously due to
nondeterminism of scheduling.

####  3.1.1. A logical relation for message-passing concurrency

It may be helpful to pause a moment and ask oneself what a logical relation
for session-typed processes should amount to. Logical relations for functional
languages relate terms by defining their equality at ground type when
evaluated to values. This can be phrased in terms of two mutually recursive
relations, a value interpretation $\mathcal{V}\llbracket\tau\rrbracket$ and a
term interpretation $\mathcal{E}\llbracket\tau\rrbracket$, defined by
structural induction on the type $\tau$. The former defines equality of values
at ground type, by inducting over the type, and the latter steps the terms
until they reach a value, demanding that these must be related by the value
interpretation. In imperative languages, logical relations are typically
enriched with Kripke possible worlds to semantically type the store (Pitts and
Stark, 1998; Ahmed et al., 2009; Dreyer et al., 2010; Neis et al., 2011; Hur
and Dreyer, 2011; Thamsborg and Birkedal, 2011).

To answer our question, it is helpful to remind ourselves that logical
relations are a means to prove observational equivalence (Morris, 1968), which
equates two programs, if the same observations can be made about them. In a
pure functional setting, the observables are the values to which the terms
evaluate. In an imperative setting, the observables can additionally comprise
the values of locations in the store. The observables in a message-passing
concurrent setting are the messages that a configuration of processes is
willing to exchange with the outside world.

A logical relation for session-typed processes thus relates pairs of process
configurations $(\mathcal{D}_{1};\mathcal{D}_{2})$, such that
$\Delta\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A$ and
$\Delta\Vdash\mathcal{D}_{2}::x_{\alpha}{:}A$, demanding that the same
messages can be observed along the free channels $\Delta$ and
$x_{\alpha}{:}A$. Fig. 6 shows the resulting logical relation for well-typed
process configurations in SESSION. We find it convenient to distinguish a
value interpretation $\mathcal{V}$ from a term interpretation $\mathcal{E}$.
As expected, the term interpretation steps the configurations until they reach
a “value”. But what does it mean for a configuration to be a value in a
message-passing concurrent setting? It means that a configuration is _ready
to_ _send_ or _receive_ along any of the free channels in
$\Delta\cup\\{x_{\alpha}{:}A\\}$. For any such channel, the term
interpretation invokes the value interpretation, which demands that the
exchanged messages be related, and then invokes the term interpretation for
the configurations resulting after the message exchange. The mutually
recursive relations are thus defined by _multiset induction over the structure
of types of the free channels_ (Derakhshan et al., 2021), yielding clauses of
the form

$(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket\qquad\mathsf{iff}\qquad\dots(\mathcal{D}_{1}^{\prime};\mathcal{D}_{2}^{\prime})\in\mathcal{E}\llbracket\Delta^{\prime}\Vdash
K^{\prime}\rrbracket\qquad(\Delta^{\prime}\Vdash K^{\prime}<\Delta\Vdash K).$

$\begin{array}[]{lcl}(1)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\cdot\Vdash
y_{\alpha})\,\mathsf{and}\\\ \qquad\in\mathcal{V}\llbracket\cdot\Vdash
y_{\alpha}{:}1\rrbracket_{\cdot;y_{\alpha}}^{m+1}&&\mathcal{D}_{1}=\mathbf{msg}(\mathbf{close}\,y_{\alpha})\,\mathsf{and}\,\mathcal{D}_{2}=\mathbf{msg}(\mathbf{close}\,y_{\alpha})\\\\[4.0pt]
(2)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta\Vdash
y_{\alpha}:\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in I})\,\mathsf{and}\,\,\exists
k_{1},k_{2}\in I.\\\ \qquad\in\mathcal{V}\llbracket(\Delta\Vdash
y_{\alpha}{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in
I})\rrbracket_{\cdot;y_{\alpha}}^{m+1}&&\mathcal{D}_{1}=\mathcal{D}^{\prime}_{1}\mathbf{msg}(y_{\alpha}.k_{1})\,\mathsf{and}\,\mathcal{D}_{2}=\mathcal{D}^{\prime}_{2}\mathbf{msg}(y_{\alpha}.k_{2})\,\mathsf{and}\,k_{1}=k_{2}\\\
&&\mathsf{and}\,({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
y_{\alpha+1}{:}A_{k_{1}}\rrbracket^{m}\\\\[4.0pt]
(3)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta\Vdash
y_{\alpha}{:}\&\\{\ell{:}A_{\ell}\\}_{\ell\in I})\,\mathsf{and}\,\,\forall
k_{1},k_{2}\in I.\\\ \qquad\in\mathcal{V}\llbracket\Delta\Vdash
y_{\alpha}{:}\&\\{\ell{:}A_{\ell}\\}_{\ell\in
I}\rrbracket_{y_{\alpha};\cdot}^{m+1}&&\mathbf{if}\,k_{1}=k_{2}\,\mathbf{then}({\mathcal{D}_{1}\mathbf{msg}(y_{\alpha}.k_{1})};{\mathcal{D}_{2}\mathbf{msg}(y_{\alpha}.k_{2})})\in\\\
&&\quad\mathcal{E}\llbracket\Delta\Vdash
y_{\alpha+1}{:}A_{k_{1}}\rrbracket^{m}\\\\[4.0pt]
(4)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta^{\prime},\Delta^{\prime\prime}\Vdash
y_{\alpha}{:}A\otimes B)\,\mathsf{and}\,\exists x_{\beta}\,\,\mathsf{s.t.}\\\
\qquad\in\mathcal{V}\llbracket\Delta^{\prime},\Delta^{\prime\prime}\Vdash
y_{\alpha}{:}A\otimes
B\rrbracket_{\cdot;y_{\alpha}}^{m+1}&&\,\mathcal{D}_{1}=\mathcal{D}^{\prime}_{1}\mathcal{T}_{1}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})\,\mathsf{for}\,\mathcal{T}_{1}\in\mathsf{Tree}(\Delta^{\prime\prime}\Vdash
x_{\beta}{:}A)\,\mathsf{and}\\\
&&\mathcal{D}_{2}=\mathcal{D}^{\prime}_{2}\mathcal{T}_{2}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})\,\mathsf{for}\,\mathcal{T}_{2}\in\mathsf{Tree}(\Delta^{\prime\prime}\Vdash
x_{\beta}{:}A)\,\mathsf{and}\\\
&&({\mathcal{T}_{1}};{\mathcal{T}_{2}})\in\mathcal{E}\llbracket\Delta^{\prime\prime}\Vdash
x_{\beta}{:}A\rrbracket^{m}\,\mathsf{and}\\\
&&({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{E}\llbracket\Delta^{\prime}\Vdash
y_{\alpha+1}{:}B\rrbracket^{m}\\\\[4.0pt]
(5)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta\Vdash
y_{\alpha}{:}A\multimap B)\,\mathsf{and}\,\forall
x_{\beta}{\not\in}\mathit{dom}(\Delta,y_{\alpha}{:}A\multimap B).\\\
\qquad\in\mathcal{V}\llbracket\Delta\Vdash y_{\alpha}{:}A\multimap
B\rrbracket_{y_{\alpha};\cdot}^{m+1}&&({\mathcal{D}_{1}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})};{\mathcal{D}_{2}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})})\in\\\
&&\quad\mathcal{E}\llbracket\Delta,x_{\beta}{:}A\Vdash
y_{\alpha+1}{:}B\rrbracket^{m}\\\\[4.0pt]
(6)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta,y_{\alpha}{:}1\Vdash
K)\,\mathsf{and}\\\ \qquad\in\mathcal{V}\llbracket\Delta,y_{\alpha}{:}1\Vdash
K\rrbracket_{y_{\alpha};\cdot}^{m+1}&&({\mathbf{msg}(\mathbf{close}\,y_{\alpha})\mathcal{D}_{1}};{\mathbf{msg}(\mathbf{close}\,y_{\alpha})\mathcal{D}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket^{m}\\\\[4.0pt]
(7)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta,y_{\alpha}{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in
I}\Vdash K)\,\mathsf{and}\,\forall k_{1},k_{2}\in I.\\\
\qquad\in\mathcal{V}\llbracket\Delta,y_{\alpha}:\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in
I}\Vdash
K\rrbracket_{y_{\alpha};\cdot}^{m+1}&&\mathbf{if}\,k_{1}=k_{2}\mathbf{then}\,({\mathbf{msg}(y_{\alpha}.k_{1})\mathcal{D}_{1}};{\mathbf{msg}(y_{\alpha}.k_{2})\mathcal{D}_{2}})\in\\\
&&\quad\mathcal{E}\llbracket\Delta,y_{\alpha+1}{:}A_{k_{1}}\Vdash
K\rrbracket^{m}\\\\[4.0pt]
(8)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta,y_{\alpha}{:}\&\\{\ell{:}A_{\ell}\\}_{\ell\in
I}\Vdash K)\,\mathsf{and}\,\exists k_{1},k_{2}\in I.\\\
\qquad\in\mathcal{V}\llbracket\Delta,y_{\alpha}{:}\&\\{\ell{:}A_{\ell}\\}_{\ell\in
I}\Vdash
K\rrbracket_{\cdot;y_{\alpha}}^{m+1}&&\mathcal{D}_{1}=\mathbf{msg}(y_{\alpha}.k_{1})\mathcal{D}^{\prime}_{1}\,\mathsf{and}\
\mathcal{D}_{2}=\mathbf{msg}(y_{\alpha}.k_{2})\mathcal{D}^{\prime}_{2}\,\mathsf{and}\,k_{1}=k_{2}\\\
&&\mathsf{and}\,({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{E}\llbracket\Delta,y_{\alpha+1}{:}A_{k_{1}}\Vdash
K\rrbracket^{m}\\\\[4.0pt]
(9)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta,y_{\alpha}{:}A\otimes
B\Vdash K)\,\mathsf{and}\,\forall
x_{\beta}{\not\in}\mathit{dom}(\Delta,y_{\alpha}{:}A\otimes B,K).\\\
\qquad\in\mathcal{V}\llbracket\Delta,y_{\alpha}{:}A\otimes B\Vdash
K\rrbracket_{y_{\alpha};\cdot}^{m+1}&&({\mathbf{msg}(\mathbf{send}x_{\beta}\,y_{\alpha})\mathcal{D}_{1}};{\mathbf{msg}(\mathbf{send}x_{\beta}\,y_{\alpha})\mathcal{D}_{2}})\in\\\
&&\quad\mathcal{E}\llbracket\Delta,x_{\beta}{:}A,y_{\alpha+1}{:}B\Vdash
K\rrbracket^{m}\\\\[4.0pt]
(10)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta^{\prime},\Delta^{\prime\prime},y_{\alpha}{:}A\multimap
B\Vdash K)\,\mathsf{and}\,\exists x_{\beta}\,\mathsf{s.t.}\\\
\qquad\in\mathcal{V}\llbracket\Delta^{\prime},\Delta^{\prime\prime},y_{\alpha}{:}A\multimap
B\Vdash
K\rrbracket_{\cdot;y_{\alpha}}^{m+1}&&\mathcal{D}_{1}=\mathcal{T}_{1}\mathbf{msg}(\mathbf{send}x_{\beta}\,y_{\alpha})\,\mathcal{D}^{\prime\prime}_{1}\,\mathsf{for}\,\mathcal{T}_{1}\in\mathsf{Tree}(\Delta^{\prime}\Vdash
x_{\beta}{:}A)\\\
&&\mathcal{D}_{2}=\mathcal{T}_{2}\mathbf{msg}(\mathbf{send}x_{\beta}\,y_{\alpha})\,\mathcal{D}^{\prime\prime}_{2}\,\mathsf{for}\,\mathcal{T}_{2}\in\mathsf{Tree}(\Delta^{\prime}\Vdash
x_{\beta}{:}A)\,\mathsf{and}\\\
&&({\mathcal{T}_{1}};{\mathcal{T}_{2}})\in\mathcal{E}\llbracket\Delta^{\prime}\Vdash
x_{\beta}{:}A\rrbracket^{m}\,\mathsf{and}\\\
&&({\mathcal{D}^{\prime\prime}_{1}};{\mathcal{D}^{\prime\prime}_{2}})\in\mathcal{E}\llbracket\Delta^{\prime\prime},y_{\alpha+1}{:}B\Vdash
K\rrbracket^{m}\\\\[4.0pt]
(11)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket^{m+1}&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta\Vdash
K)\,\mathsf{and}\,\forall\,\Upsilon_{1},\Theta_{1},\mathcal{D}^{\prime}_{1}.\,\mathsf{if}\;{\mathcal{D}_{1}}\;\mapsto^{{*}_{\Upsilon_{1};\Theta_{1}}}\;{\mathcal{D}^{\prime}_{1}}\\\
&&\mathsf{then}\,\exists\Upsilon_{2},\mathcal{D}^{\prime}_{2}\mathsf{\,such\,that\,}\,{\mathcal{D}_{2}}\mapsto^{{*}_{\Upsilon_{2}}}{\mathcal{D}^{\prime}_{2}},\;\mathsf{and}\,\Upsilon_{1}\subseteq\Upsilon_{2}\;\mathsf{and}\\\\[2.0pt]
&&\forall\,y_{\alpha}\in\mathbf{Out}(\Delta\Vdash
K).\,\mathbf{if}\,y_{\alpha}\in\Upsilon_{1}.\,\mathbf{then}\,({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{\cdot;y_{\alpha}}^{m+1}\,\mathsf{and}\\\\[2.0pt]
&&\forall\,y_{\alpha}\in\mathbf{In}(\Delta\Vdash
K).\mathbf{if}\,y_{\alpha}\in\Theta_{1}.\,\mathbf{then}\,({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{y_{\alpha};\cdot}^{m+1}\\\\[4.0pt]
(12)\;({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket^{0}&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta\Vdash
K)\par\par\par\end{array}$ Figure 6. Recursive session logical relation (RSLR)
for ILLST.

We refer to the index $\llbracket\Delta\Vdash K\rrbracket$ of the logical
relation as its _interface_. It singles out the typing of the providing free
channel on the right of the turnstile, where the metavariable $K$ stands for
either $x_{\alpha}{:}A$ or simply $\\_$. Def. 1 will clarify why the logical
relation admits $\\_$ on the right in its interface. The transition from the
value interpretation to the term interpretation amounts to an _observation_ of
a message exchange along a channel in the interface $\llbracket\Delta\Vdash
K\rrbracket$. The exchange will advance the protocol state of the concerned
process, and as a result transition the interface to
$\llbracket\Delta^{\prime}\Vdash K^{\prime}\rrbracket$, describing the post-
states of the configurations
$(\mathcal{D}_{1}^{\prime};\mathcal{D}_{2}^{\prime})$ after the message
exchange. The logical relation comprises two value interpretation clauses for
each ILLST connective, one for when the communication occurs on the _right_
along $K$, and one for when it occurs on the _left_ along $\Delta$.

Defining the logical relation by multiset induction over the structure of
types in its interface $\llbracket\Delta\Vdash K\rrbracket$ is only sound for
terminating ILLST languages. In § 3.1.3 we introduce an observation index to
stratify the logical relation. Next, we remark on a pattern underlying our
logical relation, crucial to establish extensionality.

####  3.1.2. Assume and assert—a pas de deux

A key characteristic of logical relations is _extensionality_. In a functional
context this means that relatedness has to be shown for values of types in
positive positions, but values of types in negative positions can be assumed
to be related. This idea translates equally to a message-passing concurrent
setting, embodied by the logical relation shown in Fig. 6 as follows:

  * •

_Positive_ connectives _assert_ the sending of related messages when
communicating on the _right_ and _assume_ receipt of related messages when
communicating on the _left_.

  * •

_Negative_ connectives _assume_ receipt of related messages when communicating
on the _right_ and _assert_ the sending of related messages when communicating
on the _left_.

At ground types ($1$, $\oplus$, and $\&$), relatedness of messages means that
the same messages are being exchanged. For example, clause (2) in Fig. 6 for
$\oplus$-right asserts existence of messages $\mathbf{msg}(y_{\alpha}.k_{1})$
and $\mathbf{msg}(y_{\alpha}.k_{2})$ in $\mathcal{D}_{1}$ and
$\mathcal{D}_{2}$, resp., such that $k_{1}=k_{2}$. The predicate
$(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathsf{Tree}(\Delta\Vdash K)$ is defined
as $\mathcal{D}_{1}\in\mathsf{Tree}(\Delta\Vdash K)$ and
$\mathcal{D}_{2}\in\mathsf{Tree}(\Delta\Vdash K)$, with
$\mathcal{D}_{i}\in\mathsf{Tree}(\Delta\Vdash K)$ being defined as
$\Delta\Vdash\mathcal{D}::K$ (see Def. LABEL:APX:apx:def:well-typed-config on
page LABEL:APX:apx:def:well-typed-config in the Appendix). Conversely, clause
(3) in Fig. 6 for $\&$-right assumes receipt of messages
$\mathbf{msg}(y_{\alpha}.k_{1})$ and $\mathbf{msg}(y_{\alpha}.k_{2})$ to be
added to $\mathcal{D}_{1}$ and $\mathcal{D}_{2}$ in the post-states, resp.,
such that $k_{1}=k_{2}$, for arbitrary $k_{1}$ and $k_{2}$.

For higher-order types ($\otimes$ and $\multimap$) relatedness means that
future observations to be made along the exchanged channels must be related.
For example, clause (10) in Fig. 6 for $\multimap$-left asserts existence of a
message $\mathbf{msg}(\mathbf{send}x_{\beta}\,y_{\alpha})$ and of subtrees
$\mathcal{T}_{1}$ and $\mathcal{T}_{1}$ in $\mathcal{D}_{1}$ and
$\mathcal{D}_{2}$, resp. The clause comprises two invocations of the term
relation,
$({\mathcal{T}_{1}};{\mathcal{T}_{2}})\in\mathcal{E}\llbracket\Delta^{\prime}\Vdash
x_{\beta}{:}A\rrbracket$, asserting that future observations to be made along
the sent channel $x_{\beta}$ are related, and
$({\mathcal{D}^{\prime\prime}_{1}};{\mathcal{D}^{\prime\prime}_{2}})\in\mathcal{E}\llbracket\Delta^{\prime\prime},y_{\alpha+1}{:}B\Vdash
K\rrbracket$, asserting that the continuations
$\mathcal{D}^{\prime\prime}_{1}$ and ${\mathcal{D}^{\prime\prime}_{2}}$ are
related.111We defer a discussion of the superscript and subscripts of
$\llbracket\Delta\Vdash K\rrbracket_{\\_;\\_}^{m}$ present in Fig. 6 to §
3.1.3 and § 3.1.4, resp. The channel endpoint $x_{\beta}$ is existentially
quantified and occurs either bound or free in both $\mathcal{D}_{1}$ and
$\mathcal{D}_{2}$. Conversely, clause (5) in Fig. 6 for $\multimap$-left
assumes receipt of a message
$\mathbf{msg}(\mathbf{send}x_{\beta}\,y_{\alpha})$ that carries a universally
quantified free channel $x_{\beta}$, different from the free channels
available in the pre-state ($\forall
x_{\beta}\not\in\mathit{dom}(\Delta,y_{\alpha}{:}A\multimap B)$). The
interface of free channels is then enlarged with the received channel
$x_{\beta}$ for the invocation of the term relation
$({\mathcal{D}_{1}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})};{\mathcal{D}_{2}\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})})\in\mathcal{E}\llbracket\Delta,x_{\beta}{:}A\Vdash
y_{\alpha+1}{:}B\rrbracket$.

The assumptions and assertions made by the logical relation are kept in
balance by the inherent _duality_ of session types, ensuring that the
assumptions made by two configurations to be shown related will be discharged
when composed with configurations asserted to be related. This pas de deux
between assume and assert allows us to connect our development to
biorthogonality in § 3.5.

####  3.1.3. Well-foundedness

In the presence of general recursive types, as this is the case for SESSION,
it is no longer sound to define the logical relation by multiset induction
over the structure of types in its interface $\llbracket\Delta\Vdash
K\rrbracket$. To restore well-foundedness a measure like step-indexing (Appel
and McAllester, 2001; Ahmed, 2006) can be employed. Step-indexing is typically
tied to the number of type unfolding or computation steps by which one of the
two programs is bound. A more natural and symmetric measure for our setting is
the number of _observations_ that can be made along the free channels in the
interface $\llbracket\Delta\Vdash K\rrbracket$ of the logical relation. We
thus bound the value and term interpretation of our logical relation by this
number and attach the resulting _observation index_ as the superscript $m$ to
the relation’s interface $\llbracket\Delta\Vdash K\rrbracket$, yielding
clauses of the form

$(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket^{m+1}\qquad\mathsf{iff}\qquad\dots(\mathcal{D}_{1}^{\prime};\mathcal{D}_{2}^{\prime})\in\mathcal{E}\llbracket\Delta^{\prime}\Vdash
K^{\prime}\rrbracket^{m}\qquad(m\geq 0).$

The observation index gets decremented whenever the value interpretation
“observes” a message exchange. If $m=0$, ILLST-typed configurations are
trivially related, as expressed by clause (12) in Fig. 6.

####  3.1.4. Non-termination and nondeterminism

It is now time to take a closer look at the definition of the term
interpretation of our logical relation. Its definition is challenged by the
possibility of divergence and nondeterminism of scheduling. For the former, a
progress-sensitive statement of equivalence demands that the relation relates
a divergent program only with another diverging one. For the latter, the term
interpretation has to account for the possibility that two configurations may
not _simultaneously_ be ready to send or receive along a channel in the
interface of the logical relation. To address these challenges, the term
interpretation is phrased as follows (we are repeating clause (11) in Fig. 6):

$\begin{array}[]{@{}lcl@{}}({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket^{m+1}&\mathsf{iff}&({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathsf{Tree}(\Delta\Vdash
K)\,\mathsf{and}\,\forall\,\Upsilon_{1},\Theta_{1},\mathcal{D}^{\prime}_{1}.\\\\[2.0pt]
&&\mathsf{if}\;{\mathcal{D}_{1}}\;\mapsto^{{*}_{\Upsilon_{1};\Theta_{1}}}\;{\mathcal{D}^{\prime}_{1}}\,\mathsf{then}\,\exists\Upsilon_{2},\mathcal{D}^{\prime}_{2}\mathsf{\,such\,that\,}\,{\mathcal{D}_{2}}\mapsto^{{*}_{\Upsilon_{2}}}{\mathcal{D}^{\prime}_{2}}\,\mathsf{and}\,\Upsilon_{1}\subseteq\Upsilon_{2}\;\mathsf{and}\\\\[2.0pt]
&&\forall\,y_{\alpha}\in\mathbf{Out}(\Delta\Vdash
K).\,\mathbf{if}\,y_{\alpha}\in\Upsilon_{1}.\,\mathbf{then}\,({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{\cdot;y_{\alpha}}^{m+1}\,\mathsf{and}\\\\[2.0pt]
&&\forall\,y_{\alpha}\in\mathbf{In}(\Delta\Vdash
K).\mathbf{if}\,y_{\alpha}\in\Theta_{1}.\,\mathbf{then}\,({\mathcal{D}^{\prime}_{1}};{\mathcal{D}^{\prime}_{2}})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{y_{\alpha};\cdot}^{m+1}\end{array}$

The term interpretation makes use of the transition
${\mathcal{D}_{1}}\mapsto^{{*}_{\Upsilon_{1};\Theta_{1}}}{\mathcal{D}^{\prime}_{1}}$,
which amounts to iterated application of the rewriting rules defined in Fig.
5. The star expresses that zero to multiple steps can be taken. The
superscript $\Upsilon_{1}$ denotes the set of channels occurring in the
interface $\llbracket\Delta\Vdash K\rrbracket$ for which there exist messages
in $\mathcal{D}^{\prime}_{1}$ to be sent along these channels. The superscript
$\Theta_{1}$ denotes set of channels occurring in the interface
$\llbracket\Delta\Vdash K\rrbracket$ for which there exist processes in
$\mathcal{D}^{\prime}_{1}$ waiting to receive along these channels.

To ensure progress-sensitivity, the term interpretation asserts, that,
whenever $\mathcal{D}_{1}$ can step, so can $\mathcal{D}_{2}$, and that the
messages ready to be sent to the outside world in $\mathcal{D}^{\prime}_{2}$
are at least the ones found in $\mathcal{D}^{\prime}_{1}$. Due to the dynamics
being asynchronous, the set of processes blocked along a free channel in
$\mathcal{D}^{\prime}_{1}$ and $\mathcal{D}^{\prime}_{2}$ are not required to
correspond, since a receipt is not an observable event. The existentially
quantified $\mathcal{D}^{\prime}_{2}$ is justified by nondeterminism of
scheduling, allowing the term interpretation to choose an appropriate way of
stepping $\mathcal{D}_{2}$ to catch up with $\mathcal{D}^{\prime}_{1}$.

To resolve the issue of simultaneity, the term interpretation makes use of two
_focus_ channels ranging over the sets $\Upsilon_{1}$ and $\Theta_{1}$. These
are added as a subscript $\\_;\\_$ to the value interpretation, where
$\cdot;y_{\alpha}$ indicates that $y_{\alpha}\in\Upsilon_{1}$ and
$y_{\alpha};\cdot$ that $y_{\alpha}\in\Theta_{1}$. The term interpretation
invokes the value interpretation for all the channels in $\Upsilon_{1}$ and
$\Theta_{1}$, thus ensuring that any messages ready to be sent in
$\mathcal{D}^{\prime}_{1}$ and $\mathcal{D}^{\prime}_{2}$ and any processes
waiting to receive in $\mathcal{D}^{\prime}_{1}$ will be “observed” by the
value interpretation. Non-productive configurations are trivially accommodated
by the term interpretation, by allowing the sets $\Upsilon_{1}$ and
$\Theta_{1}$ to be empty.

A reader may wonder why the logical relation seems oblivious of recursive type
unfoldings. Since the relation is indexed by the number of external
observations, it is invariant in type unfoldings. For example, for the pair of
configurations $({\mathcal{D}_{1}};{\mathcal{D}_{2}})$ it holds true that
$({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
x_{\alpha}{:}\mathsf{pin}\rrbracket^{m+1}$ as well as
$({\mathcal{D}_{1}};{\mathcal{D}_{2}})\in\mathcal{E}\llbracket\Delta\Vdash
x_{\alpha}{:}\oplus\\{\mathit{tok_{i}}{:}\mathsf{pin}\\}_{i\leq
n}\rrbracket^{m+1}$, because the value interpretation with focus channel
$x_{\alpha}$ is only triggered when a message along $x_{\alpha}$ is ready
(i.e., token). Any subsequent invocation of the term interpretation by the
value interpretation upon consumption of the message will then happen at index
$m$.

###  3.2. Linking: closure under parallel composition

The use of an observation index rather than a step index by the RSLR is
fundamental in proving various metatheoretic properties in the remainder of
this section. It allows us to keep the observation index _constant_ in the
term interpretation, while stepping the configurations internally, permitting
disagreement in the number of internal messages exchanged. As a result,
internal steps cannot depend on the observation index, facilitating proof of
the following lemma:

###### Lemma 0 (Moving existential over universal quantifier).

if we have

$\begin{array}[]{l}\forall
m.\,\forall\,\Upsilon_{1},\Theta_{1},\mathcal{D}^{\prime}_{1}.\,\,\mathsf{if}\,\mathcal{D}_{1}\mapsto^{*_{\Upsilon_{1};\Theta_{1}}}\mathcal{D}^{\prime}_{1},\,\mathsf{then}\,\exists\Upsilon_{2},\mathcal{D}^{\prime}_{2}\,\mathsf{such\,that}\,\,\mathcal{D}_{2}\mapsto^{{*}_{\Upsilon_{2}}}\mathcal{D}^{\prime}_{2}\,\mathsf{and}\,\Upsilon_{1}\subseteq\Upsilon_{2}\,\mathsf{and}\\\
\;\;\forall\,x_{\alpha}\in\mathbf{Out}(\Delta\Vdash
K).\,\mathbf{if}\,x_{\alpha}\in\Upsilon_{1}.\,\mathbf{then}\,\,(\mathcal{D}^{\prime}_{1};\mathcal{D}^{\prime}_{2})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{\cdot;x_{\alpha}}^{m+1}\,\mathsf{and}\\\
\;\;\forall\,x_{\alpha}\in\mathbf{In}(\Delta\Vdash
K).\mathbf{if}\,x_{\alpha}\in\Theta_{1}.\,\mathbf{then}\,(\mathcal{D}^{\prime}_{1};\mathcal{D}^{\prime}_{2})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{x_{\alpha};\cdot}^{m+1}.\end{array}$

then

$\begin{array}[]{l}\forall\,\Upsilon_{1},\Theta_{1},\mathcal{D}^{\prime}_{1}.\mathsf{if}\,\mathcal{D}_{1}\mapsto^{*_{\Upsilon_{1};\Theta_{1}}}\mathcal{D}^{\prime}_{1},\,\mathsf{then}\,\exists\Upsilon_{2},\mathcal{D}^{\prime}_{2}\,\mathsf{such\,that}\,\,\mathcal{D}_{2}\mapsto^{{*}_{\Upsilon_{2}}}\mathcal{D}^{\prime}_{2}\,\mathsf{and}\,\Upsilon_{1}\subseteq\Upsilon_{2}\,\mathsf{and}\\\
\;\;\forall\,x_{\alpha}\in\mathbf{Out}(\Delta\Vdash
K).\,\mathbf{if}\,x_{\alpha}\in\Upsilon_{1}.\,\mathbf{then}\,\,\forall\,k.\,(\mathcal{D}^{\prime}_{1};\mathcal{D}^{\prime}_{2})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{\cdot;x_{\alpha}}^{k+1}\,\mathsf{and}\\\
\;\;\forall\,x_{\alpha}\in\mathbf{In}(\Delta\Vdash
K).\mathbf{if}\,x_{\alpha}\in\Theta_{1}.\,\mathbf{then}\,\,\forall
k.\,(\mathcal{D}^{\prime}_{1};\mathcal{D}^{\prime}_{2})\in\mathcal{V}\llbracket\Delta\Vdash
K\rrbracket_{x_{\alpha};\cdot}^{k+1}.\end{array}$

###### Proof.

See proof of Lem. LABEL:APX:apx:lem:moving-existential on page
LABEL:APX:apx:lem:moving-existential in the Appendix. The proof relies on
confluence (Lem. LABEL:APX:apx:lem:confluence on page
LABEL:APX:apx:lem:confluence in the Appendix) and backwards closure (Lem.
LABEL:APX:apx:lem:backsecondrun on page LABEL:APX:apx:lem:backsecondrun in the
Appendix). ∎

With this lemma in hand, we can now prove that the logical relation is closed
under parallel composition.

###### Lemma 0 (Linking).

$\forall
m.\,(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathcal{E}\llbracket\Delta,u_{\alpha}{:}T\Vdash
K\rrbracket^{m}$ iff forall $\mathcal{T}_{2}$ and $\mathcal{T}_{2}$ s.t.
$\forall
m.\,(\mathcal{T}_{1};\mathcal{T}_{2})\in\mathcal{E}\llbracket\Delta^{\prime}\Vdash
u_{\alpha}{:}T\rrbracket^{m}$ we have $\forall
k.\,(\mathcal{T}_{1}\mathcal{D}_{1};\mathcal{T}_{2}\mathcal{D}_{2})\in\mathcal{E}\llbracket\Delta^{\prime},\Delta\Vdash
K\rrbracket^{k}$.

###### Proof.

See proof of Cor. LABEL:APX:apx:lem:compositionality on page
LABEL:APX:apx:lem:compositionality in the Appendix. The proof relies on Lem.
1. ∎

###  3.3. Logical equivalence

To prove that the RSLR induces an equivalence relation, we introduce the
notation $\Delta\Vdash\mathcal{D}_{1}::K\equiv\Delta\Vdash\mathcal{D}_{2}::K$,
defined below, where
$(\mathcal{C}_{1};\mathcal{C}_{2})\in\mathsf{Forest}(\Delta^{\prime}\Vdash\Delta)$
stands for $\Delta^{\prime}\Vdash\mathcal{C}_{1}::\Delta$ and
$\Delta^{\prime}\Vdash\mathcal{C}_{2}::\Delta$:

###### Definition 0.

  * •

Define the relation
$\Delta\Vdash\mathcal{D}_{1}::K\equiv\Delta\Vdash\mathcal{D}_{2}::K$ as
$(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathsf{Tree}(\Delta\Vdash K)$ and
$\forall
m.\,(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket$ and $\forall
m.(\mathcal{D}_{2};\mathcal{D}_{1})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket$.

  * •

Define the relation $\Delta\dashv\mathcal{C}_{1}[\,\,]\mathcal{F}_{1}\dashv
K\equiv\Delta\dashv\mathcal{C}_{2}[\,\,]\mathcal{F}_{2}\dashv K$ as (i)
$\exists K^{\prime}$ such that $K\Vdash\mathcal{F}_{1}::K^{\prime}\equiv
K\Vdash\mathcal{F}_{2}::K^{\prime}$ and (ii) $\exists\Delta^{\prime}$ such
that
$(\mathcal{C}_{1};\mathcal{C}_{2})\in\mathsf{Forest}(\Delta^{\prime}\Vdash\Delta)$
and
$\forall\mathcal{T}_{1}\in\mathcal{C}_{1},\,\mathsf{and}\,\forall\mathcal{T}_{2}\in\mathcal{C}_{2}$
with
$(\mathcal{T}_{1};\mathcal{T}_{2})\in\mathsf{Tree}(\Delta^{\prime}_{1}\Vdash
K^{\prime\prime})$, we have
$\Delta^{\prime}_{1}\Vdash\mathcal{T}_{1}::K^{\prime\prime}\equiv\Delta^{\prime}_{1}\Vdash\mathcal{T}_{2}::K^{\prime\prime}$.

Next, we show that the relation $\equiv$ is reflexive, symmetric, and
transitive.

###### Lemma 0 (Reflexivity).

For all configurations $\Delta\Vdash\mathcal{D}::x_{\alpha}{:}T$, we have

$(\Delta\Vdash\mathcal{D}::x_{\alpha}{:}T)\equiv(\Delta\Vdash\mathcal{D}::x_{\alpha}{:}T).$

###### Proof.

See proof of Lem. LABEL:APX:apx:lem:reflexivity-eq on page
LABEL:APX:apx:lem:reflexivity-eq in the Appendix. ∎

###### Lemma 0 (Symmetry).

For all configurations $\mathcal{D}_{1}$ and $\mathcal{D}_{2}$, we have
$(\Delta\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T)\equiv(\Delta\Vdash\mathcal{D}_{2}::x_{\alpha}{:}T),$
iff
$(\Delta\Vdash\mathcal{D}_{2}::x_{\alpha}{:}T)\equiv(\Delta\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T),$

###### Proof.

The proof is straightforward by the definition of triple equality (Def. 3). ∎

###### Lemma 0 (Transitivity).

For all configurations $\mathcal{D}_{1}$, $\mathcal{D}_{2}$, and
$\mathcal{D}_{3}$, we have

$\begin{array}[]{l}\mathsf{if}\,(\Delta\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T)\equiv(\Delta\Vdash\mathcal{D}_{2}::x_{\alpha}{:}T),\,\mathsf{and}\,(\Delta\Vdash\mathcal{D}_{2}::x_{\alpha}{:}T)\equiv(\Delta\Vdash\mathcal{D}_{3}::x_{\alpha}{:}T)\\\
\mathsf{then}\,(\Delta\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T)\equiv(\Delta\Vdash\mathcal{D}_{3}::x_{\alpha}{:}T).\end{array}$

###### Proof.

See proof of Lem. LABEL:APX:apx:lem:transitivity-eq on page
LABEL:APX:apx:lem:transitivity-eq in the Appendix. ∎

###  3.4. Adequacy

To show that the RSLR is adequate, we prove that configurations related by the
logical relation are bisimilar and vice versa. To facilitate this proof, we
first give the definition of _asynchronous bisimilarity_ (Sangiorgi and
Walker, 2001) (Def. 7). The definition relies on the labeled transition system
resulting from our RSLR displayed in Fig. 7 and on weak transitions defined as

  1. (1)

$\xRightarrow{}$ is the reflexive and transitive closure of
$\xrightarrow{\tau}$,

  2. (2)

$\xRightarrow{\alpha}$ is $\xRightarrow{}\xrightarrow{\alpha}$.

###### Definition 0 (Asynchronous bisimilarity).

Asynchronous bisimilarity is the largest symmetric relation such that whenever
$\mathcal{D}_{1}\approx_{\mathsf{a}}\mathcal{D}_{2}$, we have

  1. (1)

$(\tau-\mathtt{step})$ if
$\mathcal{D}_{1}\xrightarrow{\tau}\mathcal{D}^{\prime}_{1}$ then
$\exists\mathcal{D}^{\prime}_{2}.\,\mathcal{D}_{2}\xRightarrow{\tau}\mathcal{D}^{\prime}_{2}$
and $\mathcal{D}^{\prime}_{1}\approx_{\mathsf{a}}\mathcal{D}^{\prime}_{2},$

  2. (2)

$(\mathsf{output})$ if
$\mathcal{D}_{1}\xrightarrow{\overline{x_{\alpha}}\,q}\mathcal{D}^{\prime}_{1}$
then
$\exists\mathcal{D}^{\prime}_{2}.\,\mathcal{D}_{2}\xRightarrow{\overline{x_{\alpha}}\,q}\mathcal{D}^{\prime}_{2}$
and $\mathcal{D}^{\prime}_{1}\approx_{\mathsf{a}}\mathcal{D}^{\prime}_{2}.$

  3. (3)

$(\mathsf{left\,input})$ for all $q\not\in\mathsf{fn}(\mathcal{D}_{1})$, if
$\mathcal{D}_{1}\xrightarrow{{\mathbf{L}\,x_{\alpha}\,q}}\mathcal{D}^{\prime}_{1}$
then
$\exists\mathcal{D}^{\prime}_{2}.\,\mathcal{D}_{2}\xRightarrow{\tau}\mathcal{D}^{\prime}_{2}$
and
$\mathcal{D}^{\prime}_{1}\approx_{\mathsf{a}}\mathbf{msg}(x_{\alpha}.q)\mathcal{D}^{\prime}_{2},$

  4. (4)

$(\mathsf{right\,input})$ for all $q\not\in\mathsf{fn}(\mathcal{D}_{1})$, if
$\mathcal{D}_{1}\xrightarrow{{\mathbf{R}\,x_{\alpha}\,q}}\mathcal{D}^{\prime}_{1}$
then
$\exists\mathcal{D}^{\prime}_{2}.\,\mathcal{D}_{2}\xRightarrow{\tau}\mathcal{D}^{\prime}_{2}$
and
$\mathcal{D}^{\prime}_{1}\approx_{\mathsf{a}}\mathcal{D}^{\prime}_{2}\mathbf{msg}(x_{\alpha}.q).$

where $\mathbf{msg}(x_{\alpha}.q)$ is defined as
$\mathbf{msg}(\mathbf{close}\,x_{\alpha})$ if $q=\mathbf{close}$,
$\mathbf{msg}(x_{\alpha}.k)$ if $q=k$, and
$\mathbf{msg}(\mathbf{send}\,z_{\delta}\,x_{\alpha})$ if $q=z_{\delta}$.

Internal transition $\xrightarrow{\tau}$ defined as:
$\displaystyle\mathcal{D}_{1}\xrightarrow{\tau}\mathcal{D}_{1}^{\prime}\,\mathsf{iff}\,\mathcal{D}_{1}\mapsto\mathcal{D}^{\prime}_{1}$
Actions $\xrightarrow{\overline{y_{\alpha}}\,q}$,
$\xrightarrow{{\mathbf{L}\,y_{\alpha}\,q}}$ and
$\xrightarrow{{\mathbf{R}\,y_{\alpha}\,q}}$ defined as below when
$y\in\mathbf{fn}(\mathcal{D}_{1})$:

$\begin{array}[]{llll}(1)\,\mathcal{D}_{1}{\mathbf{msg}(\mathbf{close}\,y_{\alpha})}\,{\mathcal{D}_{2}}&\xrightarrow{\overline{y_{\alpha}}\,\mathbf{close}}&\mathcal{D}_{1}\mathcal{D}_{2}\\\\[10.0pt]
(2)\mathcal{D}_{1}\,\mathbf{msg}(y_{\alpha}.k)\mathcal{D}_{2}&\xrightarrow{\overline{y_{\alpha}}\,k}&\mathcal{D}_{1}\mathcal{D}_{2}\\\\[10.0pt]
(3)\mathcal{D}_{1}\,\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})\mathcal{D}_{2}&\xrightarrow{\overline{y_{\alpha}}\,x_{\beta}}&\mathcal{D}_{1}\mathcal{D}_{2}\\\\[10.0pt]
(4)\,\mathcal{D}_{1}\mathbf{proc}(z_{\delta},\mathbf{wait}\,y_{\alpha};P){\mathcal{D}_{2}}&\xrightarrow{{\mathbf{L}\,y_{\alpha}\,\mathbf{close}}}&{\mathbf{msg}(\mathbf{close}\,y_{\alpha})\,\mathcal{D}_{1}\mathbf{proc}(z_{\delta},\mathbf{wait}\,y_{\alpha};P)\,\mathcal{D}_{2}}\\\\[10.0pt]
(5)\,\mathcal{D}_{1}\mathbf{proc}(z_{\delta},\mathbf{case}\,y_{\alpha}\,(\ell\Rightarrow
P_{\ell})_{\ell\in
I})\,\mathcal{D}_{2}&\xrightarrow{{\mathbf{L}\,y_{\alpha}\,k}}&{\mathbf{msg}(y_{\alpha}.k)\mathcal{D}_{1}\mathbf{proc}(z_{\delta},\mathbf{case}\,y_{\alpha}\,(\ell\Rightarrow
P_{\ell})_{\ell\in I})\mathcal{D}_{2}}\\\\[10.0pt]
(6)\mathcal{D}_{1}\,\mathbf{proc}(z_{\delta},w\leftarrow\mathbf{recv}\,y_{\alpha})\mathcal{D}_{2}&\xrightarrow{{\mathbf{L}\,y_{\alpha}\,x_{\beta}}}&\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})\mathcal{D}_{1}\,\mathbf{proc}(z_{\delta},w\leftarrow\mathbf{recv}\,y_{\alpha})\,\mathcal{D}_{2}\\\\[10.0pt]
(7)\mathcal{D}_{1}\,\mathbf{proc}(y_{\alpha},\mathbf{case}\,y_{\alpha}\,(\ell\Rightarrow
P_{\ell})_{\ell\in
I})\mathcal{D}_{2}&\xrightarrow{{\mathbf{R}\,y_{\alpha}\,k}}&\mathcal{D}_{1}\,\mathbf{proc}(y_{\alpha},\mathbf{case}\,y_{\alpha}\,(\ell\Rightarrow
P_{\ell})_{\ell\in I})\,\mathcal{D}_{2}\mathbf{msg}(y_{\alpha}.k)\\\\[10.0pt]
(8)\mathcal{D}_{1}\mathbf{proc}(y_{\alpha},w\leftarrow\mathbf{recv}\,y_{\alpha})\,\mathcal{D}_{2}&\xrightarrow{{\mathbf{R}\,y_{\alpha}\,x_{\beta}}}&\mathcal{D}_{1}\mathbf{proc}(y_{\alpha},w\leftarrow\mathbf{recv}\,y_{\alpha})\mathcal{D}_{2}\,\mathbf{msg}(\mathbf{send}\,x_{\beta}\,y_{\alpha})\end{array}$

Figure 7. Labeled transition system induced by RSLR.

Our adequacy theorem (Lem. 8) shows that RSLRs are sound and complete with
regard to asynchronous bisimilarity.

###### Lemma 0 (Adequacy).

For all $(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathsf{Tree}(\Delta\Vdash K)$,
we have $\forall
m.(\mathcal{D}_{1};\mathcal{D}_{2})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket^{m}$ and $\forall
m.(\mathcal{D}_{2};\mathcal{D}_{1})\in\mathcal{E}\llbracket\Delta\Vdash
K\rrbracket^{m}$ iff $\mathcal{D}_{1}\approx_{\mathsf{a}}\mathcal{D}_{2}$.

###### Proof.

The result is a corollary of Lem. LABEL:APX:apx:lem:soundness-completeness on
page LABEL:APX:apx:lem:soundness-completeness in the Appendix. ∎

###  3.5. Biorthogonality

To define our main result, that the relation $\equiv$ is sound and complete
with regard to closure of weak bisimilarity under parallel composition (Thm.
12), we define an _orthogonality_ operation $\top$ (Pitts, 2000; Melliès and
Vouillon, 2005; Benton and Hur, 2009), leading to Def. 11. We follow Pitts
(2000)’ development. The impetus to connect RSLRs with biorthogonality we
received from reading Benton and Hur (2009)’s generalized description of
biorthogonality.

We first have to define the program relations $\mathit{PRel}(\Delta\Vdash K)$
and environment relations $\mathit{ERel}(\Delta\Vdash K)$ (Def. 10), reliant
upon the definition of a session-typed environment (Def. 9).

###### Definition 0 (Session-typed environment).

A session-typed environment with the interface $\Delta\Vdash K$, is of the
form $\mathcal{C}[\,\,]\mathcal{F}$, such that for some $\Delta^{\prime}$ and
$K^{\prime}$, we have $\Delta^{\prime}\Vdash\mathcal{C}::\Delta$ and
$K\Vdash\mathcal{F}::K^{\prime}$.

###### Definition 0 (Program- and environment- relations).

A session program-relation is a binary relation between session-typed
programs, i.e., open configurations of the form $\Delta\Vdash\mathcal{D}::K$.
Given the interface $\Delta\Vdash K$, we write $\mathit{PRel}(\Delta\Vdash K)$
for the set of all program relations that relate programs
$\Delta\Vdash\mathcal{D}::K$.

A session environment-relation is a binary relation between session-typed
environments. Given the interface $\Delta\Vdash K$, we write
$\mathit{ERel}(\Delta\Vdash K)$ for the set of all environment relations that
relate environments $\mathcal{C}[\,\,]\mathcal{F}$ with the interface
$\Delta\Vdash K$.

We can now define the orthogonality operation $\top$ (Pitts, 2000; Melliès and
Vouillon, 2005).

###### Definition 0 (The $(\\_)^{\top}$ operation on relations).

Given any interface $\Delta\Vdash K$ and $r\in\mathit{PRel}(\Delta\Vdash K)$,
we define $r^{\top}\in\mathit{ERel}(\Delta\Vdash K)$ by

$(\mathcal{C}_{1}[\,\,]\mathcal{F}_{1},\mathcal{C}_{2}[\,\,]\mathcal{F}_{2})\in
r^{\top}\,\,\mathsf{iff}\,\,\forall(\mathcal{D}_{1},\mathcal{D}_{2})\in
r.(\mathcal{C}_{1}\mathcal{D}_{1}\mathcal{F}_{1}\approx_{\mathsf{a}}\mathcal{C}_{2}\mathcal{D}_{2}\mathcal{F}_{2});$

and given any $s\in\mathit{ERel}(\Delta\Vdash K)$, we define
$s^{\top}\in\mathit{PRel}(\Delta\Vdash K)$ by

$(\mathcal{D}_{1},\mathcal{D}_{2})\in
s^{\top}\,\,\mathsf{iff}\,\,\forall(\mathcal{C}_{1}[\,\,]\mathcal{F}_{1},\mathcal{C}_{2}[\,\,]\mathcal{F}_{2})\in
s.(\mathcal{C}_{1}\mathcal{D}_{1}\mathcal{F}_{1}\approx_{\mathsf{a}}\mathcal{C}_{2}\mathcal{D}_{2}\mathcal{F}_{2}).$

As explained in (Pitts, 2000), just by virtue of its definition, we get that
the operation is a Galois connection, which is inflationary, and idempotent.

Finally, we can state our main result that the relation $\equiv$ is sound and
complete with regard to closure of weak bisimilarity under parallel
composition. The theorem relies on Def. 3 stated in § 3.3.

###### Theorem 12 ($\top\top$-closure).

Consider $(\mathcal{D}_{1},\mathcal{D}_{2})\in\mathsf{Tree}(\Delta\Vdash K)$,
we have

$\begin{array}[]{c}(\Delta\Vdash\mathcal{D}_{1}::K)\equiv(\Delta\Vdash\mathcal{D}_{2}::K)\\\\[5.0pt]
\mathbf{iff}\\\\[4.0pt]
\forall\mathcal{C}_{1},\mathcal{C}_{2},\mathcal{F}_{1},\mathcal{F}_{2}.\,\mathsf{s.t.}\,(\Delta\dashv\mathcal{C}_{1}[\,\,]\mathcal{F}_{1}\dashv
K)\equiv(\Delta\dashv\mathcal{C}_{2}[\,\,]\mathcal{F}_{2}\dashv
K)\,\,\mathsf{we\,have}\\\ \forall
m.\,{{\mathcal{C}_{1}}{\mathcal{D}_{1}}{\mathcal{F}_{1}}}\,\approx_{\mathsf{a}}\,\mathcal{C}_{2}{\mathcal{D}_{2}}{\mathcal{F}_{2}}\end{array}$

###### Proof.

See proof of Thm. LABEL:APX:apx:thm:biorthogonal on page
LABEL:APX:apx:thm:biorthogonal in the Appendix. ∎

##  4\. Noninterference

This section puts the developed RSLR to use. It develops a _refinement_ of
SESSION’s type system to prevent information flow, yielding the language
CONSESSION (§ 4.2). It then instantiates the RSLR to express equivalence up
to the secrecy level $\xi$ of an observer, $\equiv^{\Psi_{0}}_{\xi}$, given a
security lattice $\Psi_{0}$ (§ 4.3), to show that well-typed CONSESSION
programs enjoy PSNI (§ 4.4). Naturally, the refinement type system will
reject secure programs that are related by $\equiv^{\Psi_{0}}_{\xi}$, since
the RSLR delivers a _semantic_ equivalence for PSNI. The section concludes
with metatheoretic properties of $\equiv^{\Psi_{0}}_{\xi}$ (§ 4.5) and begins
with the attacker model.

###  4.1. Attacker model

Our attacker model is parametric in the secrecy level $\xi\in\Psi_{0}$ of an
attacker and a program $P$, given prior annotation of the free channels of $P$
with secrecy levels $c\in\Psi_{0}$. The model assumes

  * •

that the attacker knows the source code of $P$;

  * •

that the attacker can only observe the messages sent along the free channels
of $P$ with secrecy level $c\sqsubseteq\xi$;

  * •

assumes that an attacker cannot measure the passing of time;

  * •

assumes a nondeterministic scheduler.

###  4.2. IFC refinement type system

We now develop CONSESSION, a refinement of SESSION to prevent information
flow. Our development builds on prior work by Derakhshan et al. (2021), who
developed a _flow-sensitive_ IFC type system for ILLST, but restricted to the
terminating setting. We extend this work with support of general recursive
types and possibly recursive process definitions. The latter are _polymorphic_
in secrecy levels and can be type checked given a local security theory. A
_security theory_ $\Psi$, ranging over security variables $\psi$ and concrete
security levels drawn from the given security lattice $\Psi_{0}$ of an
application, such as the one for our banking example shown in § 2.1. At run-
time, all security variables will be replaced with concrete security levels.
Our type checker discussed in § 5.2 supports security theories.

The process term typing and configuration typing rules of CONSESSION are shown
in Fig. 8 and Fig. 9, resp. To type process terms, we use the judgment

$\Psi;\Xi\vdash_{\Sigma}P@c::x:A[d]$.

The new elements, compared to SESSION’s judgment (see § 2.2), is the security
theory $\Psi$ and the possible worlds annotations $@c$ and $[d]$ (Balzer et
al., 2019), to denote a process’ running secrecy and maximal secrecy, resp.
$\Xi$ is a linear typing context, like $\Delta$, but we use a different
metavariable because types now have maximal secrecy annotations. The idea is
that a process’ _maximal secrecy_ indicates the maximal level of secret
information the process may ever obtain, whereas a process’ _running secrecy_
denotes the highest level of secret information the process has obtained so
far.

$\displaystyle\oplus R$ $\displaystyle\displaystyle{\hbox{\hskip
61.56458pt\vbox{\hbox{\hskip-61.56456pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}P@d_{1}::y{:}A_{k}[c]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in
L$}}}}\vbox{}}}\over\hbox{\hskip
70.6891pt\vbox{\vbox{}\hbox{\hskip-70.6891pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}(y^{c}.k;P)@d_{1}::y{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in
L}[c]$}}}}}}$ $\displaystyle\oplus L$ $\displaystyle\displaystyle{\hbox{\hskip
114.15149pt\vbox{\hbox{\hskip-114.15147pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash
d_{2}=c\sqcup d_{1}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}A_{k}[c]\vdash_{\Sigma}Q_{k}@d_{2}::y{:}C[c^{\prime}]\quad\forall
k\in L$}}}}\vbox{}}}\over\hbox{\hskip
108.09775pt\vbox{\vbox{}\hbox{\hskip-108.09775pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L}[c]\vdash_{\Sigma}(\mathbf{case}\,x^{c}(\ell\Rightarrow Q_{\ell})_{\ell\in
L})@d_{1}::y{:}C[c^{\prime}]$}}}}}}$

$\displaystyle\&R$ $\displaystyle\displaystyle{\hbox{\hskip
66.59447pt\vbox{\hbox{\hskip-66.59447pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}Q_{k}@c::y{:}A_{k}[c]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall k\in
L$}}}}\vbox{}}}\over\hbox{\hskip
93.37259pt\vbox{\vbox{}\hbox{\hskip-93.37259pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}(\mathbf{case}\,y^{c}(\ell\Rightarrow
Q_{\ell})_{\ell\in I})@d_{1}::y{:}\&\\{\ell:A_{\ell}\\}_{\ell\in L}[c]$}}}}}}$
$\displaystyle\&L$ $\displaystyle\displaystyle{\hbox{\hskip
104.6146pt\vbox{\hbox{\hskip-104.6146pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash
d_{1}\sqsubseteq c$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}A_{k}[c]\vdash_{\Sigma}P@d_{1}::y{:}C[c^{\prime}]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle k\in
L$}}}}}\vbox{}}}\over\hbox{\hskip
87.87303pt\vbox{\vbox{}\hbox{\hskip-87.87303pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}\&\\{\ell:A_{\ell}\\}_{\ell\in
I}[c]\vdash_{\Sigma}(x^{c}.k;P)@d_{1}::y{:}C[c^{\prime}]$}}}}}}$

$\displaystyle\otimes R$ $\displaystyle\displaystyle{\hbox{\hskip
40.39047pt\vbox{\hbox{\hskip-40.39047pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}P@d_{1}::y{:}B[c]$}}}\vbox{}}}\over\hbox{\hskip
84.15244pt\vbox{\vbox{}\hbox{\hskip-84.15244pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,z{:}A[c]\vdash_{\Sigma}(\mathbf{send}\,z\,y^{c};P)@d_{1}::y{:}A\otimes
B[c]$}}}}}}$ $\displaystyle\otimes L$ $\displaystyle\displaystyle{\hbox{\hskip
105.40575pt\vbox{\hbox{\hskip-105.40573pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash
d_{2}=c\sqcup d_{1}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,z{:}A[c],x{:}B[c]\vdash_{\Sigma}P@d_{2}::y{:}C[c^{\prime}]$}}}}\vbox{}}}\over\hbox{\hskip
89.85645pt\vbox{\vbox{}\hbox{\hskip-89.85645pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}A\otimes
B[c]\vdash_{\Sigma}(z\leftarrow\mathbf{recv}\,x^{c};P)@d_{1}::y{:}C[c^{\prime}]$}}}}}}$

$\displaystyle\multimap R$ $\displaystyle\displaystyle{\hbox{\hskip
53.34872pt\vbox{\hbox{\hskip-53.34871pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,z{:}A[c]\vdash_{\Sigma}P@c::y{:}B[c]$}}}\vbox{}}}\over\hbox{\hskip
77.15192pt\vbox{\vbox{}\hbox{\hskip-77.1519pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}(z\leftarrow\mathbf{recv}\,y^{c};P)@d_{1}::y{:}A\multimap
B[c]$}}}}}}$ $\displaystyle\multimap L$
$\displaystyle\displaystyle{\hbox{\hskip
83.4405pt\vbox{\hbox{\hskip-83.44049pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash
d_{1}\sqsubseteq c$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}B[c]\vdash_{\Sigma}P@d_{1}::y{:}C[c^{\prime}]$}}}}\vbox{}}}\over\hbox{\hskip
100.857pt\vbox{\vbox{}\hbox{\hskip-100.85698pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,z{:}A[c],x{:}A\multimap
B[c]\vdash_{\Sigma}(\mathbf{send}\,z\,x^{c};P)@d_{1}::y{:}C[c^{\prime}]$}}}}}}$

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
51.22063pt\vbox{\vbox{}\hbox{\hskip-51.22061pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\cdot\vdash_{\Sigma}(\mathbf{close}\,y^{c})@d_{1}::y:1[c]$}}}}}}$
$1R$ $\displaystyle\displaystyle{\hbox{\hskip
43.22775pt\vbox{\hbox{\hskip-43.22774pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}Q@d_{1}::y:C[d]$}}}\vbox{}}}\over\hbox{\hskip
76.53447pt\vbox{\vbox{}\hbox{\hskip-76.53447pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x:1[c]\vdash_{\Sigma}(\mathbf{wait}\,x^{c};Q)@d_{1}::y:C[d]$}}}}}}$
$1L$

$\displaystyle\displaystyle{\hbox{\hskip
65.21591pt\vbox{\hbox{\hskip-65.21591pt\hbox{\hbox{$\displaystyle\displaystyle
Y=A\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}P::x{:}A[c]$}}}}\vbox{}}}\over\hbox{\hskip
34.71587pt\vbox{\vbox{}\hbox{\hskip-34.71585pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi\vdash_{\Sigma}P::x{:}Y[c]$}}}}}}$
$\mbox{\sc TVar}_{R}$ $\displaystyle\displaystyle{\hbox{\hskip
79.43506pt\vbox{\hbox{\hskip-79.43504pt\hbox{\hbox{$\displaystyle\displaystyle
Y=A\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}A[c]\vdash_{\Sigma}P::z{:}C[c^{\prime}]$}}}}\vbox{}}}\over\hbox{\hskip
48.935pt\vbox{\vbox{}\hbox{\hskip-48.935pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi,x{:}Y[c]\vdash_{\Sigma}P::z{:}C[c^{\prime}]$}}}}}}$
$\mbox{\sc TVar}_{L}$

$\displaystyle\displaystyle{\hbox{\hskip
180.65855pt\vbox{\hbox{\hskip-127.18884pt\hbox{\hbox{$\displaystyle\displaystyle\Psi^{\prime};\Xi_{1}^{\prime}\vdash_{\Sigma}X=P@\psi_{0}::x^{\prime}{:}A[\psi]\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash\gamma_{\mathsf{sec}}:\Psi^{\prime}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash\hat{\gamma_{\mathsf{sec}}}(\psi)\sqsubseteq
d$}}}}}\vbox{\hbox{\hskip-180.65854pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash
d_{0}\sqsubseteq\hat{\gamma_{\mathsf{sec}}}(\psi_{0})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Xi_{1},x{:}A[\hat{\gamma_{\mathsf{sec}}}(\psi_{0})]\Vdash(\gamma_{\mathsf{sec}},\gamma_{\mathsf{var}})::\Xi^{\prime}_{1},x^{\prime}{:}A[\psi]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi_{2},x{:}A[\hat{\gamma_{\mathsf{sec}}}(\psi)]\vdash_{\Sigma}Q@d_{0}::z{:}C[d]$}}}}}\vbox{}}}}\over\hbox{\hskip
121.54742pt\vbox{\vbox{}\hbox{\hskip-121.54742pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;\Xi_{1},\Xi_{2}\vdash_{\Sigma}((x^{[\hat{\gamma_{\mathsf{sec}}}(\psi)]}\leftarrow
X[(\gamma_{\mathsf{sec}},\gamma_{\mathsf{var}})]\leftarrow\Xi_{1})@\hat{\gamma_{\mathsf{sec}}}(\psi_{0});Q_{x})@d_{0}::z{:}C[d]$}}}}}}$
Spawn

$\displaystyle\displaystyle{\hbox{\hskip
151.44513pt\vbox{\hbox{\hskip-96.32469pt\hbox{\hbox{$\displaystyle\displaystyle\psi=\psi;z_{1}:C[\psi]\vdash_{\Sigma}F_{Y}=\mathtt{Fwd}_{C,x^{\psi}_{1}\leftarrow
z^{\psi}_{1}}@\psi::x_{1}{:}C[\psi]\in\Sigma$}}}\vbox{\hbox{\hskip-151.44513pt\hbox{\hbox{$\displaystyle\displaystyle
Y=A\in\Sigma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash\gamma_{\mathsf{sec}}:\psi=\psi$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
z{:}C[c],y{:}C[c]\Vdash(\gamma_{\mathsf{sec}},\gamma_{\mathsf{var}})::z_{1}{:}C[\psi],x_{1}{:}C[\psi]$}}}}}\vbox{}}}}\over\hbox{\hskip
69.76913pt\vbox{\vbox{}\hbox{\hskip-69.76913pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;z{:}C[c]\vdash_{\Sigma}F_{Y}[(\gamma_{\mathsf{sec}},\gamma_{\mathsf{var}})]@c::y{:}C[c]$}}}}}}$
D-Fwd

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
20.97502pt\vbox{\vbox{}\hbox{\hskip-20.97502pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma;\Psi_{0}}(\cdot)\;\mathbf{sig}$}}}}}}$
$\Sigma_{1}$ $\displaystyle\displaystyle{\hbox{\hskip
53.63058pt\vbox{\hbox{\hskip-53.63057pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma;\Psi_{0}}A\;\mathbf{contr}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma;\Psi_{0}}\Sigma^{\prime}\;\mathbf{sig}$}}}}\vbox{}}}\over\hbox{\hskip
35.15555pt\vbox{\vbox{}\hbox{\hskip-35.15553pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma;\Psi_{0}}Y=A,\Sigma^{\prime}\;\mathbf{sig}$}}}}}}$
$\Sigma_{2}$

$\displaystyle\displaystyle{\hbox{\hskip
194.12009pt\vbox{\hbox{\hskip-194.12007pt\hbox{\hbox{$\displaystyle\displaystyle\forall
i\in\\{1\dots n\\}.\Psi\Vdash\psi_{i}\sqsubseteq\psi$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\Vdash\psi_{0}\sqsubseteq\psi$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi;y_{1}{:}B_{1}[\psi_{1}],\dots,y_{n}{:}B_{n}[\psi_{n}]\vdash_{\Sigma}P@\psi_{0}::x{:}A[\psi]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma;\Psi_{0}}\Sigma^{\prime}\;\mathbf{sig}$}}}}}}\vbox{}}}\over\hbox{\hskip
112.22163pt\vbox{\vbox{}\hbox{\hskip-112.22162pt\hbox{\hbox{$\displaystyle\displaystyle\Vdash_{\Sigma;\Psi_{0}}\Psi;y_{1}{:}B_{1}[\psi_{1}],\dots,y_{n}{:}B_{n}[\psi_{n}]\vdash_{\Sigma}X=P@\psi_{0}::x{:}A[\psi],\Sigma^{\prime}\;\mathbf{sig}$}}}}}}$
$\Sigma_{3}$

Figure 8. Process term typing rules and signature checking rules of
CONSESSION.

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
43.83818pt\vbox{\vbox{}\hbox{\hskip-43.83817pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};x{:}A[d]\Vdash\cdot::(x{:}A[d])$}}}}}}$
$\mathbf{emp}_{1}$ $\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip 0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
20.26003pt\vbox{\vbox{}\hbox{\hskip-20.26001pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\cdot\Vdash\cdot::(\cdot)$}}}}}}$
$\mathbf{emp}_{2}$ $\displaystyle\displaystyle{\hbox{\hskip
66.70967pt\vbox{\hbox{\hskip-66.70966pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0}\Vdash\mathbb{C}::\Gamma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma^{\prime}_{0}\Vdash\mathcal{C}_{1}::x{:}A[d]$}}}}\vbox{}}}\over\hbox{\hskip
48.69963pt\vbox{\vbox{}\hbox{\hskip-48.69963pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0},\Gamma^{\prime}_{0}\Vdash\mathbb{C},\mathcal{C}_{1}::\Gamma,x{:}A[d]$}}}}}}$
$\mathbf{comp}$

$\displaystyle\displaystyle{\hbox{\hskip
167.96419pt\vbox{\hbox{\hskip-167.96417pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0}\Vdash
d_{1}\sqsubseteq d$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall
y{:}B[d^{\prime}]\in\Gamma^{\prime}_{0},\Gamma\,(\Psi_{0}\Vdash
d^{\prime}\sqsubseteq d)$}\hskip
18.00003pt\hbox{\hskip-151.52464pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0}\Vdash\mathbb{C}::\Gamma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}_{0},\Gamma,x_{\alpha}{:}A[d]\vdash\delta::\Xi^{\prime}_{0},\Xi,x{:}A[d]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Xi^{\prime}_{0},\Xi\vdash_{\Sigma}P@d_{1}::(x{:}A[d])$}}}}}}}}\vbox{\hbox{\hskip-151.52464pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0}\Vdash\mathbb{C}::\Gamma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}_{0},\Gamma,x_{\alpha}{:}A[d]\vdash\delta::\Xi^{\prime}_{0},\Xi,x{:}A[d]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Xi^{\prime}_{0},\Xi\vdash_{\Sigma}P@d_{1}::(x{:}A[d])$}}}}}\vbox{}}}}\over\hbox{\hskip
76.79498pt\vbox{\vbox{}\hbox{\hskip-76.79497pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0},\Gamma^{\prime}_{0}\Vdash\mathbb{C},\mathbf{proc}(x[d],P@d_{1})::(x{:}A[d])$}}}}}}$
$\mathbf{proc}$

$\displaystyle\displaystyle{\hbox{\hskip
141.86583pt\vbox{\hbox{\hskip-141.86581pt\hbox{\hbox{$\displaystyle\displaystyle\forall
y{:}B[d^{\prime}]\in\Gamma^{\prime}_{0},\Gamma\,(\Psi_{0}\Vdash
d^{\prime}\sqsubseteq d)$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0}\Vdash\mathbb{C}::\Gamma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma^{\prime}_{0},\Gamma\vdash
M::(x{:}A[d])$}}}}}\vbox{}}}\over\hbox{\hskip
60.75838pt\vbox{\vbox{}\hbox{\hskip-60.75838pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\Gamma_{0},\Gamma^{\prime}_{0}\Vdash\mathbb{C},\mathbf{msg}(M)::(x{:}A[d])$}}}}}}$
$\mathbf{msg}$

$\displaystyle\displaystyle{\hbox{\hskip
11.04689pt\vbox{\hbox{\hskip-11.04689pt\hbox{\hbox{$\displaystyle\displaystyle
k\in L$}}}\vbox{}}}\over\hbox{\hskip
73.30981pt\vbox{\vbox{}\hbox{\hskip-73.30981pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};y_{\alpha+1}{:}A_{k}[c]\vdash
y_{\alpha}.k::y_{\alpha}{:}\oplus\\{\ell{:}A_{\ell}\\}_{\ell\in L}[c]$}}}}}}$
$\mathbf{m}_{\oplus R}$ $\displaystyle\displaystyle{\hbox{\hskip
11.04689pt\vbox{\hbox{\hskip-11.04689pt\hbox{\hbox{$\displaystyle\displaystyle
k\in L$}}}\vbox{}}}\over\hbox{\hskip
85.41573pt\vbox{\vbox{}\hbox{\hskip-85.41573pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};x_{\alpha}{:}\&\\{\ell:A_{\ell}\\}_{\ell\in
I}[c]\vdash(x_{\alpha}.k;P)::x_{\alpha+1}{:}A_{k}[c]$}}}}}}$
$\mathbf{m}_{\&L}$

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
85.9967pt\vbox{\vbox{}\hbox{\hskip-85.99669pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};z_{\beta}{:}A[c],y_{\alpha+1}{:}B[c]\vdash\mathbf{send}\,z_{\beta}\,y_{\alpha}::y_{\alpha}{:}A\otimes
B[c]$}}}}}}$ $\mathbf{m}_{\otimes R}$

$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
88.60918pt\vbox{\vbox{}\hbox{\hskip-88.60916pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};z_{\beta}{:}A[c],x_{\alpha}{:}A\multimap
B[c]\vdash\mathbf{send}\,z_{\beta}\,x_{\alpha}::x_{\alpha+1}{:}B[c]$}}}}}}$
$\mathbf{m}_{\multimap L}$ $\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip 0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
39.69197pt\vbox{\vbox{}\hbox{\hskip-39.69196pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{0};\cdot\vdash\mathbf{close}\,y_{\alpha}::y_{\alpha}{:}1[c]$}}}}}}$
$\mathbf{m}_{1R}$

Figure 9. Configuration typing rules of CONSESSION.

To constrain the propagation of information, the following invariants are
presupposed on the typing judgment $\Psi;\Xi\vdash_{\Sigma}P@c::x:A[d]$:

  1. (i)

$\forall y{:}B[d^{\prime}]\in\Xi.\,\Psi\Vdash d^{\prime}\sqsubseteq d$

  2. (ii)

$\Psi\Vdash c\sqsubseteq d$

ensuring that the maximal secrecy of a child node is capped by the maximal
secrecy of its parent and that the running secrecy of a process is less than
or equal to its maximal secrecy, resp. Additionally, the type system ensures
that

  1. (1)

no channel of high secrecy is sent along one with lower secrecy; and

  2. (2)

a process does not send any message along a low-secrecy channel after receipt
of high secrecy information.

The first condition prevents direct flows and is enforced by requiring that
the maximal secrecy level of a carrier channel and the channels sent over it
match. The second condition is met by ensuring that a process’ running secrecy
is a sound approximation of the level of secret information a process has
obtained so far. To this end, the type system increases the running secrecy of
a process upon receipt to at least the maximal secrecy of the sending process
and, correspondingly, guards sends by making sure that the running secrecy of
the sending process is at most the maximal secrecy of the receiving process.

The typing rules in Fig. 8 look more verbose because of the secrecy labels,
but correspond to the typing rules of SESSION (Fig. 2), modulo necessary
premises for the presuppositions and above conditions. We leave it to the
reader to convince themselves that this is indeed the case, but briefly remark
on the handling of secrecy-polymorphic processes. Secrecy polymorphism
(a.k.a., label polymorphism (Gregersen et al., 2021)) allows processes to be
instantiated at varying secrecy levels. To ensure that instantiations respect
the presuppositions and conditions to ensure freedom of leakage, polymorphic
process definitions come equipped with constraints on their secrecy variables.
The body of a process is then verified assuming that these constraints are met
(rule $\Sigma_{3}$). It is the obligation of the caller—including the process
itself in case of a recursive call—to assert that the constraints are met for
the provided instantiations. Rule Spawn thus relies on an order-preserving
substitution mapping $\Psi\Vdash\gamma_{\mathsf{sec}}:\Psi^{\prime}$, provided
by the programmer, for secrecy variables in $\Psi^{\prime}$. The substitution
$\gamma_{\mathsf{sec}}$ identifies the specific instantiation provided by the
spawner in $\Psi$ to assert the constraints assumed by the spawnee in
$\Psi^{\prime}$ (see Def. LABEL:APX:apx:def:subst on page
LABEL:APX:apx:def:subst in the Appendix for more details). The premise
$\Psi\Vdash d_{0}\sqsubseteq\hat{\gamma_{\mathsf{sec}}}(\psi_{0})$ ensures
that the spawner’s level of secret information cannot surpass the one of the
spawnee, ruling out indirect flows. The premise
$\Psi\Vdash\hat{\gamma_{\mathsf{sec}}}(\psi)\sqsubseteq d$ preserves the
presuppositions.

The configuration typing rules (see Fig. 9) are as expected, and needed in the
proof of the fundamental theorem (§ 4.4). Dynamics is the one of SESSION
because of erasure of secrecy labels at run-time.

###  4.3. Up-to equivalence

To prove noninterference, we introduce an equivalence up to the secrecy level
$\xi$ of an observer relation, $\equiv^{\Psi_{0}}_{\xi}$, defined in Def. 3
below. This relation is reminiscent of logical equivalence $\equiv$ (see Def.
3), but expect free channels to be annotated with secrecy levels and allows
ignoring those channels with secrecy level $\sqsubseteq\xi$. We first define
two auxiliary notions: (i) downward projections on context of free channels
$\Gamma\Downarrow\xi$ and singleton offering free channel
$x_{\alpha}{:}T[c]\Downarrow\xi$ (Def. 1), as well as (ii) the predicates
$\mathbf{H\text{-}Provider}^{\xi}$ and $\mathbf{H\text{-}Client}^{\xi}$ (Def.
2).

###### Definition 0 (Typing context projections).

Downward projection on security linear contexts and $K^{s}$ is defined as
follows:

$\begin{array}[]{lclc}\Gamma,x_{\alpha}{:}T[c]\Downarrow\xi&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\Gamma\Downarrow\xi,x_{\alpha}{:}T[c]&\mathsf{if}\;c\sqsubseteq\xi\\\
\Gamma,x_{\alpha}{:}T[c]\Downarrow\xi&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\Gamma\Downarrow\xi&\mathsf{if}\;c\not\sqsubseteq\xi\\\
\cdot\Downarrow\xi&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\cdot&\\\
x_{\alpha}{:}T[c]\Downarrow\xi&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&x_{\alpha}{:}T[c]&\mathsf{if}\;c\sqsubseteq\xi\\\
x_{\alpha}{:}T[c]\Downarrow\xi&\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}&\\_{:}1[\top]&\mathsf{if}\;c\not\sqsubseteq\xi\\\ \end{array}$

###### Definition 0 (High provider and High client).

$\begin{array}[]{lll}\cdot\,\,\in\mathbf{H\text{-}Provider}^{\xi}(\cdot)\\\\[5.0pt]
\mathcal{B}\in\mathbf{H\text{-}Provider}^{\xi}(\Gamma,x_{\alpha}{:}A[c])&\mathsf{iff}&c\not\sqsubseteq\xi\,\mathsf{and}\,\mathcal{B}=\mathcal{B}^{\prime}\mathcal{T}\,\,\mathsf{and}\,\,\mathcal{B}^{\prime}\in\mathbf{H\text{-}Provider}^{\xi}(\Gamma)\,\,\mathsf{and}\\\
&&\,\,\mathcal{T}\in\mathsf{Tree}(\cdot\Vdash x_{\alpha}{:}A),\mathbf{or}\\\
&&c\sqsubseteq\xi\,\mathsf{and}\,\mathcal{B}\in\mathbf{H\text{-}Provider}^{\xi}(\Gamma)\\\\[10.0pt]
\mathcal{T}\in\mathbf{H\text{-}Client}^{\xi}(x_{\alpha}{:}A[c])&\mathsf{iff}&c\not\sqsubseteq\xi\,\mathsf{and}\,\mathcal{T}\in\mathsf{Tree}(x_{\alpha}{:}A\Vdash\\_:1),\mathbf{or}\\\
&&c\sqsubseteq\xi\,\mathsf{and}\,\mathcal{B}=\cdot\end{array}$

Finally, we can state the relation $\equiv^{\Psi_{0}}_{\xi}$. Like $\equiv$,
$\equiv^{\Psi_{0}}_{\xi}$ is phrased in terms of the term interpretation of
the RSLR, but restricts observations to those free channels that are
observable. The remaining free channels will be composed in parallel with
arbitrary ILLST-typed other configurations.

###### Definition 0 (Equivalence of trees by the logical relation upto the
observer level).

We define the relation
$(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A_{1}[{c_{1}}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}A_{2}[{c_{2}}])$
as

$\begin{array}[]{c}{\mathcal{D}_{1}}\in\mathsf{Tree}(\lvert\Gamma_{1}\rvert\Vdash
x_{\alpha}{:}A_{1})\,\,\mathsf{and}\,\,{\mathcal{D}_{2}}\in\mathsf{Tree}(\lvert\Gamma_{2}\rvert\Vdash
y_{\beta}{:}A_{2})\,\,\mathsf{and}\\\
\Gamma_{1}{\Downarrow}\xi=\Gamma_{2}{\Downarrow}\xi=\Gamma\,\,\mathsf{and}\,\,x_{\alpha}{:}A_{1}[{c_{1}}]{\Downarrow}\xi=y_{\beta}{:}A_{2}[{c_{2}}]{\Downarrow}\xi=K^{s}\,\,\mathsf{and}\\\
\forall\,\mathcal{B}_{1}\in\mathbf{H\text{-}Provider}^{\xi}(\Gamma_{1}).\,\forall\,\mathcal{B}_{2}\in\mathbf{H\text{-}Provider}^{\xi}(\Gamma_{2}).\,\forall\mathcal{T}_{1}\in\mathbf{H\text{-}Client}^{\xi}(x_{\alpha}{:}A_{1}[{c_{1}}]).\,\forall\mathcal{T}_{2}\in\mathbf{H\text{-}Client}^{\xi}(y_{\beta}{:}A_{2}[{c_{2}}]).\\\
\forall\,m.\,(\mathcal{B}_{1}\mathcal{D}_{1}\mathcal{T}_{1},\mathcal{B}_{2}\mathcal{D}_{2}\mathcal{T}_{2})\in\mathcal{E}\llbracket\lvert\Gamma\rvert\Vdash\lvert
K^{s}\rvert\rrbracket^{m},\,\mathsf{and}\\\\[1.0pt]
\forall\,m.\,(\mathcal{B}_{2}\mathcal{D}_{2}\mathcal{T}_{2},\mathcal{B}_{1}\mathcal{D}_{1}\mathcal{T}_{1})\in\mathcal{E}\llbracket\lvert\Gamma\rvert\Vdash\lvert
K^{s}\rvert\rrbracket^{m}.\end{array}$

The fundamental theorem, which asserts that CONSESSION-typed configurations
are related by the term interpretation of the RSLR, is phrased in terms of
$\equiv^{\Psi_{0}}_{\xi}$. Since CONSESSION types contain security
annotations, but the types in the logical relation’s interface lack security
annotations, Def. 3 makes use of an erasure operation $\lvert\\_\rvert$. Thus,
$\equiv^{\Psi_{0}}_{\xi}$ can be used for IFC-typed CONSESSION configurations
as well as “plain-vanilla” ILLST-typed configurations, facilitating _semantic_
typing for PSNI.

To illustrate $\equiv^{\Psi_{0}}_{\xi}$, we instantiate it on a simplistic
example, in the spirit of the $\mathsf{SneakyVerifier}$ encountered earlier,
shown below. Let’s assume that our security lattice ($\Psi_{0}$) is
$\mathbf{guest}\sqsubseteq\mathbf{alice}$, and that the attacker level is
$\mathbf{guest}$.

$\mathsf{pin}$ $=$ | $\&\\{$ | $\mathit{tok_{1}}{:}\mathsf{1},\mathit{tok_{2}}{:}\mathsf{1}\\}$
---|---|---
$\mathsf{bit}=\&\\{\mathit{zero}{:}\mathsf{1},\mathit{one}{:}\mathsf{1}\\}$
$y{:}\mathsf{bit}[\mathbf{guest}]\vdash\mathsf{XX}::x{:}\mathsf{pin}[\mathbf{alice}]$
---
$x\leftarrow\mathsf{XX}\leftarrow y=($
| $\mathbf{case}\,x\,($ |  $\mathit{tok}_{1}\Rightarrow y.\mathit{zero};\mathbf{wait}\,y;\,\mathbf{close}\,x,\,\mid\mathit{tok}_{2}\Rightarrow y.\mathit{one};\mathbf{wait}\,y;\,\mathbf{close}\,x))$

Process $\mathsf{XX}$ provides a free channel variable $x$, which is not
observable to the attacker, and uses a low-secrecy free channel variable $y$,
which the attacker can observe. The process receives either $\mathit{tok}_{1}$
or $\mathit{tok}_{2}$ from $x$, and sends either bit $\mathit{zero}$ or bit
$\mathit{one}$ along $y$, depending on which token it receives. After that, it
terminates. To prove that this process is secure, we would have to show that
for any substitution that instantiates free variables $x$ and $y$ with free
channels $x_{\alpha}$ and $y_{\beta}$

$y_{\beta}:\mathsf{bit}[\mathbf{guest}]\Vdash\mathbf{proc}(x_{\alpha},\mathsf{XX})::x_{\alpha}{:}\mathsf{pin}[\mathbf{alice}]\equiv^{\Psi_{0}}_{\mathbf{guest}}y_{\beta}:\mathsf{bit}[\mathbf{guest}]\Vdash\mathbf{proc}(x_{\alpha},\mathsf{XX})::x_{\alpha}{:}\mathsf{pin}[\mathbf{alice}]$

We compose the process with the following high-secrecy clients
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, sending different tokens along the
high-secrecy channel $x_{\alpha}{:}\mathsf{pin}[\mathbf{alice}]$.

$\mathcal{T}_{1}=\mathbf{proc}(z_{\eta},x_{\alpha}.\mathit{tok}_{1};\mathbf{wait}\,x_{\alpha};\mathbf{close}\,z_{\eta})\qquad\mathcal{T}_{2}=\mathbf{proc}(z_{\eta},x_{\alpha}.\mathit{tok}_{2};\mathbf{wait}\,x_{\alpha};\mathbf{close}\,z_{\eta})$

We link these high-secrecy environments with process $\mathsf{XX}$, leaving us
left to show that for all $m$:

$\begin{array}[]{r}({\color[rgb]{0.4,0,0}\mathbf{proc}(x_{\alpha},\mathsf{XX})\,\mathbf{proc}(z_{\eta},x_{\alpha}.\mathit{tok}_{1};\mathbf{wait}\,x_{\alpha};\mathbf{close}\,z_{\eta})};{\color[rgb]{0,0,1}\mathbf{proc}(x_{\alpha},\mathsf{XX})\,\mathbf{proc}(z_{\eta},x_{\alpha}.\mathit{tok}_{2};\mathbf{wait}\,x_{\alpha};\mathbf{close}\,z_{\eta})})\\\
\in\mathcal{E}\llbracket
y_{\beta}{:}\mathsf{bit}\vdash\\_{:}1\rrbracket^{m}\end{array}$

Obviously this does not hold true, confirming that process $\mathsf{XX}$ is
insecure. Similarly, the process would be rejected by the CONSESSION type
checker. Consider a variant of $\mathsf{XX}$ that sends the bit
$\mathit{zero}$ in either case. This variant would be accepted by the logical
relation, since it is secure, but rejected by the CONSESSION type checker,
showcasing that our RSLR is a semantic relation for PSNI.

###  4.4. Fundamental theorem

We are now in a position to state the fundamental theorem, asserting that
CONSESSION-typed programs are self-related, as an immediate corollary (see
Lem. 7).

###### Theorem 4 (Fundamental Theorem).

For all security levels $\xi$, and configurations

${\Psi;\Gamma_{1}\Vdash\mathbb{D}_{1}::u_{\alpha}{:}T_{1}[c_{1}]},\,\,\textit{and}\,\,{\Psi;\Gamma_{2}\Vdash\mathbb{D}_{2}::v_{\beta}{:}T_{2}[c_{2}]},$

with $\mathbb{D}_{1}{\Downarrow}\xi=_{\xi}\mathbb{D}_{2}{\Downarrow}\xi$,
$\Gamma_{1}\Downarrow\xi=\Gamma_{2}\Downarrow\xi$, and
$u_{\alpha}{:}T_{1}[c_{1}]\Downarrow\xi=v_{\beta}{:}T_{2}[c_{2}]\Downarrow\xi$
we have

$(\Gamma_{1}\Vdash\mathbb{D}_{1}::u_{\alpha}{:}T_{1}[c_{1}])\equiv^{\Psi}_{\xi}(\Gamma_{2}\Vdash\mathbb{D}_{2}::v_{\beta}{:}T_{2}[c_{2}]).$

###### Proof.

See proof of Thm. LABEL:APX:apx:thm:ftlr on page LABEL:APX:apx:thm:ftlr in the
Appendix. ∎

To strengthen the inductive hypothesis, Thm. 4 relies on the notion of
_relevant nodes_ of a configuration $\mathbb{D}{\Downarrow}\xi$, introduced by
Derakhshan et al. (2021), and the invariant that the relevant nodes in both
configurations execute the same code
$\mathbb{D}_{1}{\Downarrow}\xi=_{\xi}\mathbb{D}_{2}{\Downarrow}\xi$. Def. 5
gives the formal definition of a relevant node, but intuitively we can think
of the relevant nodes as those processes in a configuration who can either
directly or indirectly cause a message to be sent along a free channel in the
interface of the logical relation. This invariant is maintained in the proof
and crucial to keep the two configurations in sync.

The definition of relevant nodes relies on quasi-running secrecy (Derakhshan
et al., 2021), which provides a more accurate handling of receives. We refer
the interested reader to Def. LABEL:APX:apx:def:quasi on page
LABEL:APX:apx:def:quasi in the Appendix for its definition.

###### Definition 0 (Relevant node).

Consider a configuration $\Gamma\Vdash\mathbb{D}::K^{s}$ and observer level
$\xi$. A channel is relevant in $\mathbb{D}$ if (1) it has a maximal secrecy
level less than or equal to $\xi$, and (2) it is either an observable channel
or it shares a process or message with quasi-running secrecy less than or
equal to $\xi$ with a relevant channel. (A channel shares a process with
another channel if they are siblings or one is the parent of another.) A
process or message is relevant if (1) it has quasi-running secrecy less than
or equal to $\xi$, and (2) it has at least one relevant channel. We denote the
relevant processes and messages (i.e., nodes) in $\mathbb{D}$ by
$\mathbb{D}{\Downarrow}\xi$. We write
$\mathbb{D}_{1}{\Downarrow}\xi=_{\xi}\mathbb{D}_{2}{\Downarrow}\xi$ if the
relevant nodes in $\mathbb{D}_{1}$ are identical to those in $\mathbb{D}_{2}$
up to renaming of channels with higher or incomparable secrecy than the
observer.

###  4.5. Metatheoretic properties of up-to equivalence

Unsurprisingly, $\equiv^{\Psi_{0}}_{\xi}$ has analogous properties to
$\equiv$, except for reflexivity (Lem. 7), which only holds true for IFC-typed
configurations, as demonstrated by our $XX$ process in § 4.3.

####  4.5.1. Linking: closure under parallel composition

###### Lemma 0 (Linking).

If

$\begin{array}[]{lll}(i)&(\Gamma^{\prime}_{1}\Vdash\mathcal{C}_{1}::\Gamma)\equiv^{\xi}_{\Psi_{0}}(\Gamma^{\prime}_{2}\Vdash\mathcal{C}_{2}::\Gamma)\,\,\mathsf{with}\,\,\Gamma=\Gamma_{1}\Downarrow_{\xi}=\Gamma_{2}\Downarrow_{\xi}\,\,\mathsf{and}\\\
(ii)&(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A_{1}[c_{1}])\equiv^{\xi}_{\Psi_{0}}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}A_{2}[c_{2}])\,\mathsf{and}\\\
(iii)&(K^{s}\Vdash\mathcal{F}_{1}::K^{s}_{1})\equiv^{\xi}_{\Psi_{0}}(K^{s}\Vdash\mathcal{F}_{2}::K^{s}_{2})\,\,\mathsf{with}\,K^{s}=x_{\alpha}{:}A_{1}[c_{1}]\Downarrow\xi=y_{\beta}{:}A_{2}[c_{2}]\Downarrow\xi\,\mathsf{then}\\\
&(\Gamma^{\prime}_{1},\Gamma^{h}_{1}\Vdash\mathcal{C}_{1}\mathcal{D}_{1}\mathcal{F}_{1}::K^{s}_{1})\equiv^{\xi}_{\Psi_{0}}(\Gamma^{\prime}_{2},\Gamma^{h}_{2}\Vdash\mathcal{C}_{2}\mathcal{D}_{2}\mathcal{F}_{2}::K^{s}_{2}),\end{array}$

where $\Gamma^{h}_{1}$ is the set of all channels
$w_{\eta}{:}C[d]\in\Gamma_{1}$ with $d\not\sqsubseteq\xi$ and $\Gamma^{h}_{2}$
is the set of all channels $w_{\eta}{:}C[d]\in\Gamma_{2}$ with
$d\not\sqsubseteq\xi$.

###### Proof.

See Lem. LABEL:APX:apx:lem:compositionality-eq on page
LABEL:APX:apx:lem:compositionality-eq in the Appendix. ∎

####  4.5.2. Partial equivalence relation (PER)

###### Lemma 0 (Reflexivity – only for IFC-typed processes).

For all security levels $\xi$ and configurations
$\Psi_{0};\Gamma\Vdash\mathbb{D}::x_{\alpha}{:}T[c]$, we have

$(\Gamma\Vdash\lvert\mathbb{D}\rvert::x_{\alpha}{:}T[c])\equiv^{\Psi_{0}}_{\xi}(\Gamma\Vdash\lvert\mathbb{D}\rvert::x_{\alpha}{:}T[c]).$

###### Proof.

See proof of Lem. LABEL:APX:apx:lem:reflexivity on page
LABEL:APX:apx:lem:reflexivity in the Appendix. ∎

###### Lemma 0 (Symmetry).

For all security levels $\xi$ and configurations $\mathcal{D}_{1}$ and
$\mathcal{D}_{2}$, we have
$(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T_{1}[c_{1}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}T_{2}[c_{2}]),$
iff
$(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}T_{2}[c_{2}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T_{1}[c_{1}]).$

###### Proof.

See proof of Lem. LABEL:APX:apx:lem:symmetry on page
LABEL:APX:apx:lem:symmetry in the Appendix. ∎

###### Lemma 0 (Transitivity).

For all security levels $\xi$, and configurations $\mathcal{D}_{1}$,
$\mathcal{D}_{2}$, and $\mathcal{D}_{3}$, we have

$\begin{array}[]{c}\mathsf{if}\,(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T_{1}[c_{1}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}T_{2}[c_{2}])\,\mathsf{and}\,(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}T_{2}[c_{2}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{3}\Vdash\mathcal{D}_{3}::z_{\eta}{:}T_{3}[c_{3}])\\\
\mathsf{then}\,(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}T_{1}[c_{1}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{3}\Vdash\mathcal{D}_{3}::z_{\eta}{:}T_{3}[c_{3}]).\end{array}$

###### Proof.

See proof of Cor. LABEL:APX:apx:cor:transitivity on page
LABEL:APX:apx:cor:transitivity in the Appendix. ∎

####  4.5.3. Adequacy

###### Definition 0 (Bisimulation with secrecy annotated- interface).

For $\,\mathcal{D}_{1}\in\mathsf{Tree}(\lvert\Gamma_{1}\rvert\Vdash
x_{\alpha}{:}A_{1})$,
$\mathcal{D}_{2}\in\mathsf{Tree}(\lvert\Gamma_{2}\rvert\Vdash
y_{\beta}{:}A_{2})\,$ we define
$\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A_{1}[c_{1}]\approx_{\mathsf{a}}^{\xi}\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}A_{2}[c_{2}]$
as

$\begin{array}[]{c}\Gamma_{1}\Downarrow\xi=\Gamma_{2},\Downarrow\xi\,\,\,\mathsf{and}\,\,\,y_{\beta}{:}A_{2}[c_{2}]\Downarrow\xi=x_{\alpha}{:}A_{1}[c_{1}]\Downarrow\xi\,\,\,\mathsf{and}\\\
\forall\mathcal{B}_{1}\in\mathsf{H\text{-}Provider}^{\xi}(\Gamma_{1}),\mathcal{B}_{2}\in\mathsf{H\text{-}Provider}^{\xi}(\Gamma_{2}),\mathcal{T}_{1}\in\mathsf{H\text{-}CLient}^{\xi}(x_{\alpha}{:}A_{1}[c_{1}]),\,\mathcal{T}_{2}\in\mathsf{H\text{-}Client}^{\xi}(y_{\beta}{:}A_{2}[c_{2}]).\\\
\mathcal{B}_{1}\mathcal{D}_{1}\mathcal{T}_{1}\approx_{\mathsf{a}}\mathcal{B}_{2}\mathcal{D}_{2}\mathcal{T}_{2}.\end{array}$

###### Lemma 0 (Soundness and Completeness).

For all $\mathcal{D}_{1}\in\mathsf{Tree}(\lvert\Gamma_{1}\rvert\Vdash
x_{\alpha}{:}A_{1})$ and
$\mathcal{D}_{2}\in\mathsf{Tree}(\lvert\Gamma_{2}\rvert\Vdash
y_{\beta}{:}A_{2})$, we have
$(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A_{1}[{c_{1}}])\equiv^{\Psi_{0}}_{\xi}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}A_{2}[{c_{2}}])$
iff
$(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A_{1}[{c_{1}}])\approx_{\mathsf{a}}^{\xi}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}A_{2}[{c_{2}}])$.

###### Proof.

See proof of Cor. LABEL:APX:apx:cor:eq-soundness-completeness on page
LABEL:APX:apx:cor:eq-soundness-completeness in the Appendix. ∎

####  4.5.4. Biorthogonality

###### Theorem 12 ($\top\top$-closure).

Consider $\mathcal{D}_{1}\in\mathsf{Tree}(\lvert\Gamma_{1}\rvert\Vdash\lvert
x_{\alpha}{:}A_{1}[c_{1}]\rvert)$ and
$\mathcal{D}_{2}\in\mathsf{Tree}(\lvert\Gamma_{2}\rvert\Vdash\lvert
y_{\beta}{:}A_{2}[c_{2}]\rvert)$ and a given observer level $\xi\in\Psi_{0}$.
We have

$\begin{array}[]{c}(\Gamma_{1}\Vdash\mathcal{D}_{1}::x_{\alpha}{:}A_{1}[c_{1}])\equiv^{\xi}_{\Psi_{0}}(\Gamma_{2}\Vdash\mathcal{D}_{2}::y_{\beta}{:}A_{2}[c_{2}])\\\\[5.0pt]
\mathbf{iff}\\\\[4.0pt]
\forall\mathcal{C}_{1},\mathcal{C}_{2},\mathcal{F}_{1},\mathcal{F}_{2}.\,\mathsf{s.t.}\,(\Gamma_{1}\dashv\mathcal{C}_{1}[\,\,]\mathcal{F}_{1}\dashv
x_{\alpha}{:}A_{1}[c_{1}])\equiv^{\xi}_{\Psi_{0}}(\Gamma_{2}\dashv\mathcal{C}_{2}[\,\,]\mathcal{F}_{2}\dashv
y_{\beta}{:}A_{2}[c_{2}])\,\,\mathsf{we\,have}\\\
\forall\mathcal{B}_{1}\in\mathsf{H\text{-}Provider}^{\xi}(\Gamma_{1}),\mathcal{B}_{2}\in\mathsf{H\text{-}Provider}^{\xi}(\Gamma_{2}),\mathcal{T}_{1}\in\mathsf{H\text{-}CLient}^{\xi}(x_{\alpha}{:}A_{1}[c_{1}]),\,\mathcal{T}_{2}\in\mathsf{H\text{-}Client}^{\xi}(y_{\beta}{:}A_{2}[c_{2}]).\\\
{\mathcal{B}_{1}{\mathcal{C}_{1}}{\mathcal{D}_{1}}{\mathcal{F}_{1}}\mathcal{T}_{1}}\,\approx_{\mathsf{a}}\,\mathcal{B}_{2}\mathcal{C}_{2}{\mathcal{D}_{2}}{\mathcal{F}_{2}}\mathcal{T}_{2}\end{array}$

###### Proof.

See proof of Thm. LABEL:APX:apx:thm:biorthogonal-sc on page
LABEL:APX:apx:thm:biorthogonal-sc in the Appendix. ∎

##  5\. Evaluation

This section provides an example with secrecy-polymorphic processes and
comments on our type checker implementation.

###  5.1. Secrecy-polymorphic processes to the rescue

As a bonus to our polymorphic treatment of processes, we get to define generic
process definitions! This section completes our banking example by providing
generic implementations for a customer and its authorization process that can
be spawned for any specific customer of the bank. We remind the reader that
the session type definitions of our banking example can be found in Fig. 1
(b).

The bank sets up a new customer by sending the customer an authentication PIN
and an authorization process that guards their account.

$\Psi;y_{1}{:}\,\mathsf{customer}{\color[rgb]{0.72,0,0}[\psi_{1}]},u_{1}{:}\,\mathsf{pin}{\color[rgb]{0.72,0,0}[\psi_{1}]},z_{1}{:}\mathsf{auth_{out}}{\color[rgb]{0.72,0,0}[\psi_{1}]},$
$\Psi{:=}\psi_{1}{=}\mathbf{alice},\psi_{2}{=}\mathbf{bob},\psi{=}\mathbf{bank},\psi^{\prime}{=}\mathbf{guest},\Psi_{0}$
---
$y_{2}{:}\,\mathsf{customer}{\color[rgb]{0.72,0,0}[\psi_{2}]},u_{2}{:}\mathsf{pin}{\color[rgb]{0.72,0,0}[\psi_{2}]},z_{2}{:}\mathsf{auth_{out}}{\color[rgb]{0.72,0,0}[\psi_{2}]}\vdash\mathsf{Bank}::w{:}1{\color[rgb]{0.72,0,0}[\psi]}$
$w\leftarrow\mathsf{Bank}{\color[rgb]{0,0.6,0}@\psi^{\prime}}\leftarrow y=($ |  $\mathbf{send}\,u_{1}^{\psi_{1}}\,y_{1};\mathbf{send}\,z_{1}^{\psi_{1}}\,y_{1};\mathbf{send}u_{2}^{\psi_{2}}\,y_{2};\mathbf{send}\,z_{2}^{\psi_{2}}\,y_{2};\mathbf{wait}\,y_{1};\mathbf{wait}y_{2};\mathbf{close}w$)
$\Psi_{1};\cdot\vdash\mathsf{New\\_Customer}{\color[rgb]{0,0.6,0}@\mathbf{\psi^{\prime}}}::y{:}\,\mathsf{customer}{\color[rgb]{0.72,0,0}[\psi]}$
$\Psi_{1}:=\psi^{\prime}\sqsubseteq\psi,\Psi_{0}$
$y\leftarrow\mathsf{New\\_Customer}\leftarrow\cdot=($ |  $u^{\psi}\leftarrow\mathbf{recv}\,y;z^{\psi}\leftarrow\mathbf{recv}\,y;$ // $u{:}\mathsf{pin}[\psi],z{:}\mathsf{auth_{out}}[\psi]\vdash y{:}1[\psi]$
|
$y^{\hat{\gamma}(\psi)}{:}1\leftarrow\mathsf{Customer}[\gamma_{1}]{\color[rgb]{0,0.6,0}@\mathbf{\hat{\gamma}(\psi^{\prime})}}\leftarrow
u{:}\mathsf{pin},z{:}\mathsf{auth_{out}}){\color[rgb]{0,0.6,0}@\mathbf{\psi^{\prime}}}$

where
$\gamma_{1}:=\\{\psi\mapsto\mathbf{bank},\psi_{1}\mapsto\mathbf{alice},\psi_{2}\mapsto\mathbf{bob},\psi^{\prime}\mapsto\mathbf{guest}\\}$.

The types $\mathsf{auth_{out}}$ and $\mathsf{auth_{in}}$ describe the
communication of the authorization process with the customer. The
authorization process receives a PIN from the customer and sends it to the
verifier to validate the login. If the verifier process signals a successful
verification, the authorization goes ahead and logs in the customer by sending
a $\mathit{succ}$ label, followed by the account to the customer. If the PIN
verification is unsuccessful, the authorization process returns the incorrect
PIN to the customer and remains logged out. In the case of a successful
verification, the customer remains logged in until it requests a log out by
sending back its account to the authorization process; upon such a request,
the account sends back the PIN to the customer and logs them out.

$\Psi_{1};x{:}\mathsf{ver}{\color[rgb]{0.72,0,0}[\psi]},v{:}\mathsf{account}{\color[rgb]{0.72,0,0}[\psi]}\vdash\mathsf{Auth_{out}}{\color[rgb]{0,0.6,0}@\psi^{\prime}}::z{:}\,\mathsf{auth_{out}}{\color[rgb]{0.72,0,0}[\psi]}$
$\Psi_{1}=\psi^{\prime}\sqsubseteq\psi,\Psi_{0}$
---
$z{:}\mathsf{auth_{out}}\leftarrow\mathsf{Auth_{out}}\leftarrow
x{:}\mathsf{ver},v{:}\mathsf{account}=($ //
$x{:}\mathsf{ver},v{:}\mathsf{account}\vdash z{:}\mathsf{auth_{out}}$
| $w_{3}^{\psi}\leftarrow\mathbf{recv}\,z;\mathbf{send}w_{3}^{\psi}x;$
| $\mathbf{case}\,x\,($ | $\mathit{succ}\Rightarrow$ |  $z.\mathit{succ};\mathbf{send}v^{\psi}z;$ // $x{:}\mathsf{pin}\otimes\mathsf{ver}\vdash z{:}\mathsf{auth_{in}}$
|  |  | $(z^{\psi}{:}\mathsf{auth_{in}}\leftarrow\mathsf{Auth_{in}}[\gamma_{2}]{\color[rgb]{0,0.6,0}@\mathbf{\psi}}\leftarrow x{:}\mathsf{pin}\otimes\mathsf{ver})$
|  |  $\mid\mathit{fail}\Rightarrow w^{\psi}_{4}\leftarrow\mathbf{recv}x;\mathbf{send}w_{4}^{\psi}z;$ // $x{:}\mathsf{ver},v{:}\mathsf{account}\vdash z{:}\mathsf{auth_{out}}$
|  |  | $(z^{\psi}{:}\mathsf{auth_{out}}\leftarrow\mathsf{Auth_{out}}[\gamma_{2}]{\color[rgb]{0,0.6,0}@\mathbf{\psi}}\leftarrow x{:}\mathsf{ver},v{:}\mathsf{account}))){\color[rgb]{0,0.6,0}@\mathbf{\psi^{\prime}}}$
$\Psi_{1};x{:}\mathsf{pin}\otimes\mathsf{ver}{\color[rgb]{0.72,0,0}[\psi]}\vdash\mathsf{Auth_{in}}{\color[rgb]{0,0.6,0}@\psi^{\prime}}::z{:}\,\mathsf{auth_{in}}{\color[rgb]{0.72,0,0}[\psi]}$
$\Psi_{1}=\psi^{\prime}\sqsubseteq\psi,\Psi_{0}$
$z{:}\mathsf{auth_{in}}\leftarrow\mathsf{Auth_{in}}\leftarrow
x{:}\mathsf{pin}\otimes\mathsf{ver}=($
|
$v^{\psi}\leftarrow\mathbf{recv}\,z;w_{5}^{\psi}\leftarrow\mathbf{recv}x;\mathbf{send}w^{\psi}_{5}z;$
// $x{:}\mathsf{ver},v{:}\mathsf{account}\vdash z{:}\mathsf{auth_{out}}\\}$
|
$(z^{\psi}{:}\mathsf{auth_{out}}\leftarrow\mathsf{Auth_{out}}[\gamma_{2}]{\color[rgb]{0,0.6,0}@\psi}\leftarrow
x{:}\mathsf{ver},v{:}\mathsf{account}))){\color[rgb]{0,0.6,0}@\psi^{\prime}}$
$\Psi_{1};u{:}\mathsf{pin}{\color[rgb]{0.72,0,0}[\psi]},z{:}\mathsf{auth_{out}}{\color[rgb]{0.72,0,0}[\psi]}\vdash\mathsf{Customer}{\color[rgb]{0,0.6,0}@\psi^{\prime}}::y{:}\,\mathsf{1}{\color[rgb]{0.72,0,0}[\psi]}$
$\Psi_{1}=\psi^{\prime}\sqsubseteq\psi,\Psi_{0}$
$y\leftarrow\mathsf{Customer}\leftarrow\cdot=($ //
$u{:}\mathsf{pin},z{:}\mathsf{auth_{out}}\vdash y{:}\mathsf{customer}$