Logical Relations for Encryption^{∗}

Eijiro Sumii^{†} University of Tokyo

          sumii@yl.is.s.u-tokyo.ac.jp

Benjamin C. Pierce University of Pennsylvania

                                          bcpierce@cis.upenn.edu

Abstract

The theory of relational parametricity and its logical relations proof technique are powerful tools for reasoning about information hiding in the polymorphic λ-calculus. We investigate the application of these tools in the security domain by defining a cryptographic λ-calculus—an extension of the standard simply typed λ-calculus with primitives for encryption, decryption, and key generation— and introducing syntactic logical relations (in the style of Pitts and Birkedal-Harper) for this calculus that can be used to prove behavioral equivalences between programs that use encryption.

We illustrate the framework by encoding some simple security protocols, including the Needham-Schroeder public-key protocol. We give a natural account of the well-known attack on the original protocol and a straightforward proof that the improved variant of the protocol is secure.

1 Introduction

Information hiding is a central concern in both programming languages and computer security. In the security community, encryption is the fundamental means of hiding information from outsiders. In programming languages, mechanisms such as abstract data types, modules, and parametric polymorphism play an analogous role. Each community has developed a rich set of mathematical tools for reasoning about the hiding of information in applications built using its chosen primitives. Given the intuitive similarity of the notions of hiding in the two domains, it is natural to wonder whether some of these techniques can be transferred from the programming language setting and applied to security problems, or vice versa.

As a first step in this direction, we investigate the application of one well established tool from the theory of programming languages—the concept of relational parametricity [33] and its accompanying logical relations proof method—in the domain of security protocols. (By logical relations, we mean syntactic ones [6, 28]—that is, relations over syntactic expressions in a term model—throughout this paper.)

We begin by defining a cryptographic λ-calculus, an extension of the ordinary simply typed λ-calculus with primitives for encryption, decryption, and key generation. One can imagine a large family of different cryptographic λ-calculi, each based on a different set of encryption primitives. For the present study, we use the simplest member of this family—the one where the primitives are assumed to provide perfect shared-key encryption. This calculus offers a suitable mix of structures for our investigation: encryption primitives, since our goal is to reason about programs from the security domain, together with the type structure on which logical relations are built. (Some issues raised by introducing static types into the calculus will be discussed in Section 5 along with the details of the type system.) We now proceed in three steps:

∗An extended abstract appeared in Proceedings of the 14th IEEE Computer Security Foundations Workshop, Keltic Lodge, Cape Breton, Nova Scotia, Canada, June 11-13, 2001.

†This work was carried out while the first author was visiting the University of Pennsylvania.

1. We show how some simple security protocols can be modeled by expressions in the cryptographic λ-calculus. The essence of the encoding lies in representing each principal by (a pair of) the next message value it sends and/or a function representing its response to the next message it receives. Our main example is the Needham-Schroeder public-key protocol [24]. The encoding of this protocol gives a clear account both of the well-known attack on the original protocol and of the resilience of the improved variant of this protocol to the same attack [17].

2. We formalize desired secrecy properties in terms of behavioral equivalence. Suppose, for instance, that we would like to prove that a program keeps some integer secret against all possible attacks. Let p_{i} be an instance of the program with the secret integer being i. If we encode each attacker as a function f that takes the program as an argument and returns an observable value (a boolean, say), then we want to show the equality f(p_{i}) = f(p_{j}) for i ≠ j. Since such a function is itself an expression in the cryptographic λ-calculus, we can use the same language to reason about the attacker and the program.

3. We introduce a proof technique for behavioral equivalence based on logical relations. The technique gives a method of “relating” (in a formal sense) two programs that differ only in their secrets and that behave equivalently in every observable respect. In particular, in its original form in the polymorphic λ-calculus, it gives a method of showing behavioral equivalence between different implementations of the same abstract type—so-called relational parametricity. We adapt the same ideas to the cryptographic λ-calculus, which enables us to prove the equivalence of p_{i} and p_{j} from the point of view of an arbitrary attacker f, without explicitly quantifying over all such attackers.

To illustrate these ideas, let us consider a simple system with two principals A and B sharing a secret key z, where A encrypts a secret integer i with z and sends it to B, and B replies by returning i mod 2. In the standard informal notation, this protocol can be written as:

\begin{aligned}1. & A → B & : & \{i\}_{z} \\ 2. & B → A & : & i mod 2 \end{aligned}

In the cryptographic λ-calculus, this system can be encoded as a pair p of the ciphertext {i}_{z}, which represents the principal A sending the integer i encrypted with z, and a function λ{x}_{z}. x mod 2 representing the principal B, which publishes x mod 2 on receiving an integer x encrypted by z. Let p_{i} be an instance of the program with the secret integer being i.

p_{i} = new z in ⟨{i}_{z}, λ{x}_{z}. x mod 2⟩

Here, the key generation construct new z in … guarantees that z is fresh, that is, different from any other keys and unknown to the attacker.

The network, scheduler, and attackers for this system are encoded as functions operating on this pair. We assume a standard model of “possible” attackers [8], who are able to intercept, forge, and forward messages, encrypt and decrypt them with any keys known to the attacker, and—in addition—schedule processes arbitrarily. (The last point is not usually emphasized, but is generally assumed by considering any possible scheduling when verifying protocols.) In short, it has full control of the network and process scheduler—or, to put it extremely, “the attacker is the network and scheduler.” Then, the properties to prove are: (i) the system accomplishes its goal under a “good” network/scheduler and (ii) the system does not leak its secret to any possible attacker.

The “good” network/scheduler for this system can be represented as a function f that takes a pair p as an argument and applies its second element #_{2}(p), which is a function representing a principal receiving a message, to its first element #_{1}(p), which is a value representing a principal sending the message.

f = λp. #_{2}(p)#_{1}(p)

The correctness of this network/scheduler can be checked by applying f to p, which yields i mod 2 as expected. (Of course, this network/scheduler is designed to work with this particular system only. It is also possible to encode a generic network/scheduler that will work with a range of protocols, by including the intended receiver’s name in each message and delivering messages accordingly.)

On the other hand, the property that the system keeps the concrete value of i secret against any possible attacker can be stated as a claim of behavioral equivalence between, say, p_{3} and p_{5}. That is, f(p_{3}) and f(p_{5}) give the same result for any function f returning an observable value.

Why is this? The point here is that p_{3} and p_{5} differ only in the concrete values of the secret integers and behave equivalently in every other respect. That is, the correspondence between values encrypted by a secret key—i.e., the integers 3 and 5 encrypted by the key z—is preserved by every part of both programs. Indeed, the first elements of the pairs are {3}_{z} and {5}_{z}, and the second elements of the pairs are functions that, given the arguments {3}_{z} and {5}_{z}, return the same value 1. Since the key z itself is kept secret, no other values can be encrypted by it.

Our logical relation formalizes and generalizes this argument. It demonstrates behavioral equivalence between two programs which differ only in the concrete values of their secrets, i.e., the values encrypted by secret keys. It is defined as follows:

• Two integers are related if and only if they are equal.

• Two pairs are related if and only if their elements are related.

• Two functions are related if and only if they return related values when applied to related arguments.

• Two values encrypted by a secret key k are related if and only if they are related by φ(k). Here, φ is a relation environment mapping each secret key to the relation between values encrypted by that key. Intuitively, it specifies what values are encrypted by each secret key (e.g., 3 and 5 are encrypted by z in the example above) and thereby keeps track of the correspondence between ciphertexts (e.g., between {3}_{z} and {5}_{z}).

The soundness theorem for the logical relation now tells us that, in order to prove behavioral equivalence of two programs, it suffices to find some φ such that the logical relation based on φ relates the programs we are interested in. For instance, in the example above, take φ(z) = {(3, 5)}. Then:

• The first elements of p_{3} and p_{5} are related by the definition of φ.

• The second elements of p_{3} and p_{5} are related since they return related values (i.e., 1) for any related arguments (i.e., {3}_{z} and {5}_{z}).

• Therefore, the pairs p_{3} and p_{5} are related since their elements are related.

e ::= i | int op_{n}(e_{1}, …, e_{n}) | x | λx. e | e_{1}e_{2} | ⟨e_{1}, …, e_{n}⟩ | #_{i}(e) |

in_{i}(e) | case e of in_{1}(x_{1}) ⇒ e_{1} [] … [] in_{n}(x_{n}) ⇒ e_{n} | k | new x in e | {e_{1}}_{e_{2}} | let {x}_{e_{1}} = e_{2} in e_{3} else e_{4}

Figure 1: Syntax

Thus, p_{3} and p_{5} are guaranteed to be behaviorally equivalent. In this way, the logical relation allows us to prove the behavioral equivalence of programs—which amounts to proving secrecy—in a compositional manner.

The contributions of this work are twofold: theoretically, it clarifies the intuitive similarity between two forms of information hiding in different domains, namely, encryption in security systems and type abstraction in programming languages; practically, it offers a method of proving behavioral equivalence (which implies secrecy) of programs that use encryption.

The rest of this paper is structured as follows. Section 2 presents the syntax and intuitive semantics of the cryptographic λ-calculus and Section 3 demonstrates its use in encoding cryptographic protocols through examples. Section 4 shows its operational semantics, Section 5 gives a simple type system—a prerequisite for formalizing the logical relations—and Section 6 defines our logical relation and its variants to cope with more complex cases (such as “keys encrypting other keys” in security protocols). Section 7 discusses related work, and Section 8 future work.

2 Syntax and Intuitive Semantics

The cryptographic λ-calculus extends a standard λ-calculus with keys, fresh key generation, encryption, and decryption primitives. The formal syntax of the calculus is given in Figure 1. int op_{n}(e_{1}, …, e_{n}) is the syntax of primitive operators for integer arithmetics like plus_{2}(e_{1}, e_{2}). (The subscript denotes the arity of each operator. This is necessary for the type system in Section 5.) We adopt infix notations such as e_{1} +e_{2} for binary operations. We use a tuple with no elements (i.e., n = 0) to represent a dummy value, written ⟨⟩. in_{i}( ) denotes the i-th injection (“tagging”) into a disjoint sum.

A key k is an element of the countably infinite set of keys K. The key generation form new x in e generates a fresh key, binds it to the variable x, and evaluates the expression e (in which x may appear free). For example, the program new x in new y in ⟨x, y⟩ generates two fresh keys and yields a pair of them. The encryption expression {e_{1}}_{e_{2}} encrypts the value obtained by evaluating the expression e_{1} with the key obtained by evaluating the expression e_{2}. The decryption form let {x}_{e_{1}} = e_{2} in e_{3} else e_{4} attempts to decrypt the ciphertext obtained by evaluating e_{2}, using the key obtained by evaluating e_{1}. If the decryption succeeds, it binds the plaintext thus obtained to the variable x and evaluates the expression e_{3}. If the decryption fails, it instead evaluates e_{4}. For example, the program let {x}_{k′} = {1}_{k} in x + 2 else 0 encrypts the integer 1 with the key k, tries to decrypt it with another key k′—which fails because the keys are different—and therefore gives 0. On the other hand, let {x}_{k} = {1}_{k} in x + 2 else 0 gives 3 because the decryption succeeds.

Several abbreviations are used in examples. We write true for in_{1}(⟨⟩), false for in_{2}(⟨⟩), and if e then e_{1} else e_{2} for case e of in_{1}( ) ⇒ e_{1} [] in_{2}( ) ⇒ e_{2}, respectively, to represent booleans as a disjoint sum of dummy values. We use option values Some(e), abbreviating in_{1}(e), and None, abbreviating in_{2}(⟨⟩), to represent the return values of functions that may or may not actually return a meaningful value because of errors such as decryption failure. Finally, we use the pattern matching function syntax λ{x}_{e_{1}}. e_{2} to abbreviate λy. let {x}_{e_{1}} = y in e_{2} elseNone (where y does not appear free in e_{1} and e_{2}), representing functions accepting arguments encrypted by a particular key only. For example, the function λ{x}_{k}. Some(x + 1) returns Some(i + 1) when applied to an integer i encrypted by the key k, and None for any ciphertext not encrypted by k.

Example 1. The expression λ{x}_{k}. Some(x mod 2), which is an abbreviation for λy. let {x}_{k} = y in in_{1}(x mod 2) else in_{2}(⟨⟩), represents a function f that accepts an integer x encrypted by the key k and returns its remainder when divided by 2, with the tag Some to denote success. For instance, the application f({3}_{k}) gives the result Some(1) while f({i}_{k′}) returns None for any i and any k′ ≠ k.

Example 2. Let p_{i} = new z in ⟨{i}_{z}, λ{x}_{z}. Some(x mod 2)⟩ and f = λp. #_{2}(p)#_{1}(p). Then, f(p_{i}) gives Some(i mod 2). This can be seen as a run of an encoding of the following simple system, in which two principals A and B share a key z (to be precise, a key bound to the variable z): first, A encrypts and sends i; then, B receives and decrypts it, and publishes its remainder when divided by 2. The function f plays the role of a “good” network and scheduler for this system.

Our cryptographic primitives directly model only shared-key encryption, but they can also be used to approximate public-key encryption: for any key k, the encryption function λx. {x}_{k} and decryption function λ{x}_{k}. Some(x) can be passed around and used as encryption and decryption keys.

This encoding is somewhat tricky and not quite faithful to the real world: not only we are again assuming perfect encryption and taking no account of any algebraic or probabilistic properties of individual cryptography, but also it would be silly, in reality, to give an attacker the code of a function that includes any secret key, which a real attacker could presumably discover by disassembling the function. In addition, our encoding limits the capability of attackers: for instance, they cannot test equality of public keys. Nevertheless, it suffices for our goal in this paper of giving an account of a few major “benchmark” examples. (In situations where this encoding does not suffice, we could try to reinforce it: for instance, in order to reason about a protocol in which equality of public keys is an essential issue, we could give an attacker a public key like λx. {x}_{k} along with a function like λe. let { }_{k} = e⟨⟩ in true else false to test whether another (encryption) key is equal to the previous one.)

3 Applications

Now we demonstrate the use of our framework on some larger examples, in which concurrent principals communicate with one another by using encryption. Although the cryptographic λcalculus has no built-in primitives for concurrency or communication, it can emulate a concurrent, communicating system by a reasonably straightforward encoding (recall the example in Section 1).

• The system as a whole is encoded as a tuple of the processes and their public keys (if any).

• An output process is encoded as the message itself.

• An input process is encoded as a function receiving a message.

• A network/scheduler/attacker for the system is encoded as a function that applies the input functions to the output messages in a certain order, possibly manipulating the messages using the keys that it knows.

Then, the following two properties are desired in general.

• Under a “correct” network and scheduler, i.e., a function applying appropriate messages to appropriate functions in some appropriate order, the program gives some correct result (soundness).

• Under any possible attacker, the program does not do anything “wrong” such as leaking a secret (safety).

More precise definitions of “correct” and “wrong” depend on the intention of each specific protocol, as we shall see below.

3.1 Encoding the Needham-Schroeder Public-Key Protocol

Consider the following system using the Needham-Schroeder public-key protocol [24] in a network with a server A, a client B, and an attacker E. (1) B sends its own name B to A. (2) A generates a fresh nonce N_{A}, pairs it with its own name A, encrypts it with B’s public key, and sends it to B.

(3) B generates a fresh key N_{B}, pairs it with N_{A}, encrypts it 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.

\begin{aligned}1. & B → A & : & B \\ 2. & A → B & : & \{N_{A}, A\}_{k_{B}} \\ 3. & B → A & : & \{N_{A}, N_{B}\}_{k_{A}} \\ 4. & A → B & : & \{N_{B}\}_{k_{B}} \\ 5. & B → A & : & \{i\}_{N_{B}} \end{aligned}

Let us encode this system as an expression of the cryptographic λ-calculus. (The result is necessarily somewhat complex, because several actions implicitly assumed in the informal definition above— such as checks on the identity of names and keys—are made explicit in the encoding process.)

Recall that we encode such a concurrent, communicating system as a tuple of the principals and the public keys. So we begin the encoding by generating the system’s keys and publishing their public portions, that is, A’s encryption key, B’s encryption key, and a key for E. (This key for E is necessary for encoding an attack to the protocol as we shall see soon, in which E is one of the clients of A and therefore A must know the key for E.)

                           new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E}, …, …⟩

Let us now encode B as the fourth element of the tuple. B starts by publishing its own name B, which we encode as a pair of B and a function representing B’s next action, which we’ll come back to in a moment. (We assume that names of principles are just integers—like IP addresses, for example—for the sake of simplicity.) The difference from the previous expression is underlined.

                         new z_{A} in new z_{B} in new z_{E} in

⟨λx. \{x\}_{z_{A}}, λx. \{x\}_{z_{B}}, z_{E}, \underline{⟨B, …⟩}, …⟩

Next, let us encode A as the fifth element of the tuple. A receives a name X, encrypts the pair of a freshly generated nonce N_{A} and its own name A with X’s key, and publishes it.

                          new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E}, ⟨B, …⟩,
\underline{λX. new N_{A} in ⟨\{⟨N_{A}, A⟩\}_{z_{x}}, …⟩}⟩

Here, z_{x} abbreviates if X = A then z_{A} else if X = B then z_{B} else z_{E}. The next action of B is to receive the pair of N_{A} and a name A′ encrypted by z_{B}, check that A′ = A, encrypt the pair of N_{A} and a freshly generated nonce N_{B} with z_{A}, and publish it:

                 new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E},
⟨B, \underline{λ\{⟨N_{A}, A⟩\}_{z_{B}}. new N_{B} in Some(⟨\{⟨N_{A}, N_{B}⟩\}_{z_{A}}, …⟩)}⟩,
λX. new N_{A} in ⟨{⟨N_{A}, A⟩}_{z_{x}}, …⟩⟩

Here, λ{⟨N_{A}, A⟩}_{z_{B}}…. abbreviates a “pattern matching” expression λy. let {p}_{z_{B}} = y in (if #_{2}(p) = A then (λN_{A}….)#_{1}(p) elseNone) elseNone. We will use similar abbreviations throughout this paper. Next, A receives the pair of a nonce N′_{A} and N_{B}, checks that N′_{A} = N_{A}, encrypts N_{B} with z_{B}, and publishes it:

                 new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E},
⟨B, λ{⟨N_{A}, A⟩}_{z_{B}}. new N_{B} in Some(⟨{⟨N_{A}, N_{B}⟩}_{z_{A}}, …⟩)⟩,
⟨λX. new N_{A} in ⟨{⟨N_{A}, A⟩}_{z_{x}},
\underline{λ\{N_{A}, N_{x}\}_{z_{A}}. Some(\{N_{x}\}_{z_{B}})}⟩⟩⟩

Last, B receives a nonce N′_{B} encrypted by z_{B}, checks that N′_{B} = N_{B}, encrypts i with N_{B}, and publishes it:

                   new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E},
⟨B, λ{⟨N_{A}, A⟩}_{z_{B}}. new N_{B} in
Some(⟨\{⟨N_{A}, N_{B}⟩\}_{z_{A}}, \underline{λ\{N_{B}\}_{z_{B}}. Some(\{i\}_{N_{B}})}⟩)⟩,
⟨λX. new N_{A} in ⟨{⟨N_{A}, A⟩}_{z_{x}},
λ{N_{A}, N_{x}}_{z_{A}}. Some({N_{x}}_{z_{x}})⟩⟩⟩

Let NS_{i} be the expression above.

A correct run of this system can be expressed by evaluation of this expression under the following function Good, which represents a “good” network/scheduler for this system.

λp. let ⟨B, c_{B}⟩ = #_{4}(p) in
let ⟨m_{1}, c_{A}⟩ = #_{5}(p)B in
let Some(⟨m_{2}, c′_{B}⟩) = c_{B}m_{1} in

                             let Some(m_{3}) = c_{A}m_{2} in

let Some(m_{4}) = c′_{B}m_{3} in

                             Some(m_{4})

Indeed, Good(NS_{i}) evaluates to Some({i}_{N_{B}}) for some fresh N_{B}, which means a successful execution of the system.

It is well known that a use of the Needham-Schroeder public-key protocol such as the system above—namely, letting the server A accept a request not only from the friendly client B but also from the malicious attacker E—is vulnerable to the following man-in-the-middle attack, which allows E to impersonate A while interacting with B [17]. The attack goes as follows. (1) B sends its own name B to A, but E intercepts it. (1′) E sends its own name E to A. (2′) A generates a fresh nonce N_{A}, pairs it with A, encrypts it with E’s public key, and sends it to E. (2) E encrypts the pair of N_{A} and A with B’s public key and sends it to B, pretending to be A. (3,3′) B generates a fresh nonce N_{B}, pairs it with N_{A}, encrypts it with A’s public key, and sends it to A. (4′) A encrypts N_{B} with E’s public key and sends it to E. (4) E encrypts N_{B} with B’s public key and sends it to B, pretending to be A. (5) B encrypts i with N_{B} and sends it to A, but E intercepts and decrypts it.

\begin{aligned}1. & B → E(A) & : & B \\ 1′. & E → A & : & E \\ 2′. & A → E & : & \{N_{A}, A\}_{k_{E}} \\ 2. & E(A) → B & : & \{N_{A}, A\}_{k_{B}} \\ 3, 3′. & B → A & : & \{N_{A}, N_{B}\}_{k_{A}} \\ 4′. & A → E & : & \{N_{B}\}_{k_{E}} \\ 4. & E(A) → B & : & \{N_{B}\}_{k_{B}} \\ 5. & B → E(A) & : & \{i\}_{N_{B}} \end{aligned}

This attack can be expressed in the cryptographic λ-calculus by the following function Evil.

λp. let ⟨B, c_{B}⟩ = #_{4}(p) in
let ⟨{⟨N_{A}, A⟩}_{#_{3}(p)}, c_{A}⟩ = #_{5}(p)E in
let Some(⟨m, c′_{B}⟩) = c_{B}(#_{2}(p)⟨N_{A}, A⟩) in
let Some({N_{B}}_{#_{3}(p)}) = c_{A}m in
let Some({i}_{N_{B}}) = c′_{B}(#_{2}(p)N_{B}) in

                        Some(i)

Evil(NS_{i}) indeed evaluates to Some(i), which leaks the secret. In other words, if i ≠ j, then Evil(NS_{i}) and Evil(NS_{j}) evaluate to different observable values, which shows that NS_{i} and NS_{j} are not behaviorally equivalent.

Of course, the example in this section is not the only use of the Needham-Schroeder protocol. Some uses are easy to reason about within our framework while others are not: e.g., it is straightforward to extend the example above with other clients besides just B (it suffices to duplicate the encoding of B, just replacing the name B with another), but changing the constant integer i to nonconstant data like new x in x leads to a challenge in even defining how to state the secrecy of such data. Indeed, this is the reason why we introduced the 5th message {i}_{N_{B}} into the protocol—so that we can state the secrecy of N_{B} via the secrecy of i.

3.2 Encoding the Improved Needham-Schroeder Public-Key Protocol

Consider the following variant of the system above, using an improved version of the Needham-Schroeder public-key protocol [17]. (The difference from the original version is underlined.) (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 it with B’s public key, and sends it to B. (3) B generates a fresh key N_{B}, tuples it with N_{A} \underline{and B}, encrypts it 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.

\begin{aligned}1. & B → A & : & B \\ 2. & A → B & : & \{N_{A}, A\}_{k_{B}} \\ 3. & B → A & : & \{N_{A}, N_{B}, \underline{B}\}_{k_{A}} \\ 4. & A → B & : & \{N_{B}\}_{k_{B}} \\ 5. & B → A & : & \{i\}_{N_{B}} \end{aligned}

Following the same lines as the encoding of the original system, this improved system can be encoded as follows.

                  new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E},
⟨B, λ{⟨N_{A}, A⟩}_{z_{B}}. new N_{B} in
Some(⟨\{⟨N_{A}, N_{B}, \underline{B}⟩\}_{z_{A}}, λ\{N_{B}\}_{z_{B}}. Some(\{i\}_{N_{B}})⟩)⟩,
⟨λX. new N_{A} in ⟨{⟨N_{A}, A⟩}_{z_{x}},
λ\{N_{A}, N_{x}, \underline{X}\}_{z_{A}}. Some(\{N_{x}\}_{z_{x}})⟩⟩⟩

Let NS′_{i} be the expression above.

How does this change prevent the attack? Recall that Evil was the following function.

λp. let ⟨B, c_{B}⟩ = #_{4}(p) in
let ⟨{⟨N_{A}, A⟩}_{#_{3}(p)}, c_{A}⟩ = #_{5}(p)E in
let Some(⟨m, c′_{B}⟩) = c_{B}(#_{2}(p)⟨N_{A}, A⟩) in
let Some({N_{B}}_{#_{3}(p)}) = c_{A}m in
let Some({i}_{N_{B}}) = c′_{B}(#_{2}(p)N_{B}) in

                        Some(i)

When the attacker forwards the message m = {⟨N_{A}, N_{B}, B⟩}_{z_{B}} (which is encrypted by B’s secret key and cannot be decrypted by the attacker) from B to A, A tries to match B against X = E, which fails. Thus, Evil(NS′_{i}) reduces to None for any i and fails to leak the secret. In Section 6, we formally prove this secrecy property with respect to all possible attackers using our logical relation.

3.3 Encoding the ffgg Protocol

The ffgg protocol [20] is an artificial protocol with an intentional flaw. It tries to communicate a secret name M in a rather strange manner. The point is that the protocol does keep the name secret as long as just one process runs for each principal, but fails to keep the secret only when more than one processes run for one of the principals! Although the cryptographic λ-calculus is sequential, it is actually expressive enough to encode this so-called “necessarily parallel attack” by interleaving.

To see this, let us encode the following exchange between two principals A and B using the ffgg protocol. (1) A sends its own name A to B. (2) B generates two fresh nonces N_{1} and N_{2} and sends them to A. (3) A tuples N_{1}, N_{2}, and some secret value M, encrypts them with a shared secret key k, and sends them to B. However, B does not check whether this N_{2} is equal to the previous one which B already knows, and just lets x be the second element of the tuple and y be the third. (4) B tuples x, y and N_{1}, encrypts them with k, and sends them to A with N_{1} and x.

\begin{aligned}1. & A → B & : & A \\ 2. & B → A & : & N_{1}, N_{2} \\ 3. & A → B & : & \{N_{1}, N_{2}, M\}_{k} as \{N_{1}, x, y\}_{k} \\ 4. & B → A & : & N_{1}, x, \{x, y, N_{1}\}_{k} \end{aligned}

This system can be encoded as the following expression ffgg_{M}.

                      new z in

⟨⟨A, λ⟨N_{1}, N_{2}⟩. {⟨N_{1}, N_{2}, M⟩}_{z}⟩,

                      λA. new N_{1} in new N_{2} in

⟨⟨N_{1}, N_{2}⟩, λ{N_{1}, x, y}_{z}. ⟨N_{1}, x, {⟨x, y, N_{1}⟩}_{z}⟩⟩⟩

The attack on this system is as follows. (1) A sends its own name A to B. (1′) Pretending to be A, the attacker E sends A to a parallel copy B′ of B. (2a) B generates two fresh nonces N_{1} and N_{2}, and send them to A, but E intercepts them. (2′) B′ generates other two fresh nonces N′_{1} and N′_{2}, and send them to A, but E again intercepts them. (2b) E sends N_{1} and N′_{1} to A, pretending to be B. (3) A tuples N_{1}, N′_{1} and M, encrypts them with k, and sends them to B. (4) B tuples N′_{1}, M and N_{1}, encrypts them with k, and send them to A with N_{1} and N′_{1}, but E intercepts them. (3′) E forwards the tuple of N′_{1}, M and N_{1} encrypted by k to B′, pretending to be A. (4′) B′ tuples M, N_{1} and N′_{1}, encrypts them with k, and send them to A with N′_{1} and M, but E intercepts them.

\begin{aligned}1. & A → B & : & A \\ 1′. & E(A) → B′ & : & A \\ 2a. & B → E(A) & : & N_{1}, N_{2} \\ 2′. & B′ → E(A) & : & N′_{1}, N′_{2} \\ 2b. & E(B) → A & : & N_{1}, N′_{1} \\ 3. & A → B & : & \{N_{1}, N′_{1}, M\}_{k} \\ 4. & B → E(A) & : & N_{1}, N′_{1}, \{N′_{1}, M, N_{1}\}_{k} \\ 3′. & E(A) → B′ & : & \{N′_{1}, M, N_{1}\}_{k} \\ 4′. & B′ → E(A) & : & N′_{1}, M, \{M, N_{1}, N′_{1}\}_{k} \end{aligned}

This attack can be encoded as the following function, which takes the expression above as a parameter p.

λp. let ⟨A, c_{A}⟩ = #_{1}(p) in
let ⟨⟨N_{1}, N_{2}⟩, c_{B}⟩ = #_{2}(p)A in
let ⟨⟨N′_{1}, N′_{2}⟩, c′_{B}⟩ = #_{2}(p)A in
let m = c_{A}⟨N_{1}, N′_{1}⟩ in
let ⟨N_{1}, N′_{1}, m′⟩ = c_{B}m in
let ⟨N′_{1}, M, m′′⟩ = c′_{B}m′ in

                             Some(M)

This function indeed reveals the secret value M in the expression ffgg_{M} above. Note that the function representing the principal B did not have to be replicated explicitly, because functions in λ-calculus can be applied any number of times. In this way, our framework can express the so-called “necessarily parallel attack” without any extra treatment.

By the way, in this encoding, there actually exists an even simpler function which leaks the secret.

λp. let ⟨A, c_{A}⟩ = #_{1}(p) in
let ⟨⟨N_{1}, N_{2}⟩, c_{B}⟩ = #_{2}(p)A in
let m = c_{A}⟨N_{1}, N_{2}⟩ in
let ⟨N_{1}, N_{2}, m′⟩ = c_{B}m in
let ⟨N_{2}, M, m′′⟩ = c_{B}m′ in

                             Some(M)

This attack is usually considered impossible in reality, because it applies the “continuation” function c_{B} twice, which means exploiting one state of (a process running for) the principal B more than once. This kind of false attacks could perhaps be excluded in our framework by using linear types for continuation functions like c_{B}. See Section 8 for details.

\begin{aligned}v & ::= & i | λx. e | ⟨v_{1}, …, v_{n}⟩ | in_{i}(v) | k | \{v\}_{k} \\ V & ::= & (s)v | Error \end{aligned}

\overline{(s)i ⇓ (s)i} \frac{(s_{0})e_{1} ⇓ (s_{1})i_{1} … (s_{n−1})e_{n} ⇓ (s_{n})i_{n} int op_{n}(i_{1}, …, i_{n}) = j}{(s_{0})int op_{n}(e_{1}, …, e_{n}) ⇓ (s_{n})j}
\overline{(s)λx. e ⇓ (s)λx. e} \frac{(s)e_{1} ⇓ (s_{1})λx. e (s_{1})e_{2} ⇓ (s_{2})v (s_{2})[v/x]e ⇓ V}{(s)e_{1}e_{2} ⇓ V}
\frac{(s_{0})e_{1} ⇓ (s_{1})v_{1} … (s_{n−1})e_{n} ⇓ (s_{n})v_{n}}{(s_{0})⟨e_{1}, …, e_{n}⟩ ⇓ (s_{n})⟨v_{1}, …, v_{n}⟩} \frac{(s)e ⇓ (s′)⟨…, v_{i}, …⟩}{(s)#_{i}(e) ⇓ (s′)v_{i}}
\frac{(s)e ⇓ (s′)v}{(s)in_{i}(e) ⇓ (s′)in_{i}(v)} \frac{(s)e ⇓ (s′)in_{i}(v) (s′)[v/x_{i}]e_{i} ⇓ V}{(s)case e of in_{1}(x_{1}) ⇒ e_{1} [] … [] in_{n}(x_{n}) ⇒ e_{n} ⇓ V}
\overline{(s)k ⇓ (s)k} \frac{(s ⊎ \{k\})[k/x]e ⇓ V}{(s)new x in e ⇓ V}  \frac{(s)e_{1} ⇓ (s_{1})v (s_{1})e_{2} ⇓ (s_{2})k}{(s)\{e_{1}\}_{e_{2}} ⇓ (s_{2})\{v\}_{k}}
\frac{\begin{matrix}(s)e_{1} ⇓ (s_{1})k_{1} (s_{1})e_{2} ⇓ (s_{2})\{v\}_{k_{2}} \\ (s_{2})[v/x]e_{3} ⇓ V k_{1} = k_{2} \end{matrix}}{(s)let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ V} \frac{\begin{matrix}(s)e_{1} ⇓ (s_{1})k_{1} (s_{1})e_{2} ⇓ (s_{2})\{v\}_{k_{2}} \\ (s_{2})e_{4} ⇓ V k_{1} ≠ k_{2} \end{matrix}}{(s)let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ V}
\frac{(s_{0})e_{1} ⇓ (s_{1})i_{1} … (s_{j−1})e_{j} ⇓ Error}{(s_{0})int op_{n}(e_{1}, …, e_{n}) ⇓ Error} \frac{(s_{0})e_{1} ⇓ (s_{1})v_{1} … (s_{n−1})e_{n} ⇓ (s_{n})v_{n} v_{i} is not of the form j for some 1 ≤ i ≤ n}{(s_{0})int op_{n}(e_{1}, …, e_{n}) ⇓ Error}
\frac{(s)e_{1} ⇓ Error}{(s)e_{1}e_{2} ⇓ Error} \frac{(s)e_{1} ⇓ (s_{1})v_{1} (s_{1})e_{2} ⇓ Error}{(s)e_{1}e_{2} ⇓ Error} \frac{(s)e_{1} ⇓ (s_{1})v_{1} (s_{1})e_{2} ⇓ (s_{2})v_{2} v_{1} is not of the form λx. e}{(s)e_{1}e_{2} ⇓ Error}
\frac{(s_{0})e_{1} ⇓ (s_{1})v_{1} … (s_{i−1})e_{i} ⇓ Error}{(s_{0})⟨e_{1}, …, e_{n}⟩ ⇓ Error} \frac{(s)e ⇓ Error}{(s)#_{i}(e) ⇓ Error} \frac{(s)e ⇓ (s′)v v is not of the form ⟨…, v_{i}, …⟩}{(s)#_{i}(e) ⇓ Error}
\frac{(s)e ⇓ Error}{(s)in_{i}(e) ⇓ Error} \frac{(s)e ⇓ Error}{(s)case e of in_{1}(x_{1}) ⇒ e_{1} [] … [] in_{n}(x_{n}) ⇒ e_{n} ⇓ Error}

\frac{(s)e ⇓ (s′)v v is not of the form in_{i}(v_{i}) for any 1 ≤ i ≤ n}{(s)case e of in_{1}(x_{1}) ⇒ e_{1} [] … [] in_{n}(x_{n}) ⇒ e_{n} ⇓ Error}

\frac{(s)e_{1} ⇓ Error}{(s)\{e_{1}\}_{e_{2}} ⇓ Error} \frac{(s)e_{1} ⇓ (s_{1})v (s_{1})e_{2} ⇓ Error}{(s)\{e_{1}\}_{e_{2}} ⇓ Error} \frac{(s)e_{1} ⇓ (s_{1})v_{1} (s_{1})e_{2} ⇓ (s_{2})v_{2} v_{2} is not of the form k}{(s)\{e_{1}\}_{e_{2}} ⇓ Error}
\frac{(s)e_{1} ⇓ Error}{(s)let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ Error} \frac{(s)e_{1} ⇓ (s_{1})v (s_{1})e_{2} ⇓ Error}{(s)let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ Error}
\frac{(s)e_{1} ⇓ (s_{1})v_{1} (s_{1})e_{2} ⇓ (s_{2})v_{2} v_{1} is not of the form k}{(s)let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ Error} \frac{(s)e_{1} ⇓ (s_{1})v_{1} (s_{1})e_{2} ⇓ (s_{2})v_{2} v_{2} is not of the form \{v\}_{k}}{(s)let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} ⇓ Error}

Figure 2: Semantics

4 Operational Semantics

In this section and the two that follow, we present the cryptographic λ-calculus, its type system, and the logical relations proof technique in detail.

The semantics of the calculus is defined by an evaluation relation mapping terms to results. For the ordinary λ-calculus, the evaluation relation has the form e ⇓ v, read “evaluation of the (closed) expression e yields the value v.” However, since the cryptographic λ-calculus includes a primitive for key generation, we need to represent “the set of keys generated so far” in some rigorous fashion. We do this by annotating the evaluation relation with a set s, representing the keys that have already been used when evaluation begins, and a set s′, representing the keys that have been used when evaluation finishes. To be precise, we define the relation (s)e ⇓ V where V is either of the form (s′)v or Error (signalling a run-time type error). We maintain the invariant that (s)e ⇓ (s′)v implies s ⊆ s′, that is, s′ \ s is the set of fresh keys generated during the evaluation of e. The evaluation relation is defined inductively by the rules in Figure 2.

Most of the evaluation rules are standard and straightforward; we explain just a few important points. In the rule for key generation, k is guaranteed to be “freshly generated” because s ⊎ {k} is defined and therefore k ∉ s. (Here, s ⊎ s′ is defined as s ∪ s′ when s ∩ s′ = ∅, and undefined otherwise.) This is the only rule that increases the set of keys. In the rules for decryption, we first evaluate e_{1} to obtain the decryption key k_{1}, then e_{2} is evaluated to obtain a ciphertext of the form {v}_{k_{2}}. If e_{1} does not evaluate to a key or e_{2} does not evaluate to a ciphertext, then a type error occurs. Otherwise, if the two keys match (k_{1} = k_{2}), the body e_{3} is evaluated, with x bound to the decrypted plaintext v. Otherwise, the else clause e_{4} is evaluated.

The following theorem and corollary state that the result of evaluating an expression is unique, modulo the names of freshly generated keys. (We write Keys(e) for the set of keys syntactically appearing in e.)

Theorem 3. Let s_{1} ⊇ Keys(e) and let θ be a one-to-one substitution from s_{1} to another set of keys s_{2}. If (s_{1})e ⇓ (s_{1} ⊎ s′_{1})v_{1} and (s_{2})θe ⇓ V, then V has the form (s_{2} ⊎ s′_{2})v_{2} and there exists some one-to-one substitution θ′ from s′_{1} to s′_{2} such that v_{2} = (θ ⊎ θ′)v_{1}.

Proof. See the Appendix. □

Corollary 4 (Uniqueness of Evaluation Result). Let s ⊇ Keys(e). If (s)e ⇓ (s⊎s′_{1})v_{1} and(s)e ⇓ V, then V has the form (s ⊎ s′_{2})v_{2} and there exists some one-to-one substitution θ′ from s′_{1} to s′_{2} such that v_{2} = θ′v_{1}.

Proof. Let s_{1} = s_{2} = s and θ = id in Theorem 3. □

5 Type System

In this section, we define a simple type system for the cryptographic λ-calculus. Types in this setting play not only the traditional role of guaranteeing the absence of run-time type errors (a well-typed term cannot evaluate to Error), but, more importantly, provide a framework for the reasoning method we consider in the next section, in which the fundamental definition of the logical relations proceeds by induction on types.

In addition to the values found in the ordinary λ-calculus, the cryptographic λ-calculus has keys and ciphertexts. Therefore, besides the usual arrow, product, and sum types of the simply typed λ-calculus, we introduce a key type key[τ], whose elements are keys that can be used to

τ ::= int | τ_{1} → τ_{2} | τ_{1} × ⋯ × τ_{n} | τ_{1} + ⋯ + τ_{n} | key[τ] | bits[τ]
\overline{Γ, Δ ⊢ i : int}(Const) \frac{Γ, Δ ⊢ e_{1} : int … Γ, Δ ⊢ e_{n} : int}{Γ, Δ ⊢ int op_{n}(e_{1}, …, e_{n}) : int} (Op)
\overline{Γ, Δ ⊢ x : Γ(x)}(Var) \frac{Γ ⊎ \{x ↦ τ_{1}\}, Δ ⊢ e : τ_{2}}{Γ, Δ ⊢ λx. e : τ_{1} → τ_{2}} (Abs) \frac{Γ, Δ ⊢ e_{1} : τ′ → τ Γ, Δ ⊢ e_{2} : τ′}{Γ, Δ ⊢ e_{1}e_{2} : τ} (App)
\frac{Γ, Δ ⊢ e_{1} : τ_{1} … Γ, Δ ⊢ e_{n} : τ_{n}}{Γ, Δ ⊢ ⟨e_{1}, …, e_{n}⟩ : τ_{1} × ⋯ × τ_{n}} (Pair) \frac{Γ, Δ ⊢ e : τ_{1} × ⋯ × τ_{i} × ⋯ × τ_{n}}{Γ, Δ ⊢ #_{i}(e) : τ_{i}} (Proj)
\frac{Γ, Δ ⊢ e : τ_{i}}{Γ, Δ ⊢ in_{i}(e) : τ_{1} + ⋯ + τ_{i} + ⋯ + τ_{n}} (In)
\frac{Γ, Δ ⊢ e : τ_{1} + ⋯ + τ_{n} Γ ⊎ \{x_{1} ↦ τ_{1}\}, Δ ⊢ e_{1} : τ … Γ ⊎ \{x_{n} ↦ τ_{n}\}, Δ ⊢ e_{n} : τ}{Γ, Δ ⊢ case e of in_{1}(x_{1}) ⇒ e_{1} [] … [] in_{n}(x_{n}) ⇒ e_{n} : τ} (Case)
Γ, Δ ⊢ k : key[Δ(k)] (Key) \frac{Γ ⊎ \{x ↦ key[τ′]\}, Δ ⊢ e : τ}{Γ, Δ ⊢ new x in e : τ} (New)
\frac{Γ, Δ ⊢ e_{1} : τ Γ, Δ ⊢ e_{2} : key[τ]}{Γ, Δ ⊢ \{e_{1}\}_{e_{2}} : bits[τ]} (Enc)
\frac{Γ, Δ ⊢ e_{1} : key[τ′] Γ, Δ ⊢ e_{2} : bits[τ′] Γ ⊎ \{x ↦ τ′\}, Δ ⊢ e_{3} : τ Γ, Δ ⊢ e_{4} : τ}{Γ, Δ ⊢ let \{x\}_{e_{1}} = e_{2} in e_{3} else e_{4} : τ} (Dec)

Figure 3: Type System encrypt values of type τ, and a ciphertext type bits[τ], whose elements are ciphertexts containing a plaintext value of type τ. Thus, keys of a given type cannot be used to encrypt values of different types, and ciphertexts of a given type cannot contain plaintext values of different types. This restriction is not particularly bothersome, since values of (finitely many) different types can always be injected into a common sum type. (Actually, in order to guarantee type safety, we do not need to annotate both key types and ciphertext types with their underlying plaintext types. However, doing so simplifies the definition of the logical relations in Section 6.)

The typing judgment has the form Γ, Δ ⊢ e : τ, read “under the type environment Γ for variables and the type environment Δ for keys, the expression e has the type τ, i.e., e evaluates to a value of type τ.” The typing rules (which are straightforward) are given in Figure 3. Here, f ⊎ f′ for two mappings f and f′ is defined as (f ⊎ f′)(x) = f(x) for x ∈ dom(f) and (f ⊎ f′)(y) = f′(y) for y ∈ dom(f′) if dom(f) ∩ dom(f′) = ∅, and undefined otherwise. Note that the type environment Δ for keys is used in the rule (Key) in the same way the type environment Γ for variables is used in the rule (Var). For the sake of readability, we often write bool for unit + unit and option[τ] for τ + unit, where unit is the type of a tuple with no elements.

In what follows, we often abbreviate a sequence of the form X_{1}, …, X_{n} as X̃ and a proposition of the form ⋀_{1≤j≤m} P (Y_{1j}, …, Y_{nj}) as P (Ỹ_{1}, …, Ỹ_{n}). For example, k̃ ∈ s̃ abbreviates (k_{1} ∈ s_{1}) ∧ … ∧ (k_{n} ∈ s_{n}).

The following theorem and corollary state that the evaluation of a well-typed program never causes a type error.

Theorem 5. Suppose Γ, Δ ⊢ e : τ and ∅, Δ ⊢ ṽ : τ̃ for Γ = {x̃ ↦ τ̃}. If (s)[ṽ/x̃]e ⇓ V for s = dom(Δ), then there exist some v and Δ′ such that V = (s ⊎ s′)v and ∅, Δ ⊎ Δ′ ⊢ v : τ for s′ = dom(Δ′).

Proof. See the Appendix. □

Corollary 6 (Type Safety). If ∅, ∅ ⊢ e : τ, then (∅)e ⇓̸ Error.

Proof. Immediate from Theorem 5. □

One subtle point deserves mention, concerning the relation between types and the modeling of security protocols. Since we intend to represent both principals and attackers as terms of the cryptographic λ-calculus, if we restrict our attention to only well-typed terms, we seem to run the risk of artificially (and unrealistically) restricting the power of the attackers we can model. In particular, since the calculus under this type system is strongly normalizing (i.e., every well-typed program terminates), the attackers are not Turing-complete. Moreover, there exists a specific kind of attacks—so-called “type attacks”—whose essence is to deceive principals into confusing values of different types.

Nevertheless, we believe that the present simple type system is flexible enough to allow typical attacks: indeed, all of the attacks we have seen so far are well-typed in the type system. As for type attacks, they are either (1) actually well-typed in the present type system, which does not distinguish nonces from keys, or (2) easily prevented using standard dynamic type checking techniques (see e.g. [12] for details).

6 Logical Relations for Encryption

Recall the family of expressions p_{i} from Example 2:

p_{i} = new z in ⟨{i}_{z}, λ{x}_{z}. Some(x mod 2)⟩

Suppose we want to argue that each p_{i} keeps its concrete value of i secret from any possible attacker. Intuitively, this is so because the only capabilities p_{i} provides to an attacker (at least, if that attacker can be represented as an expression of the cryptographic λ-calculus) are a ciphertext encrypting i under a key that the attacker cannot learn plus a function that will return just the least significant bit of a number encrypted with this key.

The intuition that the concrete value of i is kept secret can be formulated more precisely as a non-interference condition: for any i and j such that i mod 2 = j mod 2 (i.e., such that the part of the information that we do allow p_{i} and p_{j} to reveal is the same), we want to prove that p_{i} and p_{j} are behaviorally equivalent, in the following sense.

Definition 7 (Extensional Equivalence). We say that ⊢ e ≈ e′ : τ, pronounced “the expressions e and e′ are extensionally equivalent at type τ,” if and only if both of the following conditions hold:

• ∅, ∅ ⊢ e : τ and ∅, ∅ ⊢ e′ : τ

• For any f with ∅, ∅ ⊢ f : τ → bool, there exist some s and s′ such that one of the following conditions holds:

– (∅)fe ⇓ (s)true and (∅)fe′ ⇓ (s′)true

– (∅)fe ⇓ (s)false and (∅)fe′ ⇓ (s′)false

Essentially, this says that two expressions e and e′ yield the same result under any observer function f. Although this extensional equivalence is defined for closed expressions only, it can be used to prove the more general property of contextual equivalence for open expressions as follows. Take any expressions e and e′ of type τ and any context C[ ] of type bool with a hole of type τ. Let x̃ be the free variables of e and e′, and let f = λx_{0}. C[x_{0}x̃], e_{0} = λx̃. e, and e′_{0} = λx̃. e′. Then fe_{0} = fe′_{0} implies C[e] = C[e′]. Thus, contextual equivalence of e and e′ follows from extensional equivalence of e_{0} and e′_{0}.

In the following subsections, we define three variants of the logical relation proof technique for extensional equivalence. The first one shows the basic ideas, but it is not powerful enough to prove secrecy properties of realistic programs, such as (the encoding of) the improved Needham-Schroeder public-key protocol in Section 3. The others are extensions of the basic logical relation, the second for addressing the issue of “a key encrypting another key” (as in Needham-Schroeder) and the third for accommodating discrepancies in the number of keys used in the programs being compared.

6.1 Basic Logical Relation

Extensional equivalence is difficult to prove directly because it involves a quantification over all functions f of type τ → bool, which are infinitely many in general. Instead, we would like prove it in a compositional manner, by showing that each part of two programs behaves equivalently. However, this approach will not suffice to prove any interesting case of extensional equivalence if we do not consider the correspondence between ciphertexts. Consider, for example, the expressions e = new z in ⟨{true}_{z}, {false}_{z}, λ{x}_{z}. Some(x)⟩ and e′ = new z in ⟨{false}_{z}, {true}_{z}, λ{x}_{z}. Some(not(x))⟩. Although these tuples are equivalent, it cannot be shown that the third elements λ{x}_{z}. Some(x) and λ{x}_{z}. Some(not(x)) are “equivalent” in this context without knowing (1) the fact that (the key bound to) z is kept secret throughout the whole programs and (2) the relation between values encrypted by z, that is, {true}_{z} in e corresponds to {false}_{z} in e′ and {false}_{z} to {true}_{z}. (Recall the correspondence between {3}_{z} and {5}_{z} in the example in Section 1.)

φ ⊢_{s,s′}^{val} i ∼ i′ : int  ⟺ i = i′
φ ⊢_{s,s′}^{val} f ∼ f′ : τ_{1} → τ_{2}  ⟺ f = λx. e and f′ = λx. e′ for some x, e, e′ such that

φ ⊎ ψ ⊢_{s⊎t,s′⊎t′}^{exp} [v/x]e ∼ [v′/x]e′ : τ_{2} for any v, v′, t, t′, ψ such that φ ⊎ ψ ⊢_{s⊎t,s′⊎t′}^{val} v ∼ v′ : τ_{1} and dom(ψ) ⊆ t ∩ t′

φ ⊢_{s,s′}^{val} p ∼ p′ : τ_{1} × ⋯ × τ_{n} ⟺ p = ⟨v_{1}, …, v_{n}⟩ and p′ = ⟨v′_{1}, …, v′_{n}⟩ for some ṽ, ṽ′ such that

φ ⊢_{s,s′}^{val} ṽ ∼ ṽ′ : τ̃

φ ⊢_{s,s′}^{val} t ∼ t′ : τ_{1} + ⋯ + τ_{n} ⟺ t = in_{i}(v) and t′ = in_{i}(v′) for some i, v, v′ such that

φ ⊢_{s,s′}^{val} v ∼ v′ : τ_{i}

φ ⊢_{s,s′}^{val} k ∼ k′ : key[τ]  ⟺ k = k′ and k ∈ s ∩ s′ and k ∉ dom(φ)
φ ⊢_{s,s′}^{val} c ∼ c′ : bits[τ]  ⟺ c = {v}_{k} and c′ = {v′}_{k} for some v, v′, k such that either

k ∈ dom(φ) and k ∈ s ∩ s′ and (v, v′) ∈ φ(k), or else k ∉ dom(φ) and k ∈ s ∩ s′ and φ ⊢_{s,s′}^{val} v ∼ v′ : τ

φ ⊢_{s,s′}^{exp} e ∼ e′ : τ  ⟺ (s)e ⇓ (s ⊎ t)v and (s′)e′ ⇓ (s′ ⊎ t′)v′ for some t, v, t′, v′, ψ such that

φ ⊎ ψ ⊢_{s⊎t,s′⊎t′}^{val} v ∼ v′ : τ and dom(ψ) ⊆ t ∩ t′

Figure 4: Basic Logical Relation

Thus, we generalize ⊢ e ≈ e′ : τ to the logical relation φ ⊢ e ∼ e′ : τ, in which the parameter φ is a relation environment: a mapping from keys to relations, associating to each secret key k a relation φ(k) between the values that may be encrypted by k. Given φ, the family of relations φ ⊢ e ∼ e′ : τ is defined by induction on τ as follows:

• Two functions are related if and only if they map any related arguments to related results.

• Two pairs are related if and only if their corresponding elements are related.

• Two tagged values are related if and only if their tags are equal and their bodies are related.

• Two keys are related if and only if they are identical and not secret. Here, the set of secret keys is identified with the domain of φ (see below).

• Two ciphertexts {v}_{k} and {v′}_{k′} are related if and only if k = k′ and either:

– k is secret and (v, v′) ∈ φ(k), or else

– k is not secret and v and v′ are related.

Intuitively, φ ⊢ v ∼ v′ : τ means “under any possible attackers, the values v and v′ behave equivalently and furthermore preserve the invariant that values encrypted by any secret key k are related by φ(k).” It is this invariant which makes the logical relation work at all: as is often the case in inductive proofs, requiring this extra condition helps us in proving the final goal, i.e., extensional equivalence. Note that, in the definition above, secret keys are not related even if they are identical, because if they were related, an attacker would be able to encrypt arbitrary values under the keys and break the invariance. In other words, φ represents the restriction on the attackers’ knowledge that each k ∈ dom(φ) is unknown to them and, furthermore, for each (v, v′) ∈ φ(k), the ciphertexts {v}_{k} and {v′}_{k} are indistinguishable to the attackers. (See Section 8 for some discussion of the issue of equality for ciphertexts.)

As for expressions, arbitrary expressions are related if and only if they evaluate to values that, in turn, are related under a relation environment extended with the fresh keys that were generated during evaluation.

The formal definition of the logical relation is given in Figure 4. φ ⊢_{s,s′}^{val} v ∼ v′ : τ and φ ⊢_{s,s′}^{exp} e ∼ e′ : τ are logical relations for values and expressions, respectively. The sets s and s′, respectively, denote the keys generated so far in the left and right hand sides.

Strictly speaking, the relation environment φ should take s, s′ and a (partial) mapping Δ from keys to types as parameters. Then, for each k ∈ s ∩ s′, φ(k) is a relation on two values v, v′ of type Δ(k) such that Keys(v) ⊆ s and Keys(v′) ⊆ s′. In order to simplify the notations, however, we omit s, s′ and Δ since they are obvious from the context.

Example 8. For the e and e′ in the previous example, let τ = bits[bool] × bits[bool] × (bits [bool] → option[bool]). Then, ∅ ⊢_{∅,∅}^{exp} e ∼ e′ : τ. To prove this, let t = t′ = {k} and ψ = {k ↦ {(true, false), (false, true)}} in the definition of ∅ ⊢_{∅,∅}^{exp} e ∼ e′ : τ.

Example 9. For the p_{i} in Example 2, let τ = bits[int] × (bits[int] → option[int]). Then, ∅ ⊢_{∅,∅}^{exp} p_{i} ∼ p_{j} : τ for any i and j with i mod 2 = j mod 2. (Here, we define φ ⊢_{s,s′}^{val} i ∼ i′ : int ⟺ i = i′.) To prove this, let t = t′ = {k} and ψ(k) = {(i, j)} in the definition of ∅ ⊢_{∅,∅}^{exp} p_{i} ∼ p_{j} : τ.

The following theorem and corollary state that the logical relation indeed implies extensional equivalence.

Theorem 10. Let Γ, Δ ⊢ e : τ for Γ = {x̃ ↦ τ̃}, and suppose that φ ⊢_{s,s′}^{val} ṽ ∼ ṽ′ : τ̃ with dom(φ) ∩ dom(Δ) = ∅ and s, s′ ⊇ dom(φ) ⊎ dom(Δ). Then, φ ⊢_{s,s′}^{exp} [ṽ/x̃]e ∼ [ṽ′/x̃]e : τ. That is, any expression is related to itself when its free variables are substituted with related values.

Proof. See the Appendix. □

Corollary 11 (Soundness of Logical Relation). If ∅ ⊢_{∅,∅}^{exp} e ∼ e′ : τ, then ⊢ e ≈ e′ : τ.

Proof. See the Appendix. □

6.2 Extended Logical Relation

In the basic logical relation above, a relation between values encrypted by each secret key k is given by the relation environment φ. However, φ gives us no information about the relations that should be associated with fresh keys that are still to be generated in the future. As a result, the basic logical relation technique fails to prove the equivalence of some important examples that are, in fact, equivalent: in particular, we cannot prove the security of the improved version of the Needham-Schroeder public-key protocol from Section 3.2.

For a simpler example showing where the proof technique goes wrong, consider a program q_{i} = new x in ⟨λ . new y in {y}_{x}, λ{y′}_{x}. Some({i}_{y′})⟩ for some secret integer i. Since the key x (to be precise, the key bound to the variable x) is kept secret, the key y = y′ is also kept secret, so i is kept secret. Therefore, q_{3} and q_{5}, say, should be equivalent. But in order to prove this by using the basic logical relation above, we would have to give a relation between values encrypted by the key k bound to x. Since the key k′ that will be bound to y is not yet determined, we cannot specify a relation like φ(k) = {(k′, k′)}. Thus, q_{3} and q_{5} cannot be related.

This problem can be addressed by refining the definition of the logical relation a little, i.e., parameterizing the relation environment φ with respect to sets s and s′ of keys—representing the sets of keys that will have been generated at some point of interest in the future—as well as the relation environment ψ that will be in effect at that time. (The definition of “a relation environment parametrized by another relation environment” is recursive, but such entities can be constructed inductively, just as elements of a recursive type can be.) Then, in the example above, for instance, we can specify the needed relation as φ_{s,s′}^{ψ}(k) = {(k′, k′) | ψ_{t,t′}^{χ}(k′) = {(3, 5)} for any t, t′ and χ}. Accordingly, we extend the definition of the logical relation for ciphertext types to:

φ ⊢_{s,s′}^{val} c ∼ c′ : bits[τ] ⟺
c = {v}_{k} and c′ = {v′}_{k} for some v, v′, k such that either
k ∈ dom(φ) and k ∈ s ∩ s′ and (v, v′) ∈ φ_{s,s′}^{φ}(k), or else
k ∉ dom(φ) and k ∈ s ∩ s′ and φ ⊢_{s,s′}^{val} v ∼ v′ : τ

Interestingly, even after this extension, the propositions in Section 6.1 (and their proofs!) continue to hold without change—as long as we impose the condition that φ in φ_{s,s′}^{ψ}(k) is monotonic with respect to extension of s, s′, and ψ. Intuitively, this condition guarantees that values related once do not become unrelated as fresh keys are generated in the future. This is not the case if we take φ_{s,s′}^{ψ}(k) = {(k′, k′) | k′ ∉ s ∪ s′}, for example. The monotonicity condition excludes such anomalies. Formally, we require that each φ satisfies

φ_{s,s′}^{ψ}(k) ⊆ φ_{s⊎t,s′⊎t′}^{ψ⊎χ}(k)

for any s, s′, t and t′ with s ∩ t = ∅ and s′ ∩ t′ = ∅, and for any ψ and χ with dom(ψ) ⊆ s ∩ s′ and dom(χ) ⊆ t ∩ t′. Technically, this condition is needed in the proof of Lemma 20 (weakening of logical relation) when τ is a ciphertext type. We refer to this condition as “φ is monotonic.”

Example 12. For the previous q_{i}, let τ = (unit → bits[key[int]]) × (bits[key[int]] → option [bits[int]]). Then, ∅ ⊢_{∅,∅}^{exp} q_{i} ∼ q_{j} : τ for any i and j. To prove this, let t = t′ = {k} and

ψ_{s,s′}^{φ}(k) = {(k′, k′) | φ_{t,t′}^{χ}(k′) = {(i, j)} for any t, t′ and χ}

in the definition of ∅ ⊢_{∅,∅}^{exp} q_{i} ∼ q_{j} : τ. It is straightforward to check that ψ is monotonic. Hence ⊢ q_{i} ≈ q_{j} : τ.

Example 13. Let us see how to prove the correctness of the encoding in Section 3.2 of the improved Needham-Schroeder public-key protocol, using the extended logical relation.

First, in order for the encoding NS′_{i} to be well-typed at all, values encrypted by the keys z_{B} and z_{x} need to be tagged. (The tags are underlined.)

                new z_{A} in new z_{B} in new z_{E} in

⟨λx. {x}_{z_{A}}, λx. {x}_{z_{B}}, z_{E},
⟨B, λ\{\underline{in_{1}}(⟨N_{A}, A⟩)\}_{z_{B}}. new N_{B} in
Some(⟨\{⟨N_{A}, N_{B}, B⟩\}_{z_{A}}, λ\{\underline{in_{2}}(N_{B})\}_{z_{B}}. Some(\{i\}_{N_{B}})⟩)⟩,
⟨λX. new N_{A} in ⟨\{\underline{in_{1}}(⟨N_{A}, A⟩)\}_{z_{x}},
λ\{N_{A}, N_{x}, X\}_{z_{A}}. Some(\{\underline{in_{2}}(N_{x})\}_{z_{x}})⟩⟩⟩

Call this expression NS′′_{i}. It can be given the type

(τ_{1} → bits[τ_{1}]) × (τ_{2} → bits[τ_{2}]) × key[τ_{2}]×

                  (nam × (bits[τ_{2}] → option[bits[τ_{1}]×

                                  (bits[τ_{2}] → option[bits[int]])]))×

(nam → (bits[τ_{2}] × (bits[τ_{1}] → option[bits[τ_{2}]]))) where nam is actually just int and

                            τ_{1} = key[σ] × key[int] × nam
                            τ_{2} = key[σ] × nam + key[int]

for some σ. Call this type τ.

Now, NS′′_{i} and NS′′_{j} can be related (and are therefore extensionally equivalent) for any i and j by letting t = t′ = {k_{A}, k_{B}, k_{E}} and

ψ_{s,s′}^{φ}(k_{A}) = {(v, v′) | φ ⊢_{s,s′}^{val} v ∼ v′ : τ_{1}}
∪ {(⟨N_{A}, N_{B}, B⟩, ⟨N_{A}, N_{B}, B⟩) |
φ_{t,t′}^{χ}(N_{A}) = r and φ_{t,t′}^{χ}(N_{B}) = {i, j}
for any t, t′ and χ}
ψ_{s,s′}^{φ}(k_{B}) = {(v, v′) | φ ⊢_{s,s′}^{val} v ∼ v′ : τ_{2}}
∪ {(in_{1}(⟨N_{A}, A⟩), in_{1}(⟨N_{A}, A⟩)) |
φ_{t,t′}^{χ}(N_{A}) = r for any t, t′ and χ}
∪ {(in_{2}(N_{B}), in_{2}(N_{B})) |
φ_{t,t′}^{χ}(N_{B}) = {i, j} for any t, t′ and χ}

for some r in the definition of ∅ ⊢_{∅,∅}^{exp} NS′′_{i} ∼ NS′′_{j} : τ.

It is straightforward, by the way, to check that Good(NS′′_{i}) evaluates to Some({i}_{N_{B}}) for some fresh N_{B}. So this system is indeed both safe (from attacks that can be modeled in our setting) and sound.

6.3 Another Extended Logical Relation

Another way of extending the logical relation is to let a relation environment φ map a pair of secret keys—rather than one secret key—to a relation between values encrypted by those keys. Consider, for example, the following two expressions.

e = new x in ⟨{1}_{x}, {2}_{x},

                        λz. let {i}_{x} = z in Some(i mod 2) else None⟩

e′ = new x in new y in ⟨{3}_{x}, {4}_{y},

                        λz. let {i}_{x} = z in Some(i mod 2) else
                           let {j}_{y} = z in Some(j mod 2) else None⟩

They should be extensionally equivalent because, in both expressions, the keys x and y are kept secret, and therefore the only way to use the first and second elements of the tuples is to apply the third elements, which return the same value. However, this extensional equivalence cannot be proved by using either of the logical relations above, because the second elements are encrypted by different keys.

This problem can be solved by letting a relation environment φ take a pair of secret keys, like φ(k_{x}, k_{x}) = {(1, 3)} and φ(k_{x}, k_{y}) = {(2, 4)} for example, and extending the definition of the logical relation accordingly, letting

φ ⊢_{s,s′}^{val} c ∼ c′ : bits[τ] ⟺
c = {v}_{k} and c′ = {v′}_{k′} for some v, v′, k, k′ such that either
(k, k′) ∈ dom(φ) and (k, k′) ∈ s × s′ and (v, v′) ∈ φ(k), or else
(k, k′) ∉ dom(φ) and (k, k′) ∈ s × s′ and φ ⊢_{s,s′}^{val} v ∼ v′ : τ
φ ⊢_{s,s′}^{val} k ∼ k′ : key[τ] ⟺
k = k′ and (k, k) ∈ s × s′ and
(k, k′′) ∉ dom(φ) and (k′′, k) ∉ dom(φ) for any k′′

and so forth. Again, it is straightforward to adapt the results in Section 6.1 for this extension. (It may seem somewhat surprising that the results in Section 6.1 are so easily adapted to different definitions of logical relations. This stems from the fact that the proofs of the propositions do not actually depend on the internal structure of relation environments.)

7 Related Work

Numerous approaches to formal verification of security protocols have been explored in the literature [13, 18, 19, 21, etc.]. Of these, the spi-calculus [4] is one of the most powerful; it comes equipped with useful techniques such as bisimulation [3, 7] for proving behavioral equivalences and static typing for guaranteeing secrecy [1] and authenticity [11]. We are not in a position yet to claim that our approach is superior to the spi-calculus (or any other existing approach); rather, our goal has been simply to explore how standard techniques for reasoning about type abstraction can be adapted to the task of reasoning about encryption, in particular about security protocols. For this study, λ-calculus offers an attractive starting point, since it is in this setting that relational parametricity is best understood. Of course, the cost of this choice is that we depend on the ability of the λcalculus to encode communication and concurrency by function application and interleaving. Since this encoding is not fully abstract (processes are linear by default while functions are not), a process that is actually secure is not always encoded as a secure λ-term. Any attacks that we discover for the encoded term must be reality-checked against the original process (cf. the false attack on the encoding of the ffgg protocol in Section 3). However, if the encoding of a process can be proved secure, then the process itself should also be secure, at least against our notion of attackers (cf. the correctness proof of the improved Needham-Schroeder public-key protocol in Section 3 and the discussion in Section 8).

Formalizing and proving secrecy as non-interference—i.e., equivalence between instances of a program with different secret values—has been a popular approach both in the security community and in the programming language community. Non-interference reasoning in protocol verification can be found in [9, 34, 38], among others.

There have also been many proposals for using techniques from programming languages—in particular, static typing—to guarantee security of programs. For example, Heintze and Riecke [14] proposed λ-calculus with type-based information flow control, and proved a non-interference property—that a value of high security does not leak to any context of low security—using a logical relation. Other work in this line includes [15, 16, 31, 32, 35]. Most of those approaches aim to statically exclude attackers coming into a system, rather than to dynamically protect a program from attackers outside the system. An exception is the work cited above on static typing for secrecy and authenticity in spi-calculus.

Originally, logical relations were developed in the domain of denotational semantics for the purpose of establishing various kinds of correspondence in mathematical models of typed λ-calculi (see [22, Section 8], for example). In this setting, defining or using a logical relation requires establishing or understanding the denotational model(s) on which the logical relation is defined. In addition, the soundness of such relational reasoning (with respect to the operational semantics) depends on that of the denotational model. We circumvented these issues by adopting the approach of syntactic logical relations [6, 28], i.e., (a variant of) logical relations based on a term model of a language.

Since the cryptographic λ-calculus has a key generation primitive, we must be able to reason about generative names. For this purpose, we adapted Stark’s work on λ-calculus with name generation [36] in formulating both the semantics in Section 4 and the logical relation in Section 6.1. A technical difference of our adaptation from Stark’s original is that he introduced bijections while we rely on α-conversion in order to manage the possible differences between names generated by each of the related terms. In addition, the combination of the logical relation for name generation and that for type abstraction [33] gave rise to a new problem—namely, how to specify fresh keys that have not yet been generated. This issue is critical when a fresh key is encrypted by another key, which is often the case in programs exchanging keys. We addressed this problem in Section 6.2 by extending the logical relation in a non-trivial way. The same technique would also apply for other purposes such as treating “references to references” in establishing logical relations for ML-like references [30].

Harper and Lillibridge [personal communication, July 2000] have independently developed a typed seal calculus that is closely related to our cryptographic λ-calculus. Their work mainly focuses on encoding sealing [23] primitives in terms of other mechanisms such as exceptions and references and vice versa, rather than establishing techniques for reasoning about secrecy properties of programs using sealing.

8 Future Work

Completeness of Logical Relations. As a method of proving contextual equivalence, it is natural to wonder: can we generalize the logical relations in Section 6, so that the generalization becomes complete with respect to contextual equivalence? That is, can all contextually equivalent expressions be logically related? In general, however, it is rather difficult to obtain complete logical relations. Even for the polymorphic λ-calculus, the (syntactic) logical relation is incomplete [27] for existential types. (The original paper [27] attributes this to the presence of recursion, but a similar counter-example exists even without recursion [personal communication, June 2000].) Establishing a complete logical relation for encryption would first require more investigation of complete logical relations for type abstraction.

Primitive Values and Primitive Operations Besides its functional and cryptographic core, our calculus provides only integers and integer operations. It is straightforward to introduce other primitives such as booleans and strings in a similar way, i.e., by adding (1) expressions and values for the primitives, (2) evaluation rules mapping these expressions to values, (3) types for the primitive values and typing rules for the expressions, and (4) an equality relation between those primitive values as a base case of our logical relations.

It remains to see whether and how we can introduce more fundamental extensions such as public-key cryptography as primitives (cf. [2]).

Recursive Functions and Recursive Types. It can be shown (from Theorem 10 and the definition of φ ⊢_{s,s′}^{exp} e ∼ e′ : τ) that, under our simple type system, the evaluation of a well-typed expression always terminates. Therefore, recursive functions cannot be written. Indeed, introducing recursive functions breaks the soundness proof of the logical relations; introducing recursive types breaks the very definition of the logical relations. This problem is of concern because it suggests that our approach would not be sound with respect to attacks that rely on recursion. (If, indeed, there are any such attacks in reality: observe that, for each particular λ-term, if there exists an attack that uses recursion to reveal a secret within a finite amount of time, then the same attack should also be possible without using recursion.) We expect that this limitation can be removed by incorporating the theory of logical relation for λ-calculus with recursive functions and/or recursive types (e.g., [6]).

Equality for Ciphertexts. In our calculus, we did not introduce any construct to test ciphertexts for equality. This lack of equality for ciphertexts can be a weakness of our development in this paper for the same reason as the lack of recursion may be. For example, new x in {3}_{x} and new x in {5}_{x} are equivalent in our calculus, but an attacker may discover the difference just by comparing the ciphertexts as bit strings. Using non-deterministic encryption (a.k.a. random encryption and probabilistic encryption) for implementation does not solve this problem: for instance, ⟨{123}_{k}, {123}_{k}⟩ and let x = {123}_{k} in ⟨x, x⟩ would be inequivalent under non-deterministic encryption, but they are equivalent in the present calculus.

The issue of ciphertext equality is closely related to that of polymorphic equality in the standard theory of relational parametricity for type abstraction [39, Section 3.4]. The solution would also be similar—i.e., require the corresponding relation φ(k) to respect equality—but it remains to see what effects it will have on reasoning about information hiding by encryption.

State and Linearity. Although real programs often have some kind of state or linearity (in the sense of linear logic that some of the “resources” which they offer can be exploited only once), our framework does not take them into account. Thus, it cannot prove the security of a program depending on them.

For example, consider an expression p_{i} = new z in λx. let { }_{z} = x in in_{1}(i) else in_{2}(z) for some secret integer i. Although this program leaks the secret integer i under the attacker f = λp. let in_{2}(z) = p{0}_{k} in let in_{1}(i) = p{0}_{z} in Some(i), it is actually secure if we impose the constraint that the function λx. … is used linearly (i.e., applied only once). A similar example can be given using an ML-like reference cell.

Although we have not yet come across a realistic program whose security depends on its state or linearity in a crucial manner (maybe because such a “dangerous” design is avoided a priori by engineering practice?), we expect that this issue can be addressed, too, by incorporating the theory of logical relation for λ-calculus with state or linearity [5, 30].

Moreover, pursuing this direction of adapting logical relations for linearity and state might lead to a theory of relational parametricity for process calculi with some form of information hiding, such as polymorphic π-calculus [37] and spi-calculus [4]. We conjecture that, in combination with a big-step, evaluation semantics of process calculi [29], this approach might lead to a more systematic, structural method than the bisimulation-based techniques that have been explored in the past [7, 25] for proving equivalence between concurrent programs with information hiding.

Beyond Secrecy. We were able to prove secrecy properties of security protocols by means of logical relations because (1) our logical relations are a means of proving (contextual) equivalence and (2) equivalence leads to secrecy via non-interference. A natural question is whether we might be able to prove security properties other than secrecy—such as authenticity, anonymity, etc.—in a similar fashion via logical relations. The general idea would be to prove the equivalence between (encodings of) a real system and an ideal one whose “security” is obvious (cf. [10], for instance); further study is needed to see what kinds of problems can be addressed in this manner using our framework.

Type Abstraction via Encryption. While we have focused here on adapting the theory of type abstraction into encryption, it is also interesting to think of using the techniques of encryption for type abstraction. Specifically, it may be possible to implement type abstraction by means of encryption, in order to protect secrets not only from well-typed programs, but also from arbitrary attackers—in other words, to combine polymorphism with dynamic typing without losing type abstraction. That would enable us to write programs in a high-level language using type abstraction and translate them into a lower-level code using encryption. Then, the problem is whether and how such translation is possible, preserving the abstraction. In an earlier version of this work, we suggested one possibility for such a translation [26, Section 4], but proved nothing about it. The results in the present paper—in particular, the logical relations in Section 6—may help improve our understanding of this issue.

Acknowledgements

We would like to thank Martín Abadi, Naoki Kobayashi, the members of Akinori Yonezawa’s group in the University of Tokyo, the members of the Logic and Computation Seminar—especially Andre Scedrov—and the Programming Language Club at the University of Pennsylvania, as well as the anonymous CSFW and JCS reviewers, for useful advice on earlier versions of this work.

This work was supported by the National Science Foundation under NSF Career grant CCR-9701826 and by the Japan Society for the Promotion of Science.

References

[1] Martín Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749–786, 1999. Preliminary version appeared in Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Springer-Verlag, vol. 1281, pp. 611–638, 1997.

[2] 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.

[3] 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.

[4] 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.

[5] Gavin M. Bierman, Andrew M. Pitts, and Claudio V. Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Higher Order Operational Techniques in Semantics, volume 41 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2000.

[6] Lars Birkedal and Robert Harper. Relational interpretations of recursive types in an operational setting. Information and Computation, 155(1–2):3–63, 1999. Summary appeared in Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Springer-Verlag, vol. 1281, pp. 458–490, 1997.

[7] 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.

[8] Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983.

[9] Antonio Durante, Riccardo Focardi, and Roberto Gorrieri. CVS: A compiler for the analysis of cryptographic protocols. In 12th IEEE Computer Security Foundations Workshop, pages 203–212, 1999.

[10] Antonio Durante, Riccardo Focardi, and Roberto Gorrieri. A compiler for analysing cryptographic protocols using non-interference. ACM Transactions on Software Engineering and Methodology, 9(4):488–528, 2000.

[11] Andrew D. Gordon and Alan Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop, pages 145–159, 2001.

[12] James Heather, Gavin Lowe, and Steve Schneider. How to prevent type flaw attacks on security protocols. In 13th IEEE Computer Security Foundations Workshop, pages 255–268, 2000.

[13] Nevin Heintze and Edmund Clarke, editors. Workshop on Formal Methods and Security Pro-

tocols, 1999. http://cm.bell-labs.com/cm/cs/who/nch/fmsp99/.

[14] Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998.

[15] Matthew Hennessy and James Riely. Information flow vs. resource access in the asynchronous pi-calculus. In Automata, Languages and Programming, volume 1853 of Lecture Notes in Computer Science, pages 415–427. Springer-Verlag, 2000.

[16] Kohei Honda and Nobuko Yoshida. A uniform framework for secure information flow. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 81–92, 2002.

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

[18] Catherine Meadows. Formal verification of cryptographic protocols: A survey. In Advances in Cryptology – Asiacrypt ’94, volume 917 of Lecture Notes in Computer Science, pages 133–150. Springer-Verlag, 1995.

[19] Catherine Meadows. Open issues in formal methods for cryptographic protocol analysis. In DARPA Information Survivability Conference and Exposition, pages 237–250. IEEE Computer Society, 2000.

[20] Jonathan K. Millen. A necessarily parallel attack. In Workshop on Formal Methods and

Security Protocols, 1999. http://www.cs.bell-labs.com/who/nch/fmsp99/program.html.

[21] Jonathan K. Millen. CSFW home page. http://www2.csl.sri.com/csfw/, 2004.

[22] John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.

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

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

[25] Benjamin C. Pierce and Davide Sangiorgi. Behavioral equivalence in the polymorphic picalculus. Journal of the ACM, 47(3):531–586, 2000. Extended abstract appeared in Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 531–584.

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

http://www.cis.upenn.edu/~sumii/pub/.

[27] 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.

[28] 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.

[29] Andrew M. Pitts and Joshua R. X. Ross. Process calculus based upon evaluation to committed form. Theoretical Computer Science, 195:155–182, 1998. Preliminary version appeared in CONCUR’96: Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag, vol. 1119, pp. 18–33, 1996.

[30] Andrew M. Pitts and Ian Stark. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, pages 227–273. Cambridge University Press, 1998.

[31] François Pottier. A simple view of type-secure information flow in the π-calculus. In 15th IEEE Computer Security Foundations Workshop, pages 320–330, 2002.

[32] François Pottier and Vincent Simonet. Information flow inference for ML. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 319–330, 2002.

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

[34] Peter Y. A. Ryan and Steve A. Schneider. Process algebra and non-interference. In 12th IEEE Computer Security Foundations Workshop, pages 214–227, 1999.

[35] Geoffrey Smith and Dennis Volpano. Secure information flow in a multi-threaded imperative language. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 355–364, 1998.

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

    http://www.dcs.ed.ac.uk/home/stark/publications/thesis.html.

[37] David N. Turner. The Polymorphic Pi-calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1995.

[38] Dennis Volpano. Formalization and proof of secrecy properties. In 12th IEEE Computer Security Foundations Workshop, pages 92–95, 1999.

[39] Philip Wadler. Theorems for free! In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 347–359. ACM, 1989.

Appendix

For the sake of conciseness, we write R_{s,s′}^{val}(τ)φ and R_{s,s′}^{exp}(τ)φ, respectively, for the sets {(v, v′) | φ ⊢_{s,s′}^{val} v ∼ v′ : τ} and {(e, e′) | φ ⊢_{s,s′}^{exp} e ∼ e′ : τ}. That is, (v, v′) ∈ R_{s,s′}^{val}(τ)φ means φ ⊢_{s,s′}^{val} v ∼ v′ : τ and (e, e′) ∈ R_{s,s′}^{exp}(τ)φ means φ ⊢_{s,s′}^{exp} e ∼ e′ : τ.

In the proofs, we use the following lemmas.

Lemmas about Evaluation

Lemma 14 (Monotonic Increase of Key Set). If (s)e ⇓ (s′)v, then s ⊆ s′. If s ⊇ Keys(e) furthermore, then s′ ⊇ Keys(v).

Proof. By induction on the derivation of (s)e ⇓ (s′)v. □

Lemma 15 (Evaluation of Value). (s)v ⇓ (s)v for any s and v. In addition, if (s)v ⇓ V, then V = (s)v.

Proof. Immediately follows by induction on the structure of v. □

Lemma 16 (Weakening of Key Set). If (s)e ⇓ (s′)v, then (s ⊎ t)e ⇓ (s′ ⊎ t)v for any t with t ∩ s = ∅ and t ∩ s′ = ∅.

Proof. By induction on the derivation of (s)e ⇓ (s′)v. □

Lemmas about Typing

Lemma 17 (Weakening of Type Judgment). If Γ, Δ ⊢ e : τ, then Γ ⊎ Γ′, Δ ⊎ Δ′ ⊢ e : τ for any Γ′ and Δ′ with dom(Γ) ∩ dom(Γ′) = ∅ and dom(Δ) ∩ dom(Δ′) = ∅.

Proof. By induction on the derivation of Γ, Δ ⊢ e : τ. □

Lemma 18 (Substitution Lemma). Let Γ = {x̃ ↦ τ̃}. If Γ, Δ ⊢ e : τ and ∅, Δ ⊢ ṽ : τ̃, then Γ, Δ ⊢ [ṽ/x̃]e : τ.

Proof. By induction on the derivation of Γ, Δ ⊢ e : τ. We use Lemma 17 when the last rule used for the derivation is (Var). □

Lemmas about Logical Relation

Lemma 19 (Coincidence of Logical Relations). R_{s,s′}^{val}(τ)φ ⊆ R_{s,s′}^{exp}(τ)φ for any s, s′, τ, φ.

Proof. Immediately follows from the definition of R_{s,s′}^{exp}(τ)φ and from Lemma 15. □

Lemma 20 (Weakening of Logical Relation). Suppose s ∩ s_{0} = ∅ and s′ ∩ s′_{0} = ∅ where dom(φ) ⊆ s ∩ s′ and dom(φ_{0}) ⊆ s_{0} ∩ s′_{0}. Then, R_{s,s′}^{val}(τ)φ ⊆ R_{s⊎s_{0},s′⊎s′_{0}}^{val}(τ)(φ ⊎ φ_{0}) and R_{s,s′}^{exp} (τ)φ ⊆ R_{s⊎s_{0},s′⊎s′_{0}}^{exp}(τ)(φ ⊎ φ_{0}).

Proof. By induction on the structure of τ. In the proof of the latter half, note that, by Lemma 16, if (s)e ⇓ (s ⊎ t)v and (s′)e′ ⇓ (s′ ⊎ t′)v′, then (s ⊎ s_{0})e ⇓ (s ⊎ s_{0} ⊎ t)v and (s′ ⊎ s′_{0})e′ ⇓ (s′ ⊎ s′_{0} ⊎ t′)v′.

□

Proof of Theorem 3

By induction on the derivation of (s_{1})e ⇓ (s_{1} ⊎ s′_{1})v_{1}. The latter half of Lemma 14 is used when the last rule used for the derivation is either (1) the evaluation rule for function application or (2) the evaluation rule for decryption. □

Proof of Theorem 5

By induction on the derivation of (s)[ṽ/x̃]e ⇓ V. We perform case analysis on the form of e. We show the following four cases (the other cases are similar).

Case e = x. By (Var), x = x_{i} and τ = τ_{i} for some i. Thus, by Lemma 15, we have V = (s)v_{i}. So the theorem follows by letting v = v_{i} and Δ′ = ∅.

Case e = λx. e_{0}. By the evaluation rule for λ-abstraction, we have V = (s)λx. [ṽ/x̃]e_{0}. Meanwhile, by (Abs), τ is of the form σ_{1} → σ_{2} and we have Γ ⊎ {x ↦ σ_{1}}, Δ ⊢ e_{0} : σ_{2}. Therefore, by Lemma 18, we have Γ ⊎ {x ↦ σ_{1}}, Δ ⊢ [ṽ/x̃]e_{0} : σ_{2}. Then, by Lemma (Abs), we have Γ, Δ ⊢ λx. [ṽ/x̃]e_{0} : σ_{1} → σ_{2}. Thus, the theorem follows by letting v = λx. [ṽ/x̃]e_{0} and Δ′ = ∅.

Case e = new x in e_{0}. By the evaluation rule for key generation, we have (s⊎{k})[k/x][ṽ/x̃]e_{0} ⇓ V for some k. Meanwhile, by (Key), we have ∅, Δ⊎{k ↦ τ′} ⊢ k : key[τ′]. In addition, by Lemma 17, we have ∅, Δ⊎{k ↦ τ′} ⊢ ṽ : τ̃, Furthermore, by (New) we have Γ⊎{x ↦ key[τ′]}, Δ ⊢ e_{0} : τ, so by Lemma 17 we have Γ⊎{x ↦ key[τ′]}, Δ⊎{k ↦ τ′} ⊢ e_{0} : τ. Therefore, by the induction hypothesis, there exist some v′_{0} and Δ_{0} such that V = (s ⊎ {k} ⊎ s_{0})v′_{0} and ∅, Δ ⊎ {k ↦ τ′} ⊎ Δ_{0} ⊢ v′_{0} : τ for s_{0} = dom(Δ_{0}). Thus, the theorem follows by letting v = v′_{0} and Δ′ = {k ↦ τ′} ⊎ Δ_{0}.

Case e = (let {x}_{e_{1}} = e_{2} in e_{3} else e_{4}). By (Dec), we have Γ, Δ ⊢ e_{1} : key[τ′], Γ, Δ ⊢ e_{2} : bits [τ′], Γ ⊎ {x ↦ τ′}, Δ ⊢ e_{3} : τ, and Γ, Δ ⊢ e_{4} : τ for some τ′. In addition, by the evaluation rules for decryption, we have (s)[ṽ/x̃]e_{1} ⇓ V_{1} for some V_{1}. Therefore, by the induction hypothesis, there exist some v′_{1} and Δ_{1} such that V_{1} = (s ⊎ s_{1})v′_{1} and ∅, Δ ⊎ Δ_{1} ⊢ v′_{1} : key[τ′] for s_{1} = dom(Δ_{1}). Then, since v′_{1} is a value of a key type, v′_{1} is of the form k_{1} by (Key).

Furthermore, by the evaluation rules for decryption, we have (s ⊎ s_{1})[ṽ/x̃]e_{2} ⇓ V_{2} for some V_{2}. Meanwhile, by Lemma 17, we have Γ, Δ ⊎ Δ_{1} ⊢ e_{2} : bits[τ′]. Furthermore, by Lemma 17, we have ∅, Δ ⊎ Δ_{1} ⊢ ṽ : τ̃. Therefore, by the induction hypothesis, there exist some v′_{2} and Δ_{2} such that V_{2} = (s ⊎ s_{1} ⊎ s_{2})v′_{2} and ∅, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊢ v′_{2} : bits[τ′] for s_{2} = dom(Δ_{2}). Then, since v′_{2} is a value of a ciphertext type, v′_{2} is of the form {v′}_{k_{2}} and ∅, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊢ v′ : τ′ by (Enc).

Now we perform the following case analysis.

Sub-case k_{1} = k_{2}. Let k_{1} = k_{2} = k. By the evaluation rules for decryption, we have (s ⊎ s_{1} ⊎ s_{2})[v′/x][ṽ/x̃]e_{3} ⇓ V. In addition, by Lemma 17, we have Γ ⊎ {x ↦ τ′}, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊢ e_{3} : τ. Furthermore, by Lemma 17, we have ∅, Δ⊎Δ_{1} ⊎Δ_{2} ⊢ ṽ : τ̃. Therefore, by the induction hypothesis, there exist some v′_{3} and Δ_{3} such that V = (s ⊎ s_{1} ⊎ s_{2} ⊎ s_{3})v′_{3} and ∅, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊎ Δ_{3} ⊢ v′_{3} : τ for s_{3} = dom(Δ_{3}). Thus, the theorem follows by letting v = v′_{3} and Δ′ = Δ_{1} ⊎ Δ_{2} ⊎ Δ_{3}.

Sub-case k_{1} ≠ k_{2}. By the evaluation rules for decryption, we have (s ⊎ s_{1} ⊎ s_{2})[ṽ/x̃]e_{4} ⇓ V. In addition, by Lemma 17, we have Γ, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊢ e_{4} : τ. Furthermore, by Lemma 17, we have ∅, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊢ ṽ : τ̃. Therefore, by the induction hypothesis, there exist some v′_{4} and Δ_{4} such that V = (s ⊎ s_{1} ⊎ s_{2} ⊎ s_{4})v′_{4} and ∅, Δ ⊎ Δ_{1} ⊎ Δ_{2} ⊎ Δ_{4} ⊢ v′_{4} : τ for s_{4} = dom(Δ_{4}). Thus, the theorem follows by letting v = v′_{4} and Δ′ = Δ_{1} ⊎ Δ_{2} ⊎ Δ_{4}. □

Proof of Theorem 10

By induction on the structure of e. We perform case analysis on the form of e. We show the following four cases (the other cases are similar).

Case e = x. By (Var), we have x = x_{i} and τ = τ_{i} for some i. Thus, by Lemma 19, we have ([ṽ/x̃]e, [ṽ′/x̃]e) = (v_{i}, v′_{i}) ∈ R_{s,s′}^{val}(τ)φ ⊆ R_{s,s′}^{exp}(τ_{i})φ.

Case e = λx. e_{0}. By (Abs), τ is of the form σ_{1} → σ_{2} and we have Γ⊎{x ↦ σ_{1}}, Δ ⊢ e_{0} : σ_{2}. Assume (v, v′) ∈ R_{s⊎t,s′⊎t′}^{val}(σ_{1})(φ ⊎ ψ) with dom(ψ) ⊆ t ∩ t′. By Lemma 20, we have (ṽ, ṽ′) ∈ R_{s⊎t,s⊎t′}^{val}(τ̃) (φ ⊎ ψ). Therefore, by the induction hypothesis, we have ([v/x][ṽ/x̃]e_{0}, [v′/x][ṽ′/x̃]e_{0}) ∈ R_{s⊎t,s′⊎t′}^{exp} (σ_{2})φ⊎ψ. Thus, by the definition of R_{s,s′}^{val}(σ_{1} → σ_{2})φ and by Lemma 19, we have ([ṽ/x̃]e, [ṽ′/x̃]e) = (λx. [ṽ/x̃]e_{0}, λx. [ṽ′/x̃]e_{0}) ∈ R_{s,s′}^{val}(σ_{1} → σ_{2})φ ⊆ R_{s,s′}^{exp}(σ_{1} → σ_{2})φ = R_{s,s′}^{exp}(τ)φ.

Case e = new x in e_{0}. By (New), we have Γ ⊎ {x ↦ key[σ]}, Δ ⊢ e_{0} : τ for some σ. By Lemma 20, we have (ṽ, ṽ′) ∈ R_{s⊎{k},s′⊎{k}}^{val}(τ̃)φ for any k ∉ s ∪ s′. In addition, by the definition of R_{s⊎{k},s′⊎{k}}^{val}(key[σ])φ, we have (k, k) ∈ R_{s⊎{k},s′⊎{k}}^{val}(key[σ])φ. Therefore, by the induction hypothesis, we have ([k/x][ṽ/x̃]e_{0}, [k/x][ṽ′/x̃]e_{0}) ∈ R_{s⊎{k},s′⊎{k}}^{exp}(τ)φ. Thus, by the definition of R_{s⊎{k},s′⊎{k}}^{exp}(τ)φ, there exist some t_{0}, w_{0}, t′_{0}, w′_{0}, and ψ_{0} with dom(ψ_{0}) ⊆ t_{0} ∩ t′_{0} such that (s ⊎ {k})[k/x][ṽ/x̃]e_{0} ⇓ (s ⊎ {k} ⊎ t_{0})w_{0}, (s′ ⊎ {k})[k/x][ṽ′/x̃]e_{0} ⇓ (s′ ⊎ {k} ⊎ t′_{0})w′_{0}, and (w_{0}, w′_{0}) ∈ R_{s⊎{k}⊎t_{0},s′⊎{k}⊎t′_{0}}^{val}(τ)(φ ⊎ ψ_{0}). Then, by the evaluation rule for key generation, we have (s)new x in [ṽ/x̃]e_{0} ⇓ (s ⊎ {k} ⊎ t_{0})w_{0} and (s′)new x in [ṽ′/x̃]e_{0} ⇓ (s′ ⊎ {k} ⊎ t′_{0})w′_{0}. Thus, by letting t = {k} ⊎ t_{0}, v = w_{0}, t′ = {k} ⊎ t′_{0}, v′ = w′_{0}, and ψ = ψ_{0} in the definition of R_{s,s′}^{exp}(τ)φ, we have ([ṽ/x̃]e, [ṽ′/x̃]e) = (new x in [ṽ/x̃]e_{0}, new x in [ṽ′/x̃]e_{0}) ∈ R_{s,s′}^{exp}(τ)φ.

Case e = (let {x}_{e_{1}} = e_{2} in e_{3} else e_{4}). By (Dec), we have Γ, Δ ⊢ e_{1} : key[σ], Γ, Δ ⊢ e_{2} : bits[σ], Γ ⊎ {x ↦ σ}, Δ ⊢ e_{3} : τ, and Γ, Δ ⊢ e_{4} : τ for some σ. Then, by the induction hypothesis, we have ([ṽ/x̃]e_{1}, [ṽ′/x̃]e_{1}) ∈ R_{s,s′}^{exp}(key[σ])φ. Thus, by the definition of R_{s,s′}^{exp}(key[σ])φ, there exist some t_{1}, w_{1}, t′_{1}, w′_{1}, and ψ_{1} with dom(ψ_{1}) ⊆ t_{1} ∩t′_{1} such that (s)[ṽ/x̃]e_{1} ⇓ (s⊎t_{1})w_{1}, (s′)[ṽ′/x̃]e_{1} ⇓ (s′ ⊎t′_{1})w′_{1}, and (w_{1}, w′_{1}) ∈ R_{s⊎t_{1},s′⊎t′_{1}}^{val}(key[σ])(φ ⊎ ψ_{1}). Then, by the definition of R_{s⊎t_{1},s′⊎t′_{1}}^{val}(key[σ])(φ ⊎ ψ_{1}), we have w_{1} = w′_{1} is of the form k_{1} where k_{1} ∈ (s ⊎ t_{1}) ∩ (s′ ⊎ t′_{1}) and k_{1} ∉ dom(φ ⊎ ψ_{1}).

Furthermore, by the induction hypothesis, we have ([ṽ/x̃]e_{2}, [ṽ′/x̃]e_{2}) ∈ R_{s⊎t_{1},s′⊎t′_{1}}^{exp}(bits[σ]) (φ ⊎ ψ_{1}). Thus, by the definition of R_{s⊎t_{1},s′⊎t′_{1}}^{exp}(bits[σ])(φ ⊎ ψ_{1}), there exist some t_{2}, w_{2}, t′_{2}, w′_{2}, and ψ_{2} with dom(ψ_{2}) ⊆ t_{2} ∩ t′_{2} such that (s ⊎ t_{1})[ṽ/x̃]e_{2} ⇓ (s ⊎ t_{1} ⊎ t_{2})w_{2}, (s′ ⊎ t′_{1})[ṽ′/x̃]e_{2} ⇓ (s′ ⊎ t′_{1} ⊎ t′_{2})w′_{2}, and (w_{2}, w′_{2}) ∈ R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{val}(bits[σ])(φ ⊎ ψ_{1} ⊎ ψ_{2}). Then, by the definition of R_{s⊎t_{1}⊎t_{2},s⊎t′_{1}⊎t′_{2}}^{val}(bits[σ])(φ ⊎ ψ_{1} ⊎ ψ_{2}), w_{2} and w′_{2} are respectively of the form {w}_{k_{2}} and {w′}_{k_{2}} where k_{2} ∈ (s ⊎ t_{1} ⊎ t_{2}) ∩ (s′ ⊎ t′_{1} ⊎ t′_{2}).

Now we perform the following case analysis.

Sub-case k_{1} = k_{2}. Since k_{1} ∉ dom(φ⊎ψ_{1} ⊎ψ_{2}), we have (w, w′) ∈ R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{val}(σ)(φ⊎ψ_{1} ⊎ψ_{2}). In addition, by Lemma 20, we have (ṽ, ṽ′) ∈ R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{val}(τ̃)(φ⊎ψ_{1}⊎ψ_{2}). Then, by the induction hypothesis, we have ([w/x][ṽ/x̃]e_{3}, [w′/x][ṽ′/x̃]e_{3}) ∈ R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{exp}(τ)(φ ⊎ ψ_{1} ⊎ ψ_{2}). Thus, by the definition of R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{exp}(τ)(φ⊎ψ_{1} ⊎ψ_{2}), there exist some t_{3}, w_{3}, t′_{3}, w′_{3}, and ψ_{3} with dom(ψ_{3}) ⊆ t_{3} ∩ t′_{3} such that (s ⊎ t_{1} ⊎ t_{2})[w/x][ṽ/x̃]e_{3} ⇓ (s ⊎ t_{1} ⊎ t_{2} ⊎ t_{3})w_{3}, (s′ ⊎ t′_{1} ⊎ t′_{2})[w′/x][ṽ′/x̃]e_{3} ⇓ (s′ ⊎ t′_{1} ⊎ t′_{2} ⊎ t′_{3})w′_{3}, and (w_{3}, w′_{3}) ∈ R_{s⊎t_{1}⊎t_{2}⊎t_{3},s′⊎t′_{1}⊎t′_{2}⊎t′_{3}}^{val}(τ)(φ ⊎ ψ_{1} ⊎ ψ_{2} ⊎ ψ_{3}). Therefore, by the evaluation rules for decryption, (s)let {x}_{[ṽ/x̃]e_{1}} = [ṽ/x̃]e_{2} in [ṽ/x̃]e_{3} else [ṽ/x̃]e_{4} ⇓ (s ⊎ t_{1} ⊎ t_{2} ⊎ t_{3})w_{3} and (s′)let {x}_{[ṽ′/x̃]e_{1}} = [ṽ′/x̃]e_{2} in [ṽ′/x̃]e_{3} else [ṽ′/x̃]e_{4} ⇓ (s′ ⊎ t′_{1} ⊎ t′_{2} ⊎ t′_{3})w′_{3}. Thus, by letting t = t_{1} ⊎ t_{2} ⊎ t_{3}, v = w_{3}, t′ = t′_{1} ⊎ t′_{2} ⊎ t′_{3}, v′ = w′_{3}, and ψ = ψ_{1} ⊎ ψ_{2} ⊎ ψ_{3} in the definition of R_{s,s′}^{exp} (τ)φ, we have ([ṽ/x̃]e, [ṽ′/x̃]e) = (let {x}_{[ṽ/x̃]e_{1}} = [ṽ/x̃]e_{2} in [ṽ/x̃]e_{3} else [ṽ/x̃]e_{4}, let {x}_{[ṽ′/x̃]e_{1}} = [ṽ′/x̃]e_{2} in [ṽ′/x̃]e_{3} else [ṽ′/x̃]e_{4}) ∈ R_{s,s′}^{exp}(τ)φ.

Sub-case k_{1} ≠ k_{2}. By Lemma 20, we have (ṽ, ṽ′) ∈ R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{val}(τ̃)(φ ⊎ ψ_{1} ⊎ ψ_{2}). Then, by the induction hypothesis, we have ([ṽ/x̃]e_{4}, [ṽ′/x̃]e_{4}) ∈ R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{exp}(τ)(φ ⊎ ψ_{1} ⊎ ψ_{2}). Thus, by the definition of R_{s⊎t_{1}⊎t_{2},s′⊎t′_{1}⊎t′_{2}}^{exp}(τ)(φ⊎ψ_{1} ⊎ψ_{2}), there exist some t_{4}, w_{4}, t′_{4}, w′_{4}, and ψ_{4} with dom(ψ_{4}) ⊆ t_{4} ∩ t′_{4} such that (s ⊎ t_{1} ⊎ t_{2})[ṽ/x̃]e_{4} ⇓ (s ⊎ t_{1} ⊎ t_{2} ⊎ t_{4})w_{4}, (s′ ⊎ t′_{1} ⊎ t′_{2})[ṽ′/x̃]e_{4} ⇓ (s′ ⊎ t′_{1} ⊎ t′_{2} ⊎ t′_{4})w′_{4} and (w_{4}, w′_{4}) ∈ R_{s⊎t_{1}⊎t_{2}⊎t_{4},s′⊎t′_{1}⊎t′_{2}⊎t′_{4}}^{val}(τ)(φ ⊎ ψ_{1} ⊎ ψ_{2} ⊎ ψ_{4}). Therefore, by the evaluation rules for decryption, we have (s)let {x}_{[ṽ/x̃]e_{1}} = [ṽ/x̃]e_{2} in [ṽ/x̃]e_{4} else [ṽ/x̃]e_{4} ⇓ (s ⊎ t_{1} ⊎ t_{2} ⊎ t_{4})w_{4} and (s′)let {x}_{[ṽ′/x̃]e_{1}} = [ṽ′/x̃]e_{2} in [ṽ′/x̃]e_{4} else [ṽ′/x̃]e_{4} ⇓ (s ⊎ t′_{1} ⊎ t′_{2} ⊎ t′_{4})w′_{4}. Thus, by letting t = t_{1} ⊎ t_{2} ⊎ t_{4}, v = w_{4}, t′ = t′_{1} ⊎ t′_{2} ⊎ t′_{4}, v′ = w′_{4}, and ψ = ψ_{1} ⊎ ψ_{2} ⊎ ψ_{4} in the definition of R_{s,s′}^{exp} (τ)φ, we have ([ṽ/x̃]e, [ṽ′/x̃]e) = (let {x}_{[ṽ/x̃]e_{1}} = [ṽ/x̃]e_{2} in [ṽ/x̃]e_{4} else [ṽ/x̃]e_{4}, let {x}_{[ṽ′/x̃]e_{1}} = [ṽ′/x̃]e_{2} in [ṽ′/x̃]e_{4} else [ṽ′/x̃]e_{4}) ∈ R_{s,s′}^{exp}(τ)φ. □

Proof of Corollary 11

By Theorem 10, we have (f, f) ∈ R_{∅,∅}^{exp}(τ → bool)∅ for any f with ∅, ∅ ⊢ f : τ → bool. Then, by the definition of R_{∅,∅}^{exp}(τ → bool)∅, there exist some s, w, s′, w′, φ with dom(φ) ⊆ s ∩ s′ such that (∅)f ⇓ (s)w, (∅)f ⇓ (s′)w′, and (w, w′) ∈ R_{s,s′}^{val}(τ → bool)φ. Then, by the definition of R_{s,s′}^{val}(τ → bool)φ, w and w′ are respectively of the form λx. e_{0} and λx. e′_{0} where ([v/x]e_{0}, [v′/x]e′_{0}) ∈ R_{s⊎t,s′⊎t′}^{exp} (bool)(φ ⊎ ψ) for any v, v′, t, t′, ψ with dom(ψ) ⊆ t ∩ t′ such that (v, v′) ∈ R_{s⊎t,s′⊎t′}^{val}(τ)(φ ⊎ ψ).

Meanwhile, by Lemma 20, we have (e, e′) ∈ R_{s,s′}^{exp}(τ)φ. Then, by the definition of R_{s,s′}^{exp}(τ)φ, there exist some t, v, t′, v′, ψ with dom(ψ) ⊆ t ∩ t′ such that (s)e ⇓ (s ⊎ t)v, (s′)e′ ⇓ (s′ ⊎ t′)v′, and (v, v′) ∈ R_{s⊎t,s′⊎t′}^{val}(τ)(φ ⊎ ψ).

Therefore, ([v/x]e_{0}, [v′/x]e′_{0}) ∈ R_{s⊎t,s′⊎t′}^{exp}(bool)(φ ⊎ ψ). Then, by the definition of R_{s⊎t,s′⊎t′}^{exp} (bool)(φ ⊎ ψ), there exist some s_{0}, w_{0}, s′_{0}, w′_{0}, φ_{0} with dom(φ_{0}) ⊆ s_{0} ∩ s′_{0} such that (s ⊎ t)[v/x]e_{0} ⇓ (s⊎t⊎s_{0})w_{0}, (s′⊎t′)[v′/x]e′_{0} ⇓ (s′⊎t′⊎s′_{0})w_{0}, and (w_{0}, w′_{0}) ∈ R_{s⊎t⊎s_{0},s′⊎t′⊎s′_{0}}^{val}(bool)(φ⊎ψ⊎φ_{0}). Then, by the definition of R_{s⊎t⊎s_{0},s′⊎t′⊎s′_{0}}^{val}(bool)(φ⊎ψ⊎φ_{0}), we have w_{0} = w′_{0} = true or w_{0} = w′_{0} = false.

By the way, by the evaluation rules for function application, we have (∅)fe ⇓ (s ⊎ t ⊎ s_{0})w_{0} and (∅)fe′ ⇓ (s′ ⊎ t′ ⊎ s′_{0})w′_{0}. Thus, by Definition 7, we have ⊢ e ≈ e′ : τ. □