A Bisimulation for Dynamic Sealing^{∗}

Eijiro Sumii Tohoku University^{†}

Benjamin C. Pierce University of Pennsylvania

Abstract

We define λ_{seal}, an untyped call-by-value λ-calculus with primitives for protecting abstract data by sealing, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. This provides a formal basis for reasoning about data abstraction in open, dynamic settings where static techniques such as type abstraction and logical relations are not applicable.

1 Introduction

1.1 Dynamic sealing: Birth, death, and rebirth

Sealing is a linguistic mechanism for protecting abstract data. As originally proposed by Morris [20, 21], it consists of three constructs: seal creation, sealing, and unsealing. A fresh seal is created for each module that defines abstract data. Data is sealed when it is passed out of the module, so that it cannot be inspected or modified by outsiders who do not know the seal; the data is unsealed again when it comes back into the module, so that it can be manipulated concretely. Data abstraction is preserved as long as the seal is kept local to the module.

Originally, sealing was a dynamic mechanism. Morris also proposed a static variant [21], in which the creation and use of seals at module boundaries follow a restricted pattern that can be verified by the compiler, removing the need for run-time sealing and unsealing. Other researchers found that a similar effect could be obtained by enriching a static type system with mechanisms for type abstraction (see CLU [14], for example). Type abstraction became the primary method for achieving data abstraction in languages from CLU to the present day. It is also well understood via the theory of existential types [18].

Recently, however, as programming languages and the environments in which they operate become more and more open—e.g., addressing issues of persistence and distribution—dynamic sealing is being rediscovered. For example, Rossberg [28] proposes to use a form of dynamic sealing to allow type abstraction to coexist with dynamic typing; Leifer et al. [12] use hashes of implementations of abstract types to protect abstractions among different programs running on different sites; Dreyer et al. [7] use a variant of sealing (somewhere between static and dynamic) to give a type-theoretic account of ML-like modules and functors; finally, we [23] have proposed a translation (conjectured to be fully abstract) of System-F-style type abstraction into dynamic sealing.

∗Extended abstract appeared in Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161–172, 2004.

†Research conducted when the first author was a research associate in the University of Pennsylvania.

Another reason for the renewal of interest in sealing is that it happens to coincide with perfect encryption (under shared-key cryptography), that is, with an ideal encryption scheme where a ciphertext can be decrypted only if the key under which it was encrypted is known explicitly. Perfect encryption is a common abstraction in current research on both systems security and programming languages, for example in modeling and reasoning about cryptographic protocols (e.g., the spi-calculus [3]).

1.2 Problem

Although interest in dynamic sealing is reviving, there remains a significant obstacle to its extensive study: the lack of sufficiently powerful methods for reasoning about sealing. First, to the best of our knowledge, there has been no work at all on proof techniques for sealing in untyped sequential languages. There are several versions of bisimulation for the spi-calculus, but encoding other languages such as λ-calculus into spi-calculus raises the question of what abstraction properties are preserved by the encoding itself. Indeed, standard encodings of λ-calculus into π-calculus [16] are not fully abstract, i.e., do not preserve equivalence. Second, even in statically typed settings, the published techniques for obtaining abstraction properties are in general very weak. For instance, the first two [12, 28] of the works cited above use (variants of) the colored brackets of Zdancewic et al. [8] but only prove (or even state) abstraction properties for cases where abstract data is published by itself with no interface functions provided (i.e., once sealed, data is never unsealed).

1.3 Abstraction as equivalence

We aim to establish a method for proving abstraction of programs using dynamic sealing in an untyped setting. To this end, let us first consider how to state the property of abstraction in the first place. Take, for example, the following module implementing complex numbers in an imaginary ML-like language.

     module PolarComplex =
       abstype t = real * real
       let from_re_and_im : real * real -> t =
         fun (x, y) ->
           (sqrt(x * x + y * y), atan2(y, x))
       let to_re_and_im : t -> real * real =
         fun (r, t) ->
           (r * cos(t), r * sin(t))
       let multiply : t * t -> t =
         fun ((r1, t1), (r2, t2)) ->
           (r1 * r2, t1 + t2)
     end

Using dynamic sealing instead of type abstraction, this module can be written as follows for some secret seal k.

module PolarComplex =
let from_re_and_im =
fun (x, y) ->
let z = (sqrt(x * x + y * y), atan2(y, x)) in
<seal z under k>
let to_re_and_im =
fun z ->
let (r, t) = <unseal z under k> in
(r * cos(t), r * sin(t))
let multiply =
fun (z1, z2) ->
let (r1, t1) = <unseal z1 under k> in
let (r2, t2) = <unseal z2 under k> in
let z = (r1 * r2, t1 + t2) in
<seal z under k>
end

Now, the question is: Is this use of sealing correct? That is, does it really protect data abstraction? In particular, can we show that this module has the same external behavior as another sealed module that also implements complex numbers, e.g., the following module with another secret seal

k'?
module CartesianComplex =
let from_re_and_im =
fun (x, y) ->
<check that x and y are real numbers>;
let z = (x, y) in <seal z under k'>
let to_re_and_im =
fun z ->
let (x, y) = <unseal z under k'> in (x, y)
let multiply =
fun (z1, z2) ->
let (x1, y1) = <unseal z1 under k'> in
let (x2, y2) = <unseal z2 under k'> in
let z = (x1 * x2 - y1 * y2,
         x1 * y2 + x2 * y2) in
<seal z under k'>
end

Formally, we want to show the contextual equivalence [19] of the two modules PolarComplex and CartesianComplex. In general, however, it is difficult to directly prove contextual equivalence because it demands that we consider an infinite number of contexts.

1.4 Equivalence by bisimulation

To overcome this difficulty, we define a notion of bisimulation for our language (by extending applicative bisimulation [4]) and use it as a tool for proving contextual equivalence. Essentially, a bisimulation records a set of pairs of “corresponding values” of two different programs. In the example of PolarComplex and CartesianComplex, the bisimulation is (roughly):

            {(PolarComplex, CartesianComplex)}

         ∪ {(PolarComplex.from_re_and_im, CartesianComplex.from_re_and_im),

             (PolarComplex.to_re_and_im, CartesianComplex.to_re_and_im),
             (PolarComplex.multiply, CartesianComplex.multiply)}

∪ {((x, y), (x, y)) | x, y real numbers}
∪ {({(r, θ)}_{k}, {(r cos θ, r sin θ)}_{k′}) | r ≥ 0}

The first part is the modules themselves. The second part is the individual elements of the modules. The third is arguments of from_re_and_im as well as results of to_re_and_im. The last is the representations of complex numbers sealed under k or k′, where { } denotes sealing.

From the soundness of bisimulation, we obtain the contextual equivalence of the two modules. Furthermore, our bisimulation is complete: if two programs are contextually equivalent, then there always exists a bisimulation between them. This means that (at least in theory) we can use bisimulation to prove any valid contextual equivalence.

1.5 Contribution

The main contribution of this work is a sound and complete bisimulation proof method for contextual equivalence in an untyped functional language with dynamic sealing. Along the way, we are led to refine the usual contextual equivalence to account for the variations in observing power induced by the context’s knowledge (or ignorance) of the seals used in observed terms.

Parts of our theory are analogous to bisimulation techniques developed for the spi-calculus [1, 2, 5, 6]. However, our bisimulation is technically simpler and thus more suitable for reasoning about dynamic sealing for data abstraction in sequential languages. Furthermore, our setting requires us to extend even the definition of contextual equivalence in a natural but significant way, as discussed in Section 3.

1.6 Structure of the paper

The rest of this paper is structured as follows. Section 2 formalizes the syntax and the semantics of our language, λ_{seal}. Section 3 defines a suitable notion of contextual equivalence. Section 4 presents our bisimulation and gives several examples, including the complex number packages discussed above and an encoding of the Needham-Schroeder-Lowe key exchange protocol. Section 5 proves soundness and completeness of the bisimulation with respect to contextual equivalence. Section 7 discusses related work, and Section 8 sketches future work.

1.7 Notation

Throughout the paper, we use overbars as shorthands for sequences—e.g., we write \overline{x} and (\overline{v}, \overline{v}′) instead of x_{1}, …, x_{n} and (v_{1}, v′_{1}), …, (v_{n}, v′_{n}) where n ≥ 0. Thus, \overline{k} ∈ s stands for k_{1}, …, k_{n} ∈ s and (\overline{v}, \overline{v}′) ∈ R for (v_{1}, v′_{1}), …, (v_{n}, v′_{n}) ∈ R. Similarly, \{\overline{k}\} is a shorthand for the set \{k_{1}, …, k_{n}\} where k_{i} ≠ k_{j} for any i ≠ j. When s and t are sets, s ⊎ t is defined to be s ∪ t if s ∩ t = ∅, and undefined otherwise.

d, e ::=  term
x  variable
λx. e  function
e_{1} e_{2}  application
c  constant
op(e_{1}, …, e_{n})  primitive
if e_{1} then e_{2} else e_{3}  conditional branch
⟨e_{1}, …, e_{n}⟩  tupling
#_{i}(e)  projection
k  seal
νx. e  fresh seal generation
{e_{1}}_{e_{2}}  sealing
let {x}_{e_{1}} = e_{2} in e_{3} else e_{4} unsealing
u, v, w ::=  value
λx. e  function
c  constant
⟨v_{1}, …, v_{n}⟩  tuple
k  seal
{v}_{k}  sealed value

Figure 1: Syntax of λ_{seal}

2 Syntax and Semantics

λ_{seal} is the standard untyped, call-by-value λ-calculus extended with sealing. Its syntax is given in Figure 1. Seal k is an element of the countably infinite set K of all seals. We use meta-variables s and t for finite subsets of K. Fresh seal generation νx. e generates a fresh seal k, binds it to x and evaluates e. The meaning of freshness will soon be clarified below. Sealing {e_{1}}_{e_{2}} evaluates e_{1} to value v and e_{2} to seal k, and seals v under k. Unsealing let {x}_{e_{1}} = e_{2} in e_{3} else e_{4} evaluates e_{1} to seal k_{1} and e_{2} to sealed value {v}_{k_{2}}. If k_{1} = k_{2}, the unsealing succeeds and e_{3} is evaluated with x bound to v. Otherwise, the unsealing fails and e_{4} is evaluated.

The calculus is also parametrized by first-order constants and primitives (involving no seals) such as real numbers and their arithmetics. We use infix notations for binary primitives like e_{1} +e_{2}. We assume that constants include booleans true and false. We also assume that op includes the equality = for constants. Note that we do not have equality for sealed values yet (cf. Section 6), though equality for seals is easy to implement as in let {x}_{k_{1}} = {c}_{k_{2}} in true else false.

We adopt the standard notion of variable binding and write FV (e) for the set of free variables in e. We also write Seals(e) for the set of seals that appear in term e.

We write let x = e_{1} in e_{2} for (λx. e_{2})e_{1}. We also write ⊥ for (λx. xx)(λx. xx) and λ{x}_{k}. e for λy. let {x}_{k} = y in e else ⊥ where y ∉ FV (e). Furthermore, we write λ⟨x, y⟩. e for λz. let x = #_{1}(z) in let y = #_{2}(z) in e where z ∉ FV (e). We use similar notations of pattern matching throughout the paper.

The semantics of λ_{seal} is given in Figure 2 by big-step evaluation (s) e ⇓ (t) v annotated with the set s of seals before the evaluation and the set t of seals after the evaluation. It is parametrized by the meaning [[op(c_{1}, …, c_{n})]] of primitives. For example, [[1.23 + 4.56]] = 5.79. For simplicity, we

\frac{Seals(e) ⊆ s}{(s) λx. e ⇓ (s) λx. e} (E-Lam)
\frac{(s) e_{1} ⇓ (s_{1}) λx. e (s_{1}) e_{2} ⇓ (s_{2}) v (s_{2}) [v/x]e ⇓ (t) w}{(s) e_{1} e_{2} ⇓ (t) w} (E-App)
\overline{(s) c ⇓ (s) c} (E-Const)
\frac{(s) e_{1} ⇓ (s_{1}) c_{1} … (s_{n−1}) e_{n} ⇓ (s_{n}) c_{n} [[op(c_{1}, …, c_{n})]] = c}{(s) op(e_{1}, …, e_{n}) ⇓ (s_{n}) c} (E-Prim)
\frac{(s) e_{1} ⇓ (s_{1}) true (s_{1}) e_{2} ⇓ (t) v}{(s) if e_{1} then e_{2} else e_{3} ⇓ (t) v} (E-Cond-True)
\frac{(s) e_{1} ⇓ (s_{1}) false (s_{1}) e_{3} ⇓ (t) v}{(s) if e_{1} then e_{2} else e_{3} ⇓ (t) v} (E-Cond-False)
\frac{(s) e_{1} ⇓ (s_{1}) v_{1} … (s_{n−1}) e_{n} ⇓ (s_{n}) v_{n}}{(s) ⟨e_{1}, …, e_{n}⟩ ⇓ (s_{n}) ⟨v_{1}, …, v_{n}⟩} (E-Tuple)
\frac{(s) e ⇓ (t) ⟨v_{1}, …, v_{n}⟩ 1 ≤ i ≤ n}{(s) #_{i}(e) ⇓ (t) v_{i}} (E-Proj)
\frac{k ∈ s}{(s) k ⇓ (s) k} (E-Seal)  \frac{(s ⊎ \{k\}) [k/x]e ⇓ (t) v}{(s) νx. e ⇓ (t) v} (E-New)
\frac{(s) e_{1} ⇓ (s_{1}) v (s_{1}) e_{2} ⇓ (s_{2}) k}{(s) \{e_{1}\}_{e_{2}} ⇓ (s_{2}) \{v\}_{k}} (E-Do-Seal)
\frac{(s) e_{1} ⇓ (s_{1}) k (s_{1}) e_{2} ⇓ (s_{2}) \{v\}_{k} (s_{2}) [v/x]e_{3} ⇓ (t) w}{(s) let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ (t) w} (E-Unseal-Succ)
\frac{(s) e_{1} ⇓ (s_{1}) k_{1} (s_{1}) e_{2} ⇓ (s_{2}) \{v\}_{k_{2}} k_{1} ≠ k_{2} (s_{2}) e_{4} ⇓ (t) w}{(s) let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ (t) w} (E-Unseal-Fail)

Figure 2: Semantics of λ_{seal} adopt the left-to-right evaluation order. As usual, substitutions [e/x] avoid capturing free variables by implicit α-conversion. The meaning of freshness is formalized by requiring k ∉ s in (E-New). We write (s) e ⇓ if (s) e ⇓ (t) v for some t and v.

Because of fresh seal generation, our evaluation is not quite deterministic. For instance, we have both (∅) νx. x ⇓ ({k_{1}}) k_{1} and (∅) νx. x ⇓ ({k_{2}}) k_{2} for k_{1} ≠ k_{2}. Nevertheless, we have the following property:

Property 2.1. Evaluation is deterministic modulo the names of freshly generated seals. That is, for any (s) e ⇓ (t) v and (s) e ⇓ (t′) v′ with Seals(e) ⊆ s, we have v = [\overline{k}/\overline{x}]e_{0} and v′ = [\overline{k}′/\overline{x}]e_{0} for some e_{0} with Seals(e_{0}) ⊆ s, some \overline{k} with \{\overline{k}\} ⊆ t \ s, and some \overline{k}′ with \{\overline{k}′\} ⊆ t′ \ s.

Proof. Straightforward induction on the derivation of (s) e ⇓ (t) v. □

In what follows, we implicitly use the following properties of evaluation without explicitly referring to them.

Property 2.2. Every value evaluates only to itself. That is, for any s and v with s ⊇ Seals(v), we have (s) v ⇓ (s) v. Furthermore, if (s) v ⇓ (t) w, then t = s and w = v.

Proof. Straightforward induction on the syntax of values. □

Property 2.3. Evaluation never decreases the seal set. That is, for any (s) e ⇓ (t) v, we have s ⊆ t.

Proof. Straightforward induction on the derivation of (s) e ⇓ (t) v. □

3 Generalized Contextual Equivalence

In standard untyped λ-calculus, contextual equivalence for closed values^{1} can be defined by saying that v and v′ are contextually equivalent if [v/x]e ⇓ ⟺ [v′/x]e ⇓ for any term e. In λ_{seal}, however, contextual equivalence cannot be defined for two values in isolation. For instance, consider λ{x}_{k}. x + 1 and λ{x}_{k′}. x + 2. Whether these values are equivalent or not depends on what values sealed under k or k′ are known to the context. If the original terms which created k and k′ were νz. ⟨{2}_{z}, λ{x}_{z}. x + 1⟩ and νz. ⟨{1}_{z}, λ{x}_{z}. x + 2⟩, for example, then the only values sealed under k or k′ are 2 and 1, respectively. Thus, the equivalence above does hold. On the other hand, it does not hold if the terms were, say, νz. ⟨{3}_{z}, λ{x}_{z}. x + 1⟩ and νz. ⟨{4}_{z}, λ{x}_{z}. x + 2⟩. This observation that we have to consider multiple pairs of values at once leads to the following definition of contextual equivalence.

Definition 3.1. A value relation R is a set of pairs of values.

Definition 3.2. The contextual equivalence ≡ is the set of all triples (s, s′, R) such that for any (\overline{v}, \overline{v}′) ∈ R, we have the following properties.

1For the sake of simplicity, we focus on equivalence of closed values (as opposed to open expressions) in this paper.

For open expressions e and e′ with free variables x_{1}, …, x_{n}, it suffices to consider the equivalence of λx_{1}…. λx_{n}. e and λx_{1}…. λx_{n}. e′ instead. See also our recent work [33, Section 6] for more formal discussion on this issue.

1. Seals(\overline{v}) ⊆ s and Seals(\overline{v}′) ⊆ s′.

2. (s) [\overline{v}/\overline{x}]e ⇓ ⟺ (s′) [\overline{v}′/\overline{x}]e ⇓ for any e with Seals(e) = ∅.

The intuition is that \overline{v} and \overline{v}′ are indistinguishable for any observer within the language (unless it somehow knows any of the seals in s or s′ a priori). We write (s) v_{1}, …, v_{n} ≡ (s′) v′_{1}, …, v′_{n} for (s, s′, {(v_{1}, v′_{1}), …, (v_{n}, v′_{n})}) ∈ ≡. In order to lighten the notation, we do not enclose these v_{1}, …, v_{n} and v′_{1}, …, v′_{n} in parentheses. We also write (s) v ≡_{R} (s′) v′ when (v, v′) ∈ R and (s, s′, R) ∈ ≡. Intuitively, it can be read as “value v with seal set s and value v′ with seal set s′ are contextually equivalent under contexts’ knowledge R.”

Note that no generality is lost by requiring Seals(e) = ∅ in the definition above: if e needs its own seals, it can freshly generate an arbitrary number of them by using ν; if e knows some \overline{k} ∈ s in the left-hand side and corresponding \overline{k}′ ∈ s′ in the right-hand side of contextual equivalence, it suffices to require (\overline{k}, \overline{k}′) ∈ R so that these seals can be substituted for some free \overline{x} in e by Condition (2) above. Thus, our contextual equivalence subsumes standard contextual equivalence where a context knows none, all, or part of the seals (or, more generally, values involving the seals). Conversely, the standard contextual equivalence (for closed values) is implied by the generalized one in the following sense: if (v, v′) ∈ R for some (s, s′, R) ∈ ≡, then it is immediate by definition that K[v] ⇓ ⟺ K[v′] ⇓ for any context K with a hole [ ].

Example 3.3. Let s = {k} and s′ = {k′}. We have (s) {2}_{k} ≡ (s′) {1}_{k′} since the context has no means to unseal the values sealed under k or k′. (A formal proof of this claim based on bisimulation will be given later in Example 4.2 with Corollary 5.7.) We also have (s) λ{x}_{k}. x + 1 ≡ (s′) λ{x}_{k′}. x + 2 since the context cannot make up any values sealed under k or k′.

Furthermore, we have

(s) {2}_{k}, λ{x}_{k}. x + 1 ≡ (s′) {1}_{k′}, λ{x}_{k′}. x + 2

because applications of the functions to the sealed values yield the same integer 3. Similarly,

(s) {4}_{k}, λ{x}_{k}. x + 1 ≡ (s′) {5}_{k′}, λ{x}_{k′}. x

holds. However,

\begin{aligned}& (s) \{2\}_{k}, λ\{x\}_{k}. x + 1, \{4\}_{k}, λ\{x\}_{k}. x + 1 \\ ≡ & (s′) \{1\}_{k′}, λ\{x\}_{k′}. x + 2, \{5\}_{k′}, λ\{x\}_{k′}. x \end{aligned}

does not hold, because applications of the last functions to the first sealed values yield different integers 3 and 1.

As the last example shows, even if (s, s′, R_{1}) ∈ ≡ and (s, s′, R_{2}) ∈ ≡, we do not always have (s, s′, R_{1} ∪ R_{2}) ∈ ≡. Intuitively, this means that we should not confuse two worlds where the uses of seals are different. This is the reason why we defined ≡ as a set of triples (s, s′, R) rather than just a function that takes a pair (s, s′) of seal sets and returns the set R of all pairs of equivalent values.

Conversely, again as the examples above suggest, there are cases where (s, s′, R_{1}) ∈ ≡ and (s, s′, R_{2}) ∈ ≡ for R_{1} ⊆ R_{2}. This implies that there is a partial order among the value relations R in contextual equivalence. We could alternatively define contextual equivalence only with such value relations that are maximal in this ordering, but this would just complicate the technicalities that follow.

We will use the following lemmas about contextual equivalence in what follows.

Lemma 3.4. Application, projection, fresh seal generation, and unsealing preserve contextual equivalence. That is:

1. For any (u, u′) ∈ R and (v, v′) ∈ R with (s, s′, R) ∈ ≡, if (s) uv ⇓ (t) w and (s) u′v′ ⇓ (t′) w′, then (t, t′, R ∪ {(w, w′)}) ∈ ≡.

2. For any (⟨v_{1}, …, v_{n}⟩, ⟨v′_{1}, …, v′_{n}⟩) ∈ R with (s, s′, R) ∈ ≡, we have (s, s′, R ∪ {(v_{i}, v′_{i})}) ∈ ≡ for any 1 ≤ i ≤ n.

3. For any (s, s′, R) ∈ ≡, we have (s ⊎ {k}, s′ ⊎ {k′}, R ⊎ {(k, k′)}) ∈ ≡ for any k ∉ s and k′ ∉ s′.

4. For any ({v}_{k}, {v′}_{k′}) ∈ R and (k, k′) ∈ R with (s, s′, R) ∈ ≡, we have (s, s′, R∪{(v, v′)}) ∈ ≡.

Proof. To prove the case of application, let us assume (u, u′) ∈ R and (v, v′) ∈ R with (s, s′, R) ∈ ≡ as well as (s) uv ⇓ (t) w and (s) u′v′ ⇓ (t′) w′, and prove (t, t′, R∪{(w, w′)}) ∈ ≡. The first condition of contextual equivalence in Definition 3.2 follows immediately from (part of) Property 2.1. To show the second, take any (\overline{w}, \overline{w}′) ∈ R ∪ \{(w, w′)\}, take any e with Seals(e) = ∅, and prove (t) [\overline{w}/\overline{x}]e ⇓ ⟺ (t′) [\overline{w}′/\overline{x}]e ⇓. Without loss of generality, let u_{1} = u and u′_{1} = u′. Then, from the second condition in the definition of (s, s′, R) ∈ ≡, we have

(s) [u, v, w_{2}, …, w_{n}/y, z, x_{2}, …, x_{n}](let x_{1} = yz in e) ⇓
⟺ (s′) [u′, v′, w′_{2}, …, w′_{n}/y, z, x_{2}, …, x_{n}](let x_{1} = yz in e) ⇓

from which the conclusion follows with the assumptions (s) uv ⇓ (t) w and (s) u′v′ ⇓ (t′) w′.

The other cases follow similarly by taking let x_{1} = #_{i}(y) in e or νx_{1}. e or let {x_{1}}_{y} = z in e, respectively, instead of let x_{1} = yz in e above. □

Lemma 3.5. Contextually equivalent values put in the same value context yield contextually equivalent values. That is, for any (s, s′, R) ∈ ≡ and (\overline{v}, \overline{v}′) ∈ R, and for any w = [\overline{v}/\overline{x}]e_{0} and w′ = [\overline{v}′/\overline{x}]e_{0} with Seals(e_{0}) = ∅, we have (s, s′, R ∪ \{(w, w′)\}) ∈ ≡.

Proof. Immediate from the definition of contextual equivalence, using the property of substitution that [[\overline{v}/\overline{x}]e_{0}/x]e = [\overline{v}/\overline{x}]([e_{0}/x]e) when \{\overline{x}\} ∩ FV (e) = ∅. □

Lemma 3.6. Any subset of contextually equivalent values are contextually equivalent. That is, for any (s, s′, R) ∈ ≡, we have (s, s′, S) ∈ ≡ for any S ⊆ R.

Proof. Immediate from the definition of contextual equivalence. □

4 Bisimulation

Giving a direct proof of contextual equivalence is generally difficult, because the definition involves universal quantification over an infinite number of contexts. Thus, we want a more convenient tool for proving contextual equivalence. For this purpose, we define the notion of bisimulation as follows.

Definition 4.1. A bisimulation is a set X of triples (s, s′, R) such that:

1. For each (v, v′) ∈ R, we have Seals(v) ⊆ s and Seals(v′) ⊆ s′.

2. For each (v, v′) ∈ R, v and v′ are of the same kind. That is, both are functions, both are constants, both are tuples, both are seals, or both are sealed values.

3. For each (c, c′) ∈ R, we have c = c′.

4. For each (⟨v_{1}, …, v_{n}⟩, ⟨v′_{1}, …, v′_{n′}⟩) ∈ R, we have n = n′ and (s, s′, R ∪ {(v_{i}, v′_{i})}) ∈ X for every 1 ≤ i ≤ n.

5. For each (k_{1}, k′_{1}) ∈ R and (k_{2}, k′_{2}) ∈ R, we have k_{1} = k_{2} ⟺ k′_{1} = k′_{2}.

6. For each ({v}_{k}, {v′}_{k′}) ∈ R, we have either (k, k′) ∈ R and (s, s′, R ∪ {(v, v′)}) ∈ X, or else k ∉ fst(R) and k′ ∉ snd(R). Here, fst(R) is the set of the first elements of all pairs in R and snd(R) the second.

7. Take any (λx. e, λx. e′) ∈ R. Take also any \overline{k} and \overline{k}′ with s ∩ \{\overline{k}\} = s′ ∩ \{\overline{k}′\} = ∅. Moreover, let v = [\overline{u}/\overline{x}]d and v′ = [\overline{u}′/\overline{x}]d for any (\overline{u}, \overline{u}′) ∈ R ⊎ \{(\overline{k}, \overline{k}′)\} and Seals(d) = ∅. Then, we have (s ⊎ \{\overline{k}\}) (λx. e)v ⇓ ⟺ (s′ ⊎ \{\overline{k}′\}) (λx. e′)v′ ⇓. Furthermore, if (s ⊎ \{\overline{k}\}) (λx. e)v ⇓ (t) w and (s′ ⊎ \{\overline{k}′\}) (λx. e′)v′ ⇓ (t′) w′, then (t, t′, R ⊎ \{(\overline{k}, \overline{k}′)\} ∪ \{(w, w′)\}) ∈ X.

For any bisimulation X, we write (s) v X_{R} (s′) v′ when (v, v′) ∈ R and (s, s′, R) ∈ X. This can be read “values v and v′ with seal sets s and s′ are bisimilar under contexts’ knowledge R.”

The intuitions behind the definition of bisimulation are as follows. Each of the conditions excludes pairs of values that are distinguishable by a context (except for Condition 1, which just restricts the scoping of seals). Condition 2 excludes pairs of values of different kinds, e.g., 123 and λx. x. Condition 3 excludes pairs of different constants. Condition 4 excludes pairs of tuples with distinguishable elements. Condition 5 excludes cases such as (k, k′) ∈ R and (k, k′′) ∈ R with k′ ≠ k′′, for which contexts like let {x}_{y} = {()}_{z} in x else ⊥ can distinguish the left-hand side (setting y = z = k) and the right-hand side (setting y = k′ and z = k′′). Condition 6 excludes cases where (i) the context can unseal both of two sealed values whose contents are distinguishable, or (ii) the context can unseal only one of the two sealed values.

Condition 7, the most interesting one, is about what a context can do to distinguish two functions. Obviously, this will involve applying them to some arguments—but what arguments? Certainly not arbitrary terms, because in general a context has only a partial knowledge of (values involving) the seals in s and s′. All that a context can do for making up the arguments is to carry out some computation d using values \overline{u} and \overline{u}′ from its knowledge. Therefore, the arguments have forms [\overline{u}/\overline{x}]d and [\overline{u}′/\overline{x}]d.

An important and perhaps surprising point here is that it actually suffices to consider cases where these arguments are values. This restriction is useful and even crucial for proving bisimulation of functions: if the arguments [\overline{u}/\overline{x}]d and [\overline{u}′/\overline{x}]d were not values, we should evaluate them before applying the functions; in particular, if evaluation of one argument converges, then evaluation of the other argument must converge as well; proving this property amounts to proving the contextual equivalence of \overline{u} and \overline{u}′, which was the whole purpose of our bisimulation!

Fortunately, our restriction of the arguments to values can be justified by the “fundamental property” proved in the next section, which says that the special forms [\overline{u}/\overline{x}]d and [\overline{u}′/\overline{x}]d are preserved by evaluation. The only change required as a result of this restriction is the addition of \{(\overline{k}, \overline{k}′)\} to knowledge R in Condition 7: it compensates for the fact that d can no longer be a fresh seal generation, while the context can still generate its own fresh seals \overline{k} and \overline{k}′ when making up the arguments. Without such a change, our bisimulation would indeed be unsound: a counterexample would be (∅, ∅, {(λx. {true}_{x}, λx. {false}_{x})}), which would satisfy all the conditions of bisimulation (including Condition 7, in particular, because the arguments v and v′ could not contain any seal), while contexts like νy. let {z}_{y} = [ ] y in if z then () else ⊥ can distinguish the two functions.

The rest of Condition 7 is straightforward: the results w and w′ of function application should also be bisimilar.

Example 4.2. Let s = {k}, s′ = {k′}, and R = {({2}_{k}, {1}_{k′})}. Then {(s, s′, R)} is a bisimulation, as can be seen by a straightforward check of the conditions above.

Example 4.3. Let s = {k_{1}, k_{2}}, s′ = {k′}, and

R = {(⟨{2}_{k_{1}}, {4}_{k_{2}}⟩,
⟨{1}_{k′}, {5}_{k′}⟩),
({2}_{k_{1}}, {1}_{k′}),
({4}_{k_{2}}, {5}_{k′})}.

Then {(s, s′, R)} is a bisimulation. This example illustrates the fact that the number of seals may differ in the left-hand side and in the right-hand side of bisimulation. Note that the closure condition (Condition 4) in the definition of bisimulation demands that we include not only the original pairs, but also their corresponding components.

Example 4.4. Suppose we want to show that the pair ⟨{2}_{k}, λ{x}_{k}. x+1⟩ is bisimilar to ⟨{1}_{k′}, λ{x}_{k′}. x+2)⟩, assuming that seals k and k′ are not known to the context. Again, the closure conditions in the definition force us to include the corresponding components of the pairs (Condition 4), as well as the results of evaluating the second components applied to the first components (Condition 7); moreover, since Condition 7 allows the context to enrich the set of seals with arbitrary seals of its own, our bisimulation will consist of an infinite collection of similar sets, differing in the context’s choice of seals.

Formally, let G be the following function on sets of pairs of seals:

G\{(\overline{k}_{0}, \overline{k}′_{0})\} = \{(⟨\{2\}_{k}, λ\{x\}_{k}. x + 1⟩,
⟨{1}_{k′}, λ{x}_{k′}. x + 2⟩),
({2}_{k}, {1}_{k′}),
(λ{x}_{k}. x + 1, λ{x}_{k′}. x + 2),
(3, 3)}
∪ \{(\overline{k}_{0}, \overline{k}′_{0})\}

Then

X = \{(\{k, \overline{k}_{0}\}, \{k′, \overline{k}′_{0}\}, G\{(\overline{k}_{0}, \overline{k}′_{0})\}) | k ∉ \{\overline{k}_{0}\} ∧ k′ ∉ \{\overline{k}′_{0}\}\}

is a bisimulation. The only non-trivial work required to show this is checking Condition 7 for the pair (λ\{x\}_{k}. x + 1, λ\{x\}_{k′}. x + 2) ∈ G\{(\overline{k}_{0}, \overline{k}′_{0})\}, for each \overline{k}_{0} and \overline{k}′_{0} with k ∉ \{\overline{k}_{0}\} and k′ ∉ \{\overline{k}′_{0}\}.

Consider any v = [\overline{u}/\overline{x}]d and v′ = [\overline{u}′/\overline{x}]d with (\overline{u}, \overline{u}′) ∈ G\{(\overline{k}_{0}, \overline{k}′_{0})\} ⊎ \{(\overline{k}_{1}, \overline{k}′_{1})\} and Seals(d) = \{k, \overline{k}_{0}\} ∩ \{\overline{k}_{1}\} = \{k′, \overline{k}′_{0}\} ∩ \{\overline{k}′_{1}\} = ∅. If the evaluations of (λ\{x\}_{k}. x + 1)v and (λ\{x\}_{k′}. x + 2)v′ diverge, then the condition holds.

Let us focus on cases where the evaluation of (λ{x}_{k}. x+1)v converges (without loss of generality, thanks to symmetry), that is, where v is of the form {w}_{k}. Then, either d is of the form {d_{0}}_{x_{i}} and u_{i} = k, or else d is a variable x_{i} and u_{i} = {w}_{k}. However, the former case is impossible: k is not in the first projection of G\{(\overline{k}_{0}, \overline{k}′_{0})\} or \{(\overline{k}_{1}, \overline{k}′_{1})\} by their definitions. So we must be in the latter case.

Since the only element of the form \{w\}_{k} in the first projection of G\{(\overline{k}_{0}, \overline{k}′_{0})\}⊎\{(\overline{k}_{1}, \overline{k}′_{1})\} is \{2\}_{k} where the corresponding element in its second projection is {1}_{k′}, we have v = {2}_{k} and v′ = {1}_{k′}. Then, the only evaluations of (λ{x}_{k}. x + 1)v and (λ{x}_{k′}. x + 2)v′ are

(\{k, \overline{k}_{0}\} ⊎ \{\overline{k}_{1}\}) (λ\{x\}_{k}. x + 1)v ⇓ (\{k, \overline{k}_{0}, \overline{k}_{1}\}) 3

and

(\{k′, \overline{k}′_{0}\} ⊎ \{\overline{k}′_{1}\}) (λ\{x\}_{k′}. x + 2)v′ ⇓ (\{k′, \overline{k}′_{0}, \overline{k}′_{1}\}) 3.

Thus, the condition follows from

G\{(\overline{k}_{0}, \overline{k}′_{0})\} ⊎ \{(\overline{k}_{1}, \overline{k}′_{1})\} ∪ \{(3, 3)\} = G\{(\overline{k}_{0}, \overline{k}′_{0}), (\overline{k}_{1}, \overline{k}′_{1})\}

and

(\{k, \overline{k}_{0}, \overline{k}_{1}\}, \{k′, \overline{k}′_{0}, \overline{k}′_{1}\}, G\{(\overline{k}_{0}, \overline{k}′_{0}), (\overline{k}_{1}, \overline{k}′_{1})\}) ∈ X.

Example 4.5 (Complex Numbers). Now let us show a bisimulation relating the two implementations of complex numbers in Section 1.3. First, let

v = ⟨λ⟨x, y⟩. {⟨x + 0.0, y + 0.0⟩}_{k},
λ{⟨x, y⟩}_{k}. ⟨x, y⟩,
λ⟨{⟨x_{1}, y_{1}⟩}_{k}, {⟨x_{2}, y_{2}⟩}_{k}⟩.
{⟨x_{1} × x_{2} − y_{1} × y_{2}, x_{1} × y_{2} + y_{1} × x_{2}⟩}_{k}⟩
v′ = ⟨λ⟨x, y⟩. {⟨sqrt⟨x × x + y × y⟩, atan2⟨y, x⟩⟩}_{k′},
λ{⟨r, θ⟩}_{k′}. ⟨r × cos θ, r × sin θ⟩,
λ⟨{⟨r_{1}, θ_{1}⟩}_{k′}, {⟨r_{2}, θ_{2}⟩}_{k′}⟩. {⟨r_{1} × r_{2}, θ_{1} + θ_{2}⟩}_{k′}⟩.

The first component of each triple corresponds to the from_re_and_im functions in 1.3. The implementation in v just seals the x and y coordinates provided as arguments, after checking that they are indeed real numbers by attempting to add them to 0.0. The implementation in v′ performs an appropriate change of representation before sealing. The second components correspond to the to_re_and_im functions in 1.3, and the third components to the multiply functions.

The construction of the bisimulation follows the same pattern as Example 4.4, except that the operator G is more interesting:

G\{(\overline{k}_{0}, \overline{k}′_{0})\} =
{(v, v′)}
∪ {(λ⟨x, y⟩. {⟨x + 0.0, y + 0.0⟩}_{k},
λ⟨x, y⟩. {⟨sqrt(x × x + y × y), atan2(y, x)⟩}_{k′}),
(λ{⟨x, y⟩}_{k}. ⟨x, y⟩,
λ{⟨r, θ⟩}_{k′}. ⟨r × cos θ, r × sin θ⟩),
(λ⟨{⟨x_{1}, y_{1}⟩}_{k}, {⟨x_{2}, y_{2}⟩}_{k}⟩.
{⟨x_{1} × x_{2} − y_{1} × y_{2}, x_{1} × y_{2} + y_{1} × x_{2}⟩}_{k},
λ⟨{⟨r_{1}, θ_{1}⟩}_{k′}, {⟨r_{2}, θ_{2}⟩}_{k′}⟩. {⟨r_{1} × r_{2}, θ_{1} + θ_{2}⟩}_{k′})}
∪ {(⟨x, y⟩, ⟨x, y⟩) | x and y are arbitrary real numbers}
∪ {({⟨r cos θ, r sin θ⟩}_{k}, {⟨r, θ⟩}_{k′}) | r ≥ 0}
∪ \{(\overline{k}_{0}, \overline{k}′_{0})\}

Example 4.6 (Generative vs. Non-Generative Functors). In this example, we use bisimulation to show the equivalence of two instantiations of a generative functor, where generativity is modeled by fresh seal generation and the equivalence really depends on the generativity.

A functor is a parameterized module—a function from modules to modules. For example, a module implementing sets by binary trees can be parameterized by the type of elements and their comparison function. In the same imaginary ML-like language as in Section 1.3, such a functor might be written as follows:

     functor Set(module Element : sig
                   type t
                   val less_than : t -> t -> bool
                 end) =
       type elt = Element.t
       abstype set = Element.t tree
       let empty : set = Leaf
       let rec add : elt -> set -> set =
         fun x ->
           fun Leaf -> Node(x, Leaf, Leaf)
             | Node(y, l, r) ->
                 if Element.less_than x y then
                   Node(y, add x l, r)
                 else if Element.less_than y x then
                   Node(y, l, add x r)
                 else Node(y, l, r)
       let rec is_elt_of : elt -> set -> bool =
         fun x ->
           fun Leaf -> false
             | Node(y, l, r) ->
                 if Element.less_than x y then
                   is_elt_of x l
                 else if Element.less_than y x then

                   is_elt_of x r
                 else true
     end

Now, consider the following three applications of this functor:

     module IntSet1 =
       Set(module Element =
         type t = int
         let less_than : t -> t -> bool =
           fun x -> fun y -> (x <_{int} y)
       end)
     module IntSet2 =
       Set(module Element =
         type t = int
         let less_than : t -> t -> bool =
           fun x -> fun y -> (x <_{int} y)
       end)
     module IntSet3 =
       Set(module Element =
         type t = int
         let less_than : t -> t -> bool =
           fun x -> fun y -> (x >_{int} y)
       end)

If the functor Set is non-generative,^{2} the abstract type IntSet3.set becomes compatible with IntSet1.set and IntSet2.set, even though the comparison function of IntSet3 is not compatible with that of IntSet1 or IntSet2. As a result, (part of) their abstraction as sets of integers is lost: for instance, IntSet2 and IntSet3 are distinguished by a context like

                  C[ ] = let s = [ ].add 7 ([ ].add 3 [ ].empty) in

                          IntSet1.is_elt_of 7 s

while they should be equivalent if considered just as two different implementations of integer sets.

This situation can be translated into λ_{seal} as follows. First, the non-generative functor can be implemented by the following function f, using a standard call-by-value fixed-point operator fix (which is definable since the language is untyped).

2We intentionally avoid calling it “applicative” since the original design [13] of applicative functors carefully prevents the problem which follows here.

              λlt.

⟨{nil}_{k}, fix(λadd. λ⟨x, {y}_{k}⟩.

if lt⟨x, x⟩ then ⊥ else (* check that x has type elt *)

                  if y = nil then {⟨x, nil, nil⟩}_{k} else

if lt⟨x, #_{1}(y)⟩ then {⟨#_{1}(y), add(x, #_{2}(y)), #_{3}(y)⟩}_{k} else if lt⟨#_{1}(y), x⟩ then {⟨#_{1}(y), #_{2}(y), add(x, #_{3}(y))⟩}_{k} else {y}_{k}),

fix(λis elt of. λ⟨x, {y}_{k}⟩.

                  if y = nil then false else
                  if lt⟨x, #_{1}(y)⟩ then is elt of⟨x, #_{2}(y)⟩ else
                  if lt⟨#_{1}(y), x⟩ then is elt of⟨x, #_{3}(y)⟩ else
                  true)⟩

Next, we translate the three applications of the functor into three applications of f to appropriate comparison functions:

({k}) f(λ⟨x, y⟩. x <_{int} y) ⇓ ({k}) v_{1}
({k}) f(λ⟨x, y⟩. x <_{int} y) ⇓ ({k}) v_{2}
({k}) f(λ⟨x, y⟩. x >_{int} y) ⇓ ({k}) v_{3}

The values v_{2} and v_{3} are not contextually equivalent when the context knows v_{1}. That is, ({k}, {k}, {(v_{1}, v_{1}), (v_{2}, v_{3})}) ∉ ≡. To see this, take e = #_{3}(x) ⟨7, #_{2}(y) ⟨7, #_{2}(y) ⟨3, #_{1}(y)⟩⟩⟩, setting x = v_{1}, y = v_{2} in the left hand side and x = v_{1}, y = v_{3} in the right hand side.

Note that v_{2} and v_{3} are contextually equivalent if the context knows neither v_{1}, f, nor any other values involving the seal k. That is, ({k}, {k}, {(v_{2}, v_{3})}) ∈ ≡. Indeed, the context C[ ] above uses IntSet1 to distinguish IntSet2 and IntSet3. Our definition of contextual equivalence as a set of relations (annotated with seal sets) gives a precise account for such subtle variations of contexts’ knowledge.

On the other hand, if we take the Set functor to be generative, then IntSet2 and IntSet3 are contextually equivalent even if the context also knows IntSet1, since all the abstract types are incompatible with one another. This case can be modeled in λ_{seal} by the following function g, which generates a fresh seal for each application instead of using the same seal k for all instantiations.

λlt. νz.
⟨{nil}_{z},
fix(λadd. λ⟨x, {y}_{z}⟩….),
fix(λis elt of. λ⟨x, {y}_{z}⟩….)⟩

Consider the following three applications of g.

(∅) g(λ⟨x, y⟩. x <_{int} y) ⇓ ({k_{1}}) w_{1}
({k_{1}}) g(λ⟨x, y⟩. x <_{int} y) ⇓ ({k_{1}, k_{2}}) w_{2}
({k_{1}}) g(λ⟨x, y⟩. x >_{int} y) ⇓ ({k_{1}, k_{3}}) w_{3}

Now w_{2} and w_{3} are bisimilar even if the context knows w_{1}. That is, there exists a bisimulation X such that ({k_{1}, k_{2}}, {k_{1}, k_{3}}, R) ∈ X with {(w_{1}, w_{1}), (w_{2}, w_{3})} ⊆ R. It is straightforward to construct this bisimulation in the same manner as Examples 4.4 and 4.5.

Example 4.7. Let us show that λx. ⟨3, x⟩ is bisimilar to itself. This example is technically trickier than previous ones, because arbitrary values provided by the context can appear verbatim within results. These results can again be passed as arguments and thus appear within yet larger results, etc. To achieve the required closure conditions, we need to reach a limit of this process. This can be accomplished by defining a bisimulation X inductively.

We require (∅, ∅, ∅) ∈ X as the (trivial) base case. The induction rule is as follows. Take any (s, s′, R) ∈ X. Take any \overline{w} = [\overline{v}/\overline{x}]\overline{e} and \overline{w}′ = [\overline{v}′/\overline{x}]\overline{e} with (\overline{v}, \overline{v}′) ∈ R and Seals(\overline{e}) = ∅. Take any t ⊇ s and t′ ⊇ s′ of the forms \{\overline{k}\} and \{\overline{k}′\}. Let

S = {(λx. ⟨3, x⟩, λx. ⟨3, x⟩),
(⟨3, \overline{w}⟩, ⟨3, \overline{w}′⟩),
(3, 3),
(\overline{w}, \overline{w}′),
(\overline{k}, \overline{k}′)\}.

We then require that (t, t′, T ) ∈ X for any T ⊆ S. The bisimulation we want is the least X satisfying these conditions.

Intuitively, we have defined X so that the conditions of bisimulation—Condition 7, in particular— are immediately satisfied. The final technical twist T ⊆ S is needed because the closure conditions in the definition of bisimulation add individual pairs of elements rather than adding their whole “deductive closures” at once.

Example 4.8 (Protocol Encoding). As a final illustration of the power of our bisimulation technique (and λ_{seal} itself), let us consider a more challenging example. This example is an encoding of the protocol below, which is based on the key exchange protocol of Needham, Schroeder, and Lowe [15, 22].

1. B → A : B
2. A → B : {N_{A}, A}_{k_{B}}
3. B → A : {N_{A}, N_{B}, B}_{k_{A}}
4. A → B : {N_{B}}_{k_{B}}
5. B → A : {i}_{N_{B}}

In this protocol, A is a server accepting requests from good B and evil E. It is supposed to work as follows. (1) B sends its own name B to A. (2) A generates a fresh nonce N_{A}, pair it with its own name A, encrypts the pair with B’s public key, and sends it to B. (3) B generates a fresh key N_{B}, tuples it with N_{A} and B, encrypts the tuple with A’s public key, and sends it to A. (4) A encrypts N_{B} with B’s public key and sends it to B. (5) B encrypts some secret integer i with N_{B} and sends it to A.

The idea of the encoding is as follows. We use sealing, unsealing and fresh seal generation as (perfect) encryption, decryption, and fresh key generation. The whole system is expressed as a tuple of (functions representing) keys known to the attacker and terms U and V representing principals B and A.

W = ⟨λx. {x}_{k_{A}}, λx. {x}_{k_{B}}, k_{E}, U, V ⟩

Each principal is encoded as a pair of the last value it sent (if any) and a continuation function waiting to receive a next message. When the message is received, the function returns the next state of the principal. Communication occurs by a context applying these functions in an appropriate

S = {(U, U′), (V, V′), (W, W′),

— corresponding keys and constants known to the attacker (\overline{k}, \overline{k}′), (A, A), (B, B), (E, E), (λx. {x}_{k_{A}}, λx. {x}_{k′_{A}}), (λx. {x}_{k_{B}}, λx. {x}_{k′_{B}}), (k_{E}, k′_{E}), (\overline{w}, \overline{w}′), (\{\overline{w}\}_{k_{A}}, \{\overline{w}′\}_{k′_{A}}), (\{\overline{w}\}_{k_{B}}, \{\overline{w}′\}_{k′_{B}}),

— corresponding components from principal B at Step 1 (λ{⟨x, y⟩}_{k_{B}}. assert(y = A); νz. ({⟨x, z, B⟩}_{k_{A}}, λ{z_{0}}_{k_{B}}. assert(z_{0} = z); {i}_{z}), λ{⟨x, y⟩}_{k′_{B}}. assert(y = A); νz. ({⟨x, z, B⟩}_{k′_{A}}, λ{z_{0}}_{k′_{B}}. assert(z_{0} = z); {j}_{z})),

— corresponding components from principal A at Step 2, communicating with B (⟨\{⟨\overline{k}_{AB}, A⟩\}_{k_{B}}, λ\{⟨y_{0}, z, x_{0}⟩\}_{k_{A}}. assert(y_{0} = \overline{k}_{AB}); assert(x_{0} = B); \{z\}_{k_{B}}⟩, ⟨\{⟨\overline{k}′_{AB}, A⟩\}_{k′_{B}}, λ\{⟨y_{0}, z, x_{0}⟩\}_{k′_{A}}. assert(y_{0} = \overline{k}′_{AB}); assert(x_{0} = B); \{z\}_{k′_{B}}⟩), (\{⟨\overline{k}_{AB}, A⟩\}_{k_{B}}, \{⟨\overline{k}′_{AB}, A⟩\}_{k′_{B}}), (λ\{⟨y_{0}, z, x_{0}⟩\}_{k_{A}}. assert(y_{0} = \overline{k}_{AB}); assert(x_{0} = B); \{z\}_{k_{B}}, λ\{⟨y_{0}, z, x_{0}⟩\}_{k′_{A}}. assert(y_{0} = \overline{k}′_{AB}); assert(x_{0} = B); \{z\}_{k′_{B}}),

— corresponding components from principal B at step 3, communicating with A (⟨\{⟨\overline{k}_{AB}, \overline{k}_{B}, B⟩\}_{k_{A}}, λ\{z_{0}\}_{k_{B}}. assert(z_{0} = \overline{k}_{AB}); \{i\}_{\overline{k}_{B}}⟩, ⟨\{⟨\overline{k}′_{AB}, \overline{k}′_{B}, B⟩\}_{k′_{A}}, λ\{z_{0}\}_{k′_{B}}. assert(z_{0} = \overline{k}′_{AB}); \{j\}\overline{k}′_{B}⟩), (\{⟨\overline{k}_{AB}, \overline{k}_{B}, B⟩\}_{k_{A}}, \{⟨\overline{k}′_{AB}, \overline{k}′_{B}, B⟩\}_{k′_{A}}), (λ\{z_{0}\}_{k_{B}}. assert(z_{0} = \overline{k}_{AB}); \{i\}_{\overline{k}_{B}}, λ\{z_{0}\}_{k′_{B}}. assert(z_{0} = \overline{k}′_{AB}); \{j\}\overline{k}′_{B}),

— corresponding components from principal A at step 4, communicating with B (\{\overline{k}_{B}\}_{k_{B}}, \{\overline{k}′_{B}\}_{k′_{B}}),

— corresponding components from principal B at step 5, communicating with A (\{i\}_{\overline{k}_{B}}, \{j\}\overline{k}′_{B}),

— corresponding components from principal A at Step 2, communicating with E (⟨\{⟨\overline{k}_{AE}, A⟩\}_{k_{E}}, λ\{⟨y_{0}, z, x_{0}⟩\}_{k_{A}}. assert(y_{0} = \overline{k}_{AE}); assert(x_{0} = E); \{z\}_{k_{E}}⟩, ⟨\{⟨\overline{k}′_{AE}, A⟩\}_{k′_{E}}, λ\{⟨y_{0}, z, x_{0}⟩\}_{k′_{A}}. assert(y_{0} = \overline{k}′_{AE}); assert(x_{0} = E); \{z\}_{k′_{E}}⟩), (\{⟨\overline{k}_{AE}, A⟩\}_{k_{E}}, \{⟨\overline{k}′_{AE}, A⟩\}_{k′_{E}}), (λ\{⟨y_{0}, z, x_{0}⟩\}_{k_{A}}. assert(y_{0} = \overline{k}_{AE}); assert(x_{0} = E); \{z\}_{k_{E}}, λ\{⟨y_{0}, z, x_{0}⟩\}_{k′_{A}}. assert(y_{0} = \overline{k}′_{AE}); assert(x_{0} = E); \{z\}_{k′_{E}}), (⟨\overline{k}_{AE}, A⟩, ⟨\overline{k}′_{AE}, A⟩), (\overline{k}_{AE}, \overline{k}′_{AE}),

— corresponding components from principal B at Step 3, communicating with E (⟨\{⟨\overline{w}, \overline{k}_{B}, B⟩\}_{k_{A}}, λ\{z_{0}\}_{k_{B}}. assert(z_{0} = \overline{k}_{B}); \{i\}_{\overline{k}_{B}}⟩, ⟨\{⟨\overline{w}′, \overline{k}′_{B}, B⟩\}_{k′_{A}}, λ\{z_{0}\}_{k′_{B}}. assert(z_{0} = \overline{k}′_{B}); \{j\}\overline{k}′_{B}⟩), (\{⟨\overline{w}, \overline{k}_{B}, B⟩\}_{k_{A}}, \{⟨\overline{w}′, \overline{k}′_{B}, B⟩\}_{k′_{A}}), (λ\{z_{0}\}_{k_{B}}. assert(z_{0} = \overline{k}_{B}); \{i\}_{\overline{k}_{B}}, λ\{z_{0}\}_{k′_{B}}. assert(z_{0} = \overline{k}′_{B}); \{j\}\overline{k}′_{B})),

— corresponding components from principal A at Step 4, communicating with E (\{\overline{w}\}_{k_{E}}, \{\overline{w}′\}_{k′_{E}})\}

Figure 3: Bisimulation for the Needham-Schroeder-Lowe protocol order (when the environment is behaving normally) or perhaps in some strange, arbitrary order (when the environment is under the control of a malicious attacker). Thus, contexts play the role of the network, scheduler, and attackers. More details about the encoding—including a more detailed justification of the claim that it is a reasonable encoding of the protocol above—can be found in previous work [32]. We write assert(e_{1}); e_{2} as syntactic sugar for if e_{1} then e_{2} else ⊥.

U = ⟨B, λ{⟨x, y⟩}_{k_{B}}. assert(y = A);
νz. ⟨{⟨x, z, B⟩}_{k_{A}},
λ{z_{0}}_{k_{B}}. assert(z_{0} = z);
{i}_{z}⟩⟩
V = λx. let k_{x} = (if x = B then k_{B} else

                                     if x = E then k_{E} else ⊥) in

νy. ⟨{(y, A)}_{k_{x}},
λ{⟨y_{0}, z, x_{0}⟩}_{k_{A}}. assert(y_{0} = y);
assert(x_{0} = x);
{z}_{k_{x}}⟩

Now, take any integers i and j. We prove that the system W above (where the secret value sent from B to A is i) and the system W′ below (where the secret is j) are bisimilar, which means that the protocol keeps i and j secret against attackers.

U′ = ⟨B, λ{⟨x, y⟩}_{k′_{B}}. assert(y = A);
νz. ⟨{⟨x, z, B⟩}_{k′_{A}},
λ{z_{0}}_{k′_{B}}. assert(z_{0} = z);
{j}_{z}⟩⟩
V′ = λx. let k_{x} = (if x = B then k′_{B} else

                                      if x = E then k′_{E} else ⊥) in

νy. ⟨{(y, A)}_{k_{x}},
λ{⟨y_{0}, z, x_{0}⟩}_{k′_{A}}. assert(y_{0} = y);
assert(x_{0} = x);
{z}_{k_{x}}⟩
W′ = ⟨λx. {x}_{k′_{A}}, λx. {x}_{k′_{B}}, k′_{E}, U′, V′⟩

The construction of the bisimulation X is by induction, following the same basic pattern as Example 4.7. The base case is (∅, ∅, ∅) ∈ X. The induction rule is as follows. Take any (s, s′, R) ∈ X. Take any \overline{w} = [\overline{v}/\overline{x}]\overline{e} and \overline{w}′ = [\overline{v}′/\overline{x}]\overline{e} with (\overline{v}, \overline{v}′) ∈ R and Seals(\overline{e}) = ∅. Take any t ⊇ s and t′ ⊇ s′ of the forms \{k_{A}, k_{B}, k_{E}, \overline{k}_{AB}, \overline{k}_{AE}, \overline{k}_{B}, \overline{k}\} and \{k′_{A}, k′_{B}, k′_{E}, \overline{k}′_{AB}, \overline{k}′_{AE}, \overline{k}′_{B}, \overline{k}′\}. Then, (t, t′, T ) ∈ X for any subset T of the set S given in Figure 3. It is routine to check the conditions of bisimulation for this X.

It is well known that the secrecy property does not hold for the original version of this protocol (i.e., without Lowe’s fix), in which the third message is {N_{A}, N_{B}}_{k_{A}} instead of {N_{A}, N_{B}, B}_{k_{A}} (i.e., the B is missing). This flaw is mirrored in our setting as well: if we tried to construct a bisimulation for this version in the same way as above, it would fail to be a bisimulation for the following reason. Since we would have

(\{⟨\overline{w}, \overline{k}_{B}⟩\}_{k_{A}}, \{⟨\overline{w}′, \overline{k}′_{B}⟩\}_{k′_{A}}) ∈ S

instead of

(\{⟨\overline{w}, \overline{k}_{B}, B⟩\}_{k_{A}}, \{⟨\overline{w}′, \overline{k}′_{B}, B⟩\}_{k′_{A}}) ∈ S

along with (\overline{k}_{AE}, \overline{k}′_{AE}) ∈ S, we would have (\{⟨\overline{k}_{AE}, \overline{k}_{B}⟩\}_{k_{A}}, \{⟨\overline{k}′_{AE}, \overline{k}′_{B}⟩\}_{k′_{A}}) ∈ S by taking \overline{w} = \overline{k}_{AE} and \overline{w}′ = \overline{k}′_{AE} in the definition of X above. Since we would have

(λ\{⟨y_{0}, z⟩\}_{k_{A}}. assert(y_{0} = \overline{k}_{AE}); \{z\}_{k_{E}},
λ\{⟨y_{0}, z⟩\}_{k′_{A}}. assert(y_{0} = \overline{k}′_{AE}); \{z\}_{k′_{E}}) ∈ S

as well instead of

(λ\{⟨y_{0}, z, x_{0}⟩\}_{k_{A}}. assert(y_{0} = \overline{k}_{AE}); assert(x_{0} = E); \{z\}_{k_{E}},
λ\{⟨y_{0}, z, x_{0}⟩\}_{k′_{A}}. assert(y_{0} = \overline{k}′_{AE}); assert(x_{0} = E); \{z\}_{k′_{E}}) ∈ S

we should also have (\{\overline{k}_{B}\}_{k_{E}}, \{\overline{k}′_{B}\}_{k′_{E}}) ∈ S by applying these functions to the previous ciphertexts, according the condition of bisimulation for functions (Condition 7). Furthermore, since (k_{E}, k′_{E}) ∈ S, we would need (\overline{k}_{B}, \overline{k}′_{B}) ∈ S as well, according to the condition of bisimulation for sealed values (Condition 6). Then, since (\{i\}_{\overline{k}_{B}}, \{j\}\overline{k}′_{B}) ∈ S, we should require (i, j) ∈ S. This contradicts with the condition of bisimulation for constants (Condition 3) if i ≠ j. Observe how the same attack is prevented in the fixed version of this protocol: the assertion assert(x_{0} = E) fails since x_{0} is bound to B.

5 Soundness and Completeness

Bisimilarity, written ∼, is the largest bisimulation. It exists because the union of two bisimulations is always a bisimulation. We will need several simple lemmas about bisimulation in the development that follows.

Lemma 5.1 (Monotonicity). Take any bisimulation X. For any (s, s′, R) ∈ X and (t, t′, S) ∈ X with R ⊆ S, if (s) v X_{R} (s′) v′, then (t) v X_{S} (t′) v′.

Proof. Immediate from the definitions of (s) v X_{R} (s′) v′ and (t) v X_{S} (t′) v′. □

Lemma 5.2 (Addition of Fresh Seals). Take any bisimulation X and (s, s′, R) ∈ X. Then, X ∪ {(s ⊎ {k}, s′ ⊎ {k′}, R ⊎ {(k, k′)})} is a bisimulation for any k ∉ s and k′ ∉ s′.

Proof. Straightforward by checking the conditions of bisimulation. □

We want to show that the bisimilarity ∼ coincides with the contextual equivalence ≡. Since we defined ∼ by co-induction, the easy direction is showing that contextual equivalence implies bisimilarity.

Lemma 5.3 (Completeness of Bisimilarity). ≡ ⊆ ∼.

Proof. Since ∼ is the greatest bisimulation, it suffices to check that ≡ is a bisimulation. Condition 1 is immediate since it is the same as Condition (1) in the definition of contextual equivalence. Condition 2 follows by considering contexts which destruct v and v′, i.e., a context applying them as functions, a context projecting them as tuples, etc. Condition 3 follows by considering a context like if [ ] = c then () else ⊥. Condition 4 follows from Lemma 3.4 (2). Condition 5 follows by considering a context like let {x}_{y} = {()}_{z} in x else ⊥, setting y = k_{1} and z = k_{2} in the left-hand side, and y = k′_{1} and z = k′_{2} in the right-hand side. Condition 6 follows by considering contexts of the form let {x}_{y} = z in e—setting y = k and z = {v}_{k} in the left-hand side, and y = k′ and z = {v′}_{k′} in the right-hand-side—and by Lemma 3.4 (4). Condition 7 follows by Lemma 3.4 (1) together with Lemma 3.4 (3) to add the fresh seals \overline{k} and \overline{k}′, Lemma 3.5 to make the arguments v and v′, and Lemma 3.6 to remove them after the applications. □

Next, we need to prove soundness, i.e., that bisimilarity implies contextual equivalence. For this purpose, we define the following relation.

Definition 5.4 (Bisimilarity in Context). We define ≅ as

\{(s, s′, R, [\overline{v}/\overline{x}]e_{0}, [\overline{v}′/\overline{x}]e_{0}) | (s) \overline{v} ∼_{R} (s′) \overline{v}′ ∧ Seals(e_{0}) = ∅\}

where (s) \overline{v} ∼_{R} (s′) \overline{v}′ is a shorthand for (s) v_{1} ∼_{R} (s′) v′_{1} ∧ … ∧ (s) v_{n} ∼_{R} (s′) v′_{n}.

We write (s) e ≅_{R} (s′) e′ for (s, s′, R, e, e′) ∈ ≅. The intuition of this definition is: ≅ relates bisimilar values \overline{v} and \overline{v}′ put in context e_{0}.

The two lemmas below are the key properties of our bisimulation. The first states that evaluation preserves ≅, the second that ≅ implies observational equivalence (i.e., if evaluation of one expression converges, then evaluation of the other expression also converges).

Lemma 5.5 (Fundamental Property, Part I). Suppose (s_{0}) e ≅_{R_{0}} (s′_{0}) e′. If (s_{0}) e ⇓ (t) w and (s′_{0}) e′ ⇓ (t′) w′, then (t) w ≅_{R} (t′) w′ for some R ⊇ R_{0}.

Proof. By induction on the derivation of (s_{0}) e ⇓ (t) w.

By the definition of ≅, we have e = [\overline{v}_{0}/\overline{x}_{0}]e_{0} and e′ = [\overline{v}′_{0}/\overline{x}_{0}]e_{0} for some (s_{0}) \overline{v}_{0} ∼_{R_{0}} (s′_{0}) \overline{v}′_{0} with Seals(e_{0}) = ∅. If e is a value, then e′ is also a value (easy case analysis on the syntax of e_{0}) and the result is immediate, because every value evaluates only to itself. We consider the remaining possibilities in detail, assuming that e_{0} is neither a value nor a variable; there is one case for each of the non-value evaluation rules.

Case (E-Tuple), (E-Do-Seal). Straightforward induction.

Case (E-Proj). Straightforward induction, using Condition 4 of the definition of bisimulation.

Case (E-Prim), (E-Cond-True) and (E-Cond-False). Straightforward induction, using Condition 3 of the definition of bisimulation.

Case (E-New). Straightforward induction, using Lemma 5.2.

Case (E-App). Then e_{0} has the form e_{1}e_{2} and the final step in the derivation of (s_{0}) e ⇓ (t) w has the following form:

\frac{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) w_{1} (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) w_{2} …}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](e_{1}e_{2}) ⇓ (t) w}

The third premise is elided; we will come back to it in a minute. Since (E-App) is the only rule for evaluating an application, the final step in the derivation of (s′_{0}) e′ ⇓ (t′) w′ has a similar form:

\frac{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) w′_{1} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) w′_{2} …}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](e_{1}e_{2}) ⇓ (t′) w′}

By the definition of ≅, we have (s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ≅_{R_{0}} (s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1}. Thus, by the induction hypothesis on the subderivations for [\overline{v}_{0}/\overline{x}_{0}]e_{1} and [\overline{v}′_{0}/\overline{x}_{0}]e_{1}, we obtain (s_{1}) w_{1} ≅_{R_{1}} (s′_{1}) w′_{1} for some R_{1} ⊇ R_{0}. By the definition of ≅, we have w_{1} = [\overline{v}_{1}/\overline{x}_{1}]e_{3} and w′_{1} = [\overline{v}′_{1}/\overline{x}_{1}]e_{3} for some (s_{1}) \overline{v}_{1} ∼_{R_{1}} (s′_{1}) \overline{v}′_{1} with Seals(e_{3}) = ∅. Since (s_{0}) \overline{v}_{0} ∼_{R_{0}} (s′_{0}) \overline{v}′_{0} and R_{0} ⊆ R_{1}, we have (s_{1}) \overline{v}_{0} ∼_{R_{1}} (s′_{1}) \overline{v}′_{0} by Lemma 5.1.

Applying the definition of ≅ again, we have (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ≅_{R_{1}} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2}. So we may apply the induction hypothesis to the subderivations for [\overline{v}_{0}/\overline{x}_{0}]e_{2} and [\overline{v}′_{0}/\overline{x}_{0}]e_{2}, obtaining (s_{2}) w_{2} ≅_{R_{2}} (s′_{2}) w′_{2} for some R_{2} ⊇ R_{1}. By the definition of ≅, we have w_{2} = [\overline{v}_{2}/\overline{x}_{2}]e_{4} and w′_{2} = [\overline{v}′_{2}/\overline{x}_{2}]e_{4} for some (s_{2}) \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{2} with Seals(e_{4}) = ∅. Since (s_{1}) \overline{v}_{1} ∼_{R_{1}} (s′_{1}) \overline{v}′_{1} and R_{1} ⊆ R_{2}, we have (s_{2}) \overline{v}_{1} ∼_{R_{2}} (s′_{2}) \overline{v}′_{1} by Lemma 5.1.

Now we need to deal with the third premises. Since w_{1} = [\overline{v}_{1}/\overline{x}_{1}]e_{3} and w′_{1} = [\overline{v}′_{1}/\overline{x}_{1}]e_{3} must both be functions, e_{3} itself must be either a function or a variable; we consider these cases in turn.

Sub-case e_{3} = λy. e_{5}. Then the final steps in the evaluation derivations for e and e′ are:

\frac{\begin{matrix}(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) [\overline{v}_{1}/\overline{x}_{1}](λy. e_{5}) \\ (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) [\overline{v}_{2}/\overline{x}_{2}]e_{4} \\ (s_{2}) [\overline{v}_{1}, \overline{v}_{2}/\overline{x}_{1}, \overline{x}_{2}][e_{4}/y]e_{5} ⇓ (t) w \end{matrix}}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](e_{1}e_{2}) ⇓ (t) w} ; \frac{\begin{matrix}(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) [\overline{v}′_{1}/\overline{x}_{1}](λy. e_{5}) \\ (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) [\overline{v}′_{2}/\overline{x}_{2}]e_{4} \\ (s′_{2}) [\overline{v}′_{1}, \overline{v}′_{2}/\overline{x}_{1}, \overline{x}_{2}][e_{4}/y]e_{5} ⇓ (t′) w′ \end{matrix}}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](e_{1}e_{2}) ⇓ (t′) w′}

Since (s_{2}) \overline{v}_{1}, \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{1}, \overline{v}′_{2} and Seals(e_{4}) = Seals(e_{5}) = ∅, we have (s_{2}) [\overline{v}_{1}, \overline{v}_{2}/\overline{x}_{1}, \overline{x}_{2}][e_{4}/y]e_{5} ≅_{R_{2}} (s′_{2}) [\overline{v}′_{1}, \overline{v}′_{2}/\overline{x}_{1}, \overline{x}_{2}][e_{4}/y]e_{5} by the definition of ≅. So we may apply the induction hypothesis a third time, yielding (t) w ≅_{R} (t′) w′ for some R ⊇ R_{2} ⊇ R_{1} ⊇ R_{0}, as required.

Sub-case e_{3} = x_{0}_{i}, with v_{1}_{i} = λy. e_{5} and v′_{1}_{i} = λy. e′_{5} . Then the evaluation derivations for e and e′ are:

\frac{\begin{matrix}(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) λy. e_{5} \\ (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) [\overline{v}_{2}/\overline{x}_{2}]e_{4} \\ (s_{2}) [[\overline{v}_{2}/\overline{x}_{2}]e_{4}/y]e_{5} ⇓ (t) w \end{matrix}}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](e_{1}e_{2}) ⇓ (t) w} ; \frac{\begin{matrix}(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) λy. e′_{5} \\ (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) [\overline{v}′_{2}/\overline{x}_{2}]e_{4} \\ (s′_{2}) [[\overline{v}′_{2}/\overline{x}_{2}]e_{4}/y]e_{5} ⇓ (t′) w′ \end{matrix}}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](e_{1}e_{2}) ⇓ (t′) w′}

Since (s_{2}) [[\overline{v}_{2}/\overline{x}_{2}]e_{4}/y]e_{5} ⇓ (t) w and (s′_{2}) [[\overline{v}′_{2}/\overline{x}_{2}]e_{4}/y]e_{5} ⇓ (t′) w′, we have (s_{2}) (λy. e_{5})[\overline{v}_{2}/\overline{x}_{2}]e_{4} ⇓ (t) w and (s_{2}) (λy. e′_{5})[\overline{v}′_{2}/\overline{x}_{2}]e_{4} ⇓ (t′) w′ by (E-App). Then, since (s_{2}) λy. e_{5} ∼_{R_{2}} (s′_{2}) λy. e′_{5} and (s_{2}) \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{2} and since Seals(e_{4}) = ∅, we have (t, t′, R_{2}∪\{(w, w′)\}) ∈ ∼ by Condition 7 of the definition of bisimulation. Thus, by the definition of ≅, we have (t) [w/z]z ≅_{R_{2}∪{(w,w′)}} (t′) [w′/z]z. That is, (t) w ≅_{R} (t′) w′ for R = R_{2} ∪ {(w, w′)} ⊇ R_{2} ⊇ R_{1} ⊇ R_{0}, as required.

Case (E-Unseal-Succ). Then e_{0} is of the form let {y}_{e_{1}} = e_{2} in e_{3} else e_{4} and the given evaluation derivations have the forms:

\frac{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) w_{1} (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) w_{2} …}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t) w}

\frac{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) w′_{1} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) w′_{2} …}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t′) w′}

By the definition of ≅, we have (s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ≅_{R_{0}} (s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1}. Thus, by the induction hypothesis, we have (s_{1}) w_{1} ≅_{R_{1}} (s′_{1}) w′_{1} for some R_{1} ⊇ R_{0}. Then, by the definition of ≅, we have w_{1} = [\overline{v}_{1}/\overline{x}_{1}]e_{5} and w′_{1} = [\overline{v}′_{1}/\overline{x}_{1}]e_{5} for some (s_{1}) \overline{v}_{1} ∼_{R_{1}} (s′_{1}) \overline{v}′_{1} and Seals(e_{5}) = ∅. Since (s_{0}) \overline{v}_{0} ∼_{R_{0}} (s′_{0}) \overline{v}′_{0} and R_{0} ⊆ R_{1}, we have (s_{1}) \overline{v}_{0} ∼_{R_{1}} (s′_{1}) \overline{v}′_{0} by Lemma 5.1.

Now, again by the definition of ≅, we have (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ≅_{R_{1}} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2}. Thus, by the induction hypothesis, we have (s_{2}) w_{2} ≅_{R_{2}} (s′_{2}) w′_{2} for some R_{2} ⊇ R_{1}. Then, by the definition of ≅, we have w_{2} = [\overline{v}_{2}/\overline{x}_{2}]e_{6} and w′_{2} = [\overline{v}′_{2}/\overline{x}_{2}]e_{6} for some (s_{2}) \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{2} and Seals(e_{6}) = ∅. Since (s_{1}) \overline{v}_{0} ∼_{R_{1}} (s′_{1}) \overline{v}′_{0} and R_{1} ⊆ R_{2}, we have (s_{2}) \overline{v}_{0} ∼_{R_{2}} (s′_{2}) \overline{v}′_{0} by Lemma 5.1. Furthermore, since (s_{1}) \overline{v}_{1} ∼_{R_{1}} (s′_{1}) \overline{v}′_{1} and R_{1} ⊆ R_{2}, we have (s_{2}) \overline{v}_{1} ∼_{R_{2}} (s′_{2}) \overline{v}′_{1} by Lemma 5.1.

Since w_{1} = [\overline{v}_{1}/\overline{x}_{1}]e_{5} and w′_{1} = [\overline{v}′_{1}/\overline{x}_{1}]e_{5} must be seals while w_{2} = [\overline{v}_{2}/\overline{x}_{2}]e_{6} and w′_{2} = [\overline{v}′_{2}/\overline{x}_{2}]e_{6} must be values sealed under these seals, there are two possible forms for e_{5} and e_{6}.

Sub-case e_{5} = x_{1}_{i} and e_{6} = {e_{7}}_{x_{2}_{j}}. The evaluation derivation for e is

\frac{\begin{matrix}(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) v_{1}_{i} \\ (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) \{[\overline{v}_{2}/\overline{x}_{2}]e_{7}\}_{v_{2}_{j}} \\ (s_{2}) [\overline{v}_{0}, \overline{v}_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ⇓ (t) w \end{matrix}}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t) w}

where v_{1}_{i} = v_{2}_{j}. Since (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) v′_{1}_{i} and (s_{2}) v_{2}_{j} ∼_{R_{2}} (s′_{2}) v′_{2}_{j}, we have v′_{1}_{i} = v′_{2}_{j} by Condition 5 of bisimulation. Then, the evaluation derivation for e′ is:

\frac{\begin{matrix}(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) v′_{1}_{i} \\ (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) \{[\overline{v}′_{2}/\overline{x}_{2}]e_{7}\}_{v′_{2}}_{j} \\ (s′_{2}) [\overline{v}′_{0}, \overline{v}′_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ⇓ (t′) w′ \end{matrix}}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t′) w′}

Since (s_{2}) \overline{v}_{0}, \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{0}, \overline{v}′_{2} and Seals(e_{3}) = Seals(e_{7}) = ∅, we have (s_{2}) [\overline{v}_{0}, \overline{v}_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ≅_{R_{2}} (s′_{2}) [\overline{v}′_{0}, \overline{v}′_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} by the definition of ≅. Then, by the induction hypothesis, we have (t) w ≅_{R} (t′) w′ for some R ⊇ R_{2} ⊇ R_{1} ⊇ R_{0}.

Sub-case e_{5} = x_{1}_{i} and e_{6} = x_{2}_{j}. The evaluation derivation for e is

\frac{\begin{matrix}(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) v_{1}_{i} (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) v_{2}_{j} \\ (s_{2}) [\overline{v}_{0}, v/\overline{x}_{0}, y]e_{3} ⇓ (t) w \end{matrix}}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t) w}

where v_{2}_{j} = {v}_{v_{1}_{i}} for some v. Since (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) v′_{1}_{i} and (s_{2}) v_{2}_{j} ∼_{R_{2}} (s′_{2}) v′_{2}_{j}, we have v′_{2}_{j} = {v′}_{k′} for some (s_{2}) v ∼_{R_{2}} (s′_{2}) v′ and (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) k′ by Condition 6 of bisimulation.

Furthermore, since (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) k′ and (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) v′_{1}_{i}, we have k′ = v′_{1}_{i} by Condition 5 of bisimulation. Then, the evaluation derivation for e′ is:

\frac{\begin{matrix}(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) v′_{1}_{i} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) v′_{2}_{j} \\ (s′_{2}) [\overline{v}′_{0}, v′/\overline{x}_{0}, y]e_{3} ⇓ (t′) w′ \end{matrix}}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t′) w′}

Since (s_{2}) \overline{v}_{0}, v ∼_{R_{2}} (s′_{2}) \overline{v}′_{0}, v′ and Seals(e_{3}) = ∅, we have (s_{2}) [\overline{v}_{0}, v/\overline{x}_{0}, y]e_{3} ≅_{R_{2}} (s′_{2}) [\overline{v}′_{0}, v′/\overline{x}_{0}, y]e_{3} by the definition of ≅. Then, by the induction hypothesis, we have (t) w ≅_{R} (t′) w′ for some R ⊇ R_{2} ⊇ R_{1} ⊇ R_{0}.

Case (E-Unseal-Fail). Similar to the case of (E-Unseal-Succ). □

Lemma 5.6 (Fundamental Property, Part II). If (s_{0}) e ≅_{R_{0}} (s′_{0}) e′, then (s_{0}) e ⇓ ⟺ (s′_{0}) e′ ⇓.

Proof. We assume (s_{0}) e ⇓ (t) w and prove (s′_{0}) e′ ⇓ by induction on the derivation of (s_{0}) e ⇓ (t) w. The other direction follows by symmetry.

The argument is very similar to the proof of Lemma 5.5, except that we are proving the existence of an evaluation derivation for e′ by using the given evaluation derivation for e, instead of proving a property of given evaluation derivations for e and e′. We show just the most interesting case: the one for (E-Unseal-Succ).

By the definition of ≅, we have e = [\overline{v}_{0}/\overline{x}_{0}]e_{0} and e′ = [\overline{v}′_{0}/\overline{x}_{0}]e_{0} for some (s_{0}) \overline{v}_{0} ∼_{R_{0}} (s′_{0}) \overline{v}′_{0} and Seals(e_{0}) = ∅. In the case of (E-Unseal-Succ), e_{0} is of the form let {y}_{e_{1}} = e_{2} in e_{3} else e_{4} and the evaluation derivation for e has the following form:

\frac{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) w_{1} (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) w_{2} …}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t) w}

We aim to derive an evaluation of e′ of a similar form:

\frac{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) w′_{1} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) w′_{2} …}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t′) w′}

By the definition of ≅, we have (s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ≅_{R_{0}} (s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1}. Since (s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓, we have (s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) w′_{1} for some s′_{1} and w′_{1} by the induction hypothesis. Furthermore, by Lemma 5.5, we have (s_{1}) w_{1} ≅_{R_{1}} (s′_{1}) w′_{1} for some R_{1} ⊇ R_{0}. Then, by the definition of ≅, we have w_{1} = [\overline{v}_{1}/\overline{x}_{1}]e_{5} and w′_{1} = [\overline{v}′_{1}/\overline{x}_{1}]e_{5} for some (s_{1}) \overline{v}_{1} ∼_{R_{1}} (s′_{1}) \overline{v}′_{1} and Seals(e_{5}) = ∅. Since (s_{0}) \overline{v}_{0} ∼_{R_{0}} (s′_{0}) \overline{v}′_{0} and R_{0} ⊆ R_{1}, we have (s_{1}) \overline{v}_{0} ∼_{R_{1}} (s′_{1}) \overline{v}′_{0} by Lemma 5.1.

Now, again by the definition of ≅, we have (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ≅_{R_{1}} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2}. Since (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓, we have (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) w′_{2} for some s′_{2} and w′_{2} by the induction hypothesis. Furthermore, by Lemma 5.5, we have (s_{2}) w_{2} ≅_{R_{2}} (s′_{2}) w′_{2} for some R_{2} ⊇ R_{1}. Then, by the definition of ≅, we have w_{2} = [\overline{v}_{2}/\overline{x}_{2}]e_{6} and w′_{2} = [\overline{v}′_{2}/\overline{x}_{2}]e_{6} for some (s_{2}) \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{2} and Seals(e_{6}) = ∅. Since (s_{1}) \overline{v}_{0} ∼_{R_{1}} (s′_{1}) \overline{v}′_{0} and R_{1} ⊆ R_{2}, we have (s_{2}) \overline{v}_{0} ∼_{R_{2}} (s′_{2}) \overline{v}′_{0} by Lemma 5.1. Furthermore, since (s_{1}) \overline{v}_{1} ∼_{R_{1}} (s′_{1}) \overline{v}′_{1} and R_{1} ⊆ R_{2}, we have (s_{2}) \overline{v}_{1} ∼_{R_{2}} (s′_{2}) \overline{v}′_{1} by Lemma 5.1.

Since w_{1} = [\overline{v}_{1}/\overline{x}_{1}]e_{5} must be a seal while w_{2} = [\overline{v}_{2}/\overline{x}_{2}]e_{6} must be a value sealed under this seal, there are two possible forms for e_{5} and e_{6}.

Sub-case e_{5} = x_{1}_{i} and e_{6} = {e_{7}}_{x_{2}_{j}}. The evaluation derivation for e is

\frac{\begin{matrix}(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) v_{1}_{i} \\ (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) \{[\overline{v}_{2}/\overline{x}_{2}]e_{7}\}_{v_{2}_{j}} \\ (s_{2}) [\overline{v}_{0}, \overline{v}_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ⇓ (t) w \end{matrix}}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t) w}

where v_{1}_{i} = v_{2}_{j}. Since (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) v′_{1}_{i} and (s_{2}) v_{2}_{j} ∼_{R_{2}} (s′_{2}) v′_{2}_{j} where v_{1}_{i} and v_{2}_{j} are seals, v′_{1}_{i} and v′_{2}_{j} are also seals by Condition 2 of bisimulation. Furthermore, v′_{1}_{i} = v′_{2}_{j} by Condition 5 of bisimulation.

Meanwhile, since (s_{2}) \overline{v}_{0}, \overline{v}_{2} ∼_{R_{2}} (s′_{2}) \overline{v}′_{0}, \overline{v}′_{2} and Seals(e_{3}) = Seals(e_{7}) = ∅, we have (s_{2}) [\overline{v}_{0}, \overline{v}_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ≅_{R_{2}} (s′_{2}) [\overline{v}′_{0}, \overline{v}′_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} by the definition of ≅. Then, since (s_{2}) [\overline{v}_{0}, \overline{v}_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ⇓, we have (s′_{2}) [\overline{v}′_{0}, \overline{v}′_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ⇓ (t′) w′ for some t′ and w′ by the induction hypothesis.

Therefore, since v′_{1}_{i} = v′_{2}_{j}, we can derive an evaluation of e′ as follows:

\frac{\begin{matrix}(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) v′_{1}_{i} \\ (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) \{[\overline{v}′_{2}/\overline{x}_{2}]e_{7}\}_{v′_{2}}_{j} \\ (s′_{2}) [\overline{v}′_{0}, \overline{v}′_{2}/\overline{x}_{0}, \overline{x}_{2}][e_{7}/y]e_{3} ⇓ (t′) w′ \end{matrix}}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t′) w′}

Sub-case e_{5} = x_{1}_{i} and e_{6} = x_{2}_{j}. The evaluation derivation for e is

\frac{\begin{matrix}(s_{0}) [\overline{v}_{0}/\overline{x}_{0}]e_{1} ⇓ (s_{1}) v_{1}_{i} (s_{1}) [\overline{v}_{0}/\overline{x}_{0}]e_{2} ⇓ (s_{2}) v_{2}_{j} \\ (s_{2}) [\overline{v}_{0}, v/\overline{x}_{0}, y]e_{3} ⇓ (t) w \end{matrix}}{(s_{0}) [\overline{v}_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t) w}

where v_{2}_{j} = {v}_{v_{1}_{i}} for some v. Since (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) v′_{1}_{i} and (s_{2}) v_{2}_{j} ∼_{R_{2}} (s′_{2}) v′_{2}_{j} where v_{1}_{i} is a seal and v_{2}_{j} is a sealed value, v′_{1}_{i} is also a seal and v′_{2}_{j} is also a sealed value by Condition 2 of bisimulation. Furthermore, we have v′_{2}_{j} = {v′}_{k′} for some (s_{2}) v ∼_{R_{2}} (s′_{2}) v′ and (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) k′ by Condition 6 of bisimulation. Moreover, since (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) k′ and (s_{2}) v_{1}_{i} ∼_{R_{2}} (s′_{2}) v′_{1}_{i}, we have k′ = v′_{1}_{i} by Condition 5 of bisimulation.

Meanwhile, since (s_{2}) \overline{v}_{0}, v ∼_{R_{2}} (s′_{2}) \overline{v}′_{0}, v′ and Seals(e_{3}) = ∅, we have (s_{2}) [\overline{v}_{0}, v/\overline{x}_{0}, y]e_{3} ≅_{R_{2}} (s′_{2}) [\overline{v}′_{0}, v′/\overline{x}_{0}, y]e_{3} by the definition of ≅. Then, since (s_{2}) [\overline{v}_{0}, v/\overline{x}_{0}, y]e_{3} ⇓, we have (s′_{2}) [\overline{v}′_{0}, v′/\overline{x}_{0}, y]e_{3} ⇓ (t′) w′ for some t′ and w′ by the induction hypothesis.

Therefore, since v′_{2}_{j} = {v′}_{v′_{1}}_{i}, we can derive an evaluation of e′

\frac{\begin{matrix}(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}]e_{1} ⇓ (s′_{1}) v′_{1}_{i} (s′_{1}) [\overline{v}′_{0}/\overline{x}_{0}]e_{2} ⇓ (s′_{2}) v′_{2}_{j} \\ (s′_{2}) [\overline{v}′_{0}, v′/\overline{x}_{0}, y]e_{3} ⇓ (t′) w′ \end{matrix}}{(s′_{0}) [\overline{v}′_{0}/\overline{x}_{0}](let \{y\}_{e_{1}} = e_{2} in e_{3} else e_{4}) ⇓ (t′) w′}

as required. □

An immediate consequence of the previous property is that bisimulation implies contextual equivalence.

Corollary 5.7 (Soundness of Bisimilarity). ∼ ⊆ ≡.

Proof. Suppose (s, s′, R) ∈ ∼ and we shall prove (s, s′, R) ∈ ≡. The first condition of contextual equivalence is immediate since it is the same as the first condition of bisimulation. The second condition of contextual equivalence is proved as follows. Take any (\overline{v}, \overline{v}′) ∈ R and any e with Seals(e) = ∅. By definition, (s) [\overline{v}/\overline{x}]e ≅_{R} (s′) [\overline{v}′/\overline{x}]e. Thus, by Lemma 5.6, (s) [\overline{v}/\overline{x}]e ⇓ ⟺ (s′) [\overline{v}′/\overline{x}]e ⇓. □

Combining soundness and completeness, we obtain the main theorem about our bisimulation: that bisimilarity coincides with contextual equivalence.

Theorem 5.8. ∼ = ≡.

Proof. By Lemma 5.3 and Corollary 5.7. □

6 Extension with Equality for Sealed Values

A number of variants of λ_{seal} can be considered. For example, the version of λ_{seal} in this paper does not allow a context to test two sealed values for equality. This is reasonable if the environment is a safe runtime system (where sealing can be implemented just by tagging) which disallows comparison of sealed values. It is unrealistic, however, to expect such a restriction in an arbitrary (perhaps hostile) environment, where sealing must be implemented by encryption. Fortunately, our technique extends directly to such a modest change as adding equality for sealed values. For instance, it is straightforward to extend λ_{seal} with syntactic equality =_{1} for first-order values (including sealed values) along with an additional condition of bisimulation: v_{1} =_{1} v_{2} ⟺ v′_{1} =_{1} v′_{2} for every (v_{1}, v′_{1}) ∈ R and (v_{2}, v′_{2}) ∈ R. Then, it is also straightforward to prove the soundness and completeness of bisimilarity under this extension, with an additional lemma that ≅ respects =_{1} (which can be proved by induction on the syntax of values being compared).

Of course, the more observations we allow, the more difficult it becomes to establish the equivalence of two given modules. For example, the two implementations of complex numbers given in the introduction are no longer equivalent (or bisimilar) under the extension above, because there are many polar representations of 0 + 0i while there is only one Cartesian representation. So, for example, a context like

                 C[ ] = let x = [ ].from_re_and_im(0.0, 0.0) in

                          let y = [ ].from_re_and_im(-1.0, 0.0) in
                          x =_{1} [ ].multiply x y

would distinguish CartesianComplex and PolarComplex. To recover the equivalence, the polar representation of 0 + 0i must be standardized and checks inserted wherever it can be created:

     let from_re_and_im =
       fun (x, y) ->
         let z =
           if x = 0.0 && y = 0.0 then (0.0, 0.0) else
           (sqrt(x * x + y * y), atan2(y, x)) in
         <seal z under k>

     let multiply =
       fun (z1, z2) ->
         let (r1, t1) = <unseal z1 under k> in
         let (r2, t2) = <unseal z2 under k> in
         let z =
           if r1 = 0.0 || r2 = 0.0 then (0.0, 0.0) else
           (r1 * r2, t1 + t2) in
         <seal z under k>

7 Related Work

As discussed in the introduction, sealing was first proposed by Morris [20, 21] and has been revisited in more recent work on extending the “scope” (in both informal and technical senses) of type abstraction in various forms [7, 12, 28, 30].

Bisimulations have been studied extensively in process calculi. In particular, bisimulations for the spi-calculus [1, 2, 5, 6] are the most relevant to this work, because the perfect encryption in spi-calculus is very similar to dynamic sealing in our calculus. Our bisimulation is analogous to bisimulations for spi-calculus in that both keep track of the environment’s knowledge.

However, since processes and messages are different entities in spi-calculus, all the technicalities— i.e., definitions and proofs—must be developed separately for processes and messages. By contrast, our bisimulation is monolithic and more straightforward. In particular, the condition of our bisimulation for functions (Condition 7 in Definition 4.1) is simpler than conditions of bisimulations in spi-calculus for the case of input, where the received messages are defined by another large set of separate rules and/or not so much restricted as function arguments in Condition 7, leading to more complex bisimulations.

Furthermore, it is possible even to encode and verify some (though not all) security protocols in our framework. The encoding naturally models the concurrency among principals and attackers (including so-called “necessarily parallel” attacks) by means of interleaving. Thanks to higher-order functions, we can also simulate asymmetric encryption and can thereby express public-key protocols such as Needham-Schroeder-Lowe (unlike the spi-calculus) without extending the calculus. See our previous work [32] for further discussion about this encoding of security protocols.

While our bisimulation is complete with respect to contextual equivalence, no completeness proof is available for spi-calculus bisimulations: the original [2] is known to be incomplete; others [5, 6] are proved to be complete only for some subset of processes (called structurally image-finite processes) despite the claim of completeness for one of them [6]; proof of (soundness and) completeness for bisimilarity in applied π-calculus [1, Theorem 1] has not been written down in a form accessible to others [personal communication, August 2004].

Another line of work on bisimulations in process calculi concerns techniques for lightening the burden of constructing a bisimulation—e.g., Milner and Sangiorgi’s “bisimulation up to” [29]. It remains to be seen whether these techniques would be useful in our setting. Note that our operational semantics is built upon big-step evaluation (as opposed to small-step reduction) in the first place, which cuts down the intermediate terms and reduces the size of a bisimulation.

Abramsky [4] studied applicative bisimulation for the λ-calculus. For functions λx. e and λx. e′ to be bisimilar, it requires that (λx. e)d and (λx. e′)d are observationally equivalent for any closed d, and that they evaluate to bisimilar values if the evaluations converge. Thus, it requires the two arguments to be the same, which actually makes the soundness proof harder [9]. We avoided this problem by allowing some difference between the arguments of functions in our bisimulation.

Jeffrey and Rathke [10] defined bisimulation for λ-calculus with name generation, of which our seal generation is an instance. Although their theory does distinguish private and public names, it lacks a proper mechanism to keep track of contexts’ knowledge of name-involving values in general, such as functions containing names inside the bodies. As a result, they had to introduce additional language constructs—such as global references [10] or communication channels [11]—for the bisimulation to be sound. We solved this problem by using a set of relations (rather than a single relation) between values as a bisimulation, i.e., by considering multiple pairs of values at once.

A well-known method of proving the abstraction obtained by type abstraction is logical relations [17, 27]. Although they are traditionally defined on denotational models, they have recently been studied in the syntactic setting of term models as well [24, 25]. In previous work [32], we have defined syntactic logical relations for perfect encryption and used them to prove secrecy properties of security protocols. Although logical relations are analogous to bisimulations in that both relate corresponding values between two different programs, logical relations are defined by induction on types and cannot be applied in untyped settings. Moreover, logical relations in more sophisticated settings (such as recursive functions and recursive types) than simply typed λ-calculus tend to become rather complicated. Indeed, “keys encrypting keys” (as in security protocols) required nontrivial extension in the logical relations above, while they imposed no difficulty to our bisimulation in this paper.

8 Conclusions

We have defined a bisimulation for λ_{seal} and proved its soundness and completeness with respect to contextual equivalence.

There are several directions for future work. One is to apply our bisimulation to more examples, e.g., to prove the full abstraction of our translation of type abstraction into dynamic sealing— indeed, this was actually the original motivation for the present work. When the target language is untyped, the translation of source term ⊢ M : τ can be given as let x = erase(M) in E_{∅}^{+}(x, τ), where E^{+} is defined like Figure 4 along with its dual E^{−} in a type-directed manner. Intuitively, E^{+} is a “firewall” that protects terms from contexts, where E^{−} is a “sandbox” that protects contexts from terms. Bisimulation would help proving properties of this translation. We may also be able to use such an interpretation of type abstraction by dynamic sealing as a (both formal and informal) basis for reasoning about type abstraction in broader settings.

Another possibility is to define and use bisimulation for other forms of information hiding, such as type abstraction. Our treatment of seals are analogous to the treatment of generative names in general [26, 31], of which abstract types are an instance as soon as they escape from their scope (by communication [30], for example). Thus, it would be possible to define bisimulation for type abstraction in a similar manner to the definition of our bisimulation for dynamic sealing. This is interesting because such bisimulation may be complete with respect to contextual equivalence as in this work, while it is difficult to obtain complete logical relations for type abstraction [24, 25]. See our recent work [33] for further discussions on this topic.

It would also be interesting to extend our developments for more general operations on sealing/encryption as in applied pi-calculus [1]. Recall that the syntax and semantics in Section 2 did

E_{ρ}^{+}(x, bool)  = x
E_{ρ}^{+}(x, τ_{1} × … × τ_{n}) = let ⟨y_{1}, …, y_{n}⟩ = x in
⟨E_{ρ}^{+}(y_{1}, τ_{1}), …, E_{ρ}^{+}(y_{n}, τ_{n})⟩
E_{ρ}^{+}(x, τ → σ)  = λy. let z = xE_{ρ}^{−}(y, τ) in E_{ρ}^{+}(z, σ)
E_{ρ}^{+}(x, ∀α. τ)  = λy. let z = x() in E_{ρ}^{+}(z, τ)
E_{ρ}^{+}(x, ∃α. τ)  = νz. E_{ρ,α↦z}^{+}(x, τ)
E_{ρ}^{+}(x, α)  = {x}_{ρ(α)}
E_{ρ}^{+}(x, α)  = x  if α ∉ Dom(ρ)

E_{ρ}^{−}(x, bool)  = if x then true else false

E_{ρ}^{−}(x, τ_{1} × … × τ_{n}) = let ⟨y_{1}, …, y_{n}⟩ = x in
⟨E_{ρ}^{−}(y_{1}, τ_{1}), …, E_{ρ}^{−}(y_{n}, τ_{n})⟩
E_{ρ}^{−}(x, τ → σ)  = λy. let z = xE_{ρ}^{+}(y, τ) in E_{ρ}^{−}(z, σ)
E_{ρ}^{−}(x, ∀α. τ)  = λy. νz. E_{ρ,α↦z}^{−}(x, τ)
E_{ρ}^{−}(x, ∃α. τ)  = E_{ρ}^{−}(x, τ)
E_{ρ}^{−}(x, α)  = let {y}_{ρ(α)} = x in y else ⊥
E_{ρ}^{−}(x, α)  = x  if α ∉ Dom(ρ)

Figure 4: Translation of type abstraction into dynamic sealing

not allow any primitive op (or constant c) to involve seals.

Mechanical support for bisimulation proofs is of natural interest as well. Full automation is hopeless, since general cases subsume the halting problem (i.e., whether the evaluation of a λexpression converges or diverges), but many of the conditions of bisimulation are easy to check or satisfy by adding elements to the bisimulation. One challenging point would be the case analysis on function arguments [\overline{u}/\overline{x}]d and [\overline{u}′/\overline{x}]d in Condition 7, shown in detail in Example 4.4.

Acknowledgements

We would like to thank Martín Abadi, Andre Scedrov, Naoki Kobayashi, and the members of Programming Language Club at the University of Pennsylvania for suggestions and support throughout the development of this work.

References

[1] Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 104–115, 2001.

[2] Martín Abadi and Andrew D. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5:267–303, 1998. Preliminary version appeared in 7th European Symposium on Programming, Lecture Notes in Computer Science, Springer-Verlag, vol. 1381, pp. 12–26, 1998.

[3] Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999. Preliminary version appeared in Proceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36–47, 1997.

[4] Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65–117. Addison-Wesley, 1990.

[5] Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic processes. SIAM Journal on Computing, 31(3):947–986, 2002. Preliminary version appeared in 14th Annual IEEE Symposium on Logic in Computer Science, pp. 157–166, 1999.

[6] Johannes Borgström and Uwe Nestmann. On bisimulations for the spi calculus. In 9th International Conference on Algebraic Methodology and Software Technology, volume 2422 of Lecture Notes in Computer Science, pages 287–303. Springer-Verlag, 2002.

[7] Derek Dreyer, Karl Crary, and Robert Harper. A type system for higher-order modules. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 236–249, 2003.

[8] Dan Grossman, Greg Morrisett, and Steve Zdancewic. Syntactic type abstraction. ACM Transactions on Programming Languages and Systems, 22(6):1037–1080, 2000. Extended abstract appeared as Principals in Programming Languages: A Syntactic Proof Technique in Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming, pp. 197–207, 1999.

[9] Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, 1996.

[10] Alan Jeffrey and Julian Rathke. Towards a theory of bisimulation for local names. In 14th Annual IEEE Symposium on Logic in Computer Science, pages 56–66, 1999.

[11] Alan Jeffrey and Julian Rathke. A theory of bisimulation for a fragment of Concurrent ML with local names. Theoretical Computer Science, 323:1–48, 2004. Extended abstract appeared in 15th Annual IEEE Symposium on Logic in Computer Science, pp. 311–321, 2000.

[12] James J. Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. Global abstractionsafe marshalling with hash types. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 87–98, 2003.

[13] Xavier Leroy. Applicative functors and fully transparent higher-order modules. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 142–153, 1995.

[14] Barbara Liskov. A history of CLU. In The Second ACM SIGPLAN Conference on History of Programming Languages, pages 133–147, 1993.

[15] Gavin Lowe. An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters, 56(3):131–133, 1995.

[16] Robin Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, 1999.

[17] John C. Mitchell. On the equivalence of data representations. In Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305–330. Academic Press, 1991.

[18] John C. Mitchell and Gordon D. Plotkin. Abstract types have existential types. ACM Transactions on Programming Languages and Systems, 10(3):470–502, 1988. Preliminary version appeared in Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 37–51, 1985.

[19] James H. Morris, Jr. Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology, 1968.

[20] James H. Morris, Jr. Protection in programming languages. Communications of the ACM, 16(1):15–21, 1973.

[21] James H. Morris, Jr. Types are not sets. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 120–124, 1973.

[22] Roger Needham and Michael Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999, 1978.

[23] Benjamin C. Pierce and Eijiro Sumii. Relating cryptography and polymorphism, 2000. Draft.

http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/.

[24] Andrew M. Pitts. Existential types: Logical relations and operational equivalence. In Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 309–326. Springer-Verlag, 1998.

[25] Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321–359, 2000. Preliminary version appeared in HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science, vol. 10, 1998.

[26] Andrew M. Pitts and Ian Stark. Observable properties of higher order functions that dynamically create local names, or: what’s new? In Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, 1993.

[27] John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congres, pages 513–523, 1983.

[28] Andreas Rossberg. Generativity and dynamic opacity for abstract types. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 241–252, 2003.

[29] Davide Sangiorgi and Robin Milner. The problem of “weak bisimulation up to”. In CONCUR ’92, Third International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 32–46. Springer-Verlag, 1992.

[30] Peter Sewell. Modules, abstract types, and distributed versioning. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 236– 247, 2001.

[31] Ian Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, 1994.

http://homepages.inf.ed.ac.uk/stark/namhof.html.

[32] Eijiro Sumii and Benjamin C. Pierce. Logical relations for encryption. Journal of Computer Security, 11(4):521–554, 2003. Extended abstract appeared in 14th IEEE Computer Security Foundations Workshop, pp. 256–269, 2001.

[33] Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. Technical Report MS-CIS-04-27, Department of Computer and Information Science, University

of Pennsylvania, 2004. http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/. Extended abstract

appeared in Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 63–74, 2005.