Relating Cryptography and Polymorphism

Benjamin Pierce^{∗} Eijiro Sumii^{†} University of Pennsylvania

July 16, 2000^{‡}

Abstract

Cryptography is information hiding. Polymorphism is also information hiding. So is cryptography polymorphic? Is polymorphism cryptographic?

To investigate these questions, we define the cryptographic λ-calculus, a simply typed λcalculus with shared-key cryptographic primitives. Although this calculus is simply typed, it is powerful enough to encode recursive functions, recursive types, and dynamic typing. We then develop a theory of relational parametricity for our calculus as Reynolds did for the polymorphic λ-calculus. This theory is useful for proving equivalences in our calculus; for instance, it implies a non-interference property: values encrypted by a key cannot be distinguished from one another by any function ignorant of the key. We close with an encoding of the polymorphic λ-calculus into the cryptographic calculus that uses cryptography to protect type abstraction.

Our results shed a new light upon the relationship between cryptography and polymorphism, and offer a first step toward extending programming idioms based on type abstraction (such as modules and packages) from the civilized world of polymorphism, where only well-typed programs are allowed, to the unstructured world of cryptography, where friendly programs must cohabit with malicious attackers.

1 Introduction

Information hiding is a crucial concept in programming. It is essential not only for modularity but also for security of programs. Type abstraction and encryption are common approaches to information hiding.

Type abstraction forbids illegal access to secret data by concealing the type of the data. For example, consider the following package, which provides a list ints of secret integers and a function isdiv to test whether one of the secret integers is divisible by another.

pack int, {ints = [1, 2, 3], isdiv = λi. λj. (i mod j = 0)}
as ∃α. {ints : α list, isdiv : α → α → bool}

This achieves the security by concealing the type int of the data 1, 2, and 3. The typing rules for existential types [17] guarantee that users of the package must treat the type abstractly.

∗bcpierce@cis.upenn.edu †sumii@saul.cis.upenn.edu. Visiting scholar from the University of Tokyo. Research fellow of the Japan Society for the Promotion of Science.

‡Last revised on October 6, 2000

On the other hand, encryption prevents illegal access to secret data by obfuscating the value of the data, for example as follows. (The terms ⌊—⌋_{k} and ⌈—⌉_{k} denote encryption and decryption, respectively, under the key k.)

let k = generate fresh key() in

{ints = [⌊1⌋_{k}, ⌊2⌋_{k}, ⌊3⌋_{k}], isdiv = λx. λy. (⌈x⌉_{k} mod ⌈y⌉_{k} = 0)}

Type abstraction is static and high-level: a potential violation of secrecy causes a type error before execution, as long as the whole program (including the “attacker”) abides by the type system. This leads to a powerful method of reasoning about type abstraction, known as parametricity [24]. The principle of parametricity assures us that “related” programs are equivalent, in the sense that they are indistinguishable in any well-typed context, where the notion “related” is defined as follows:

• Two values of a base type b are related if and only if they are equal.

• Two values of a function type τ_{1} → τ_{2} are related if and only if they map any related arguments to related results.

• Two values of an abstract type α are related if and only if they satisfy the relation φ(α), where φ maps each abstract type to a relation between its concrete types.

The power of parametricity comes from the fact that we can take any relation as φ(α) for each α in order to let two programs related. For example, in the first program above, we can take φ(α) = {(1, 2), (2, 4), (3, 6)}. Then, by parametricity, this program is equivalent to the same program with [1, 2, 3] substituted with [2, 4, 6], because isdiv(i)(j) is equal to isdiv(i′)(j′) for any (i, i′) ∈ φ(α) and (j, j′) ∈ φ(α). Therefore, the packaging is secure in the sense that it never leaks the secret data, as long as everybody plays by the rules of the type system. However, type abstraction fails if the scope of a value of an abstract type exceeds the scope of the type checker, e.g. if the value is saved in a file or sent over a network. For instance, the security of the package above is broken if the secret data ints is written to a file and read from the file just as a list of integers.

By contrast, encryption is dynamic and low-level: illegal access to secret data causes a decryption failure either in the user code (like ⌈head(ints)⌉_{bogus key}) or in the provider code (like isdiv ⌊7⌋_{bogus key}⌊8⌋_{bogus key}) during execution. It keeps attackers from breaking the protection with no assumptions about what they do, except for the secrecy of the keys and the mathematical strength of the underlying cryptosystem.

These comparisons between type abstraction and encryption lead us to wonder whether we can establish some more formal relationships between them. In particular:

• Can we adapt the parametricity theory of type abstraction to reason about programs that use encryption for information hiding?

• Can we have our cake and eat it too, first writing programs in the high-level but restrictive setting of type abstraction, and then translating them to the lower-level but more flexible setting of encryption without losing modularity and security?

In this paper, we give a full answer to the first question and a partial answer to the second. Specifically, we (i) present the cryptographic λ-calculus, a simply typed λ-calculus with shared-key cryptographic primitives, and illustrate its expressive power through several examples (Section 2), (ii) establish a theory of relational parametricity à la Reynolds [24] for this calculus (Section 3), and (iii) sketch an encoding of System F [13, 23] into the cryptographic λ-calculus (Section 4), using encryption to simulate type abstraction. Our primary contributions are (ii) and (iii). The expressiveness of the calculus is—though useful for modeling malicious attackers—a secondary issue.

2 The Cryptographic λ-Calculus

2.1 Syntax and Semantics

Our calculus is a standard simply typed call-by-value λ-calculus with records, booleans, and integers, enriched with simple primitives for shared-key cryptography.

An encryption ⌊t_{1}⌋_{t_{2}} encrypts the plaintext t_{1} with the key t_{2}, and a decryption let ⌊x⌋_{t_{1}} = t_{2} in t_{3} else t_{4} tries to decrypt the ciphertext t_{2} with the key t_{1}. If the decryption succeeds, it binds the plaintext to the variable x and evaluates the body t_{3}. If the decryption fails, it evaluates the handler t_{4}. A key generation new⟨τ, α⟩ generates a key to encrypt and decrypt values of the type τ using the password α. A key ⟨τ, α, n⟩ consists of the type τ of the values to encrypt and decrypt, the password α, and the sequence number n. The type is necessary for type soundness: without it, two values of different types could be encrypted using the same key, and then confused when they are decrypted, like let ⌊x⌋_{⟨ ,α,0⟩} = ⌊true⌋_{⟨ ,α,0⟩} in x − 1 else … (cf. Section 2.2). The sequence number is taken from a global counter, incremented on each key generation. Passwords are used for statically tracking knowledge about (possibly infinite) sets of dynamically generated keys to state security properties of programs in our calculus. (This point is discussed further after Corollary 10 in Section 3.) The primitive fail aborts evaluation.

We assume the following properties of these cryptographic primitives.

• No ciphertext can be decrypted or forged without using the key. In particular, no ciphertext can be fabricated from other ciphertexts (non-malleability [10]).

• No operation can be performed on ciphertexts without decrypting them. In particular, no ciphertexts can be compared for (in)equality. In practice, this condition can be satisfied by including random nonces in ciphertexts.

• No password can be guessed by conjecture. In practice, this assumption can be fulfilled by choosing “good” passwords for keys.

In short, we assume perfect encryption. Although no present-day cryptosystem—to our knowledge— has been proven to be satisfy all these conditions (and some are known not to), they offer a clean starting point for the arguments that we give in this paper. Investigating what kind of results can be obtained when these assumptions are weakened is a topic for future work.

Formally, the syntax and semantics of the cryptographic λ-calculus are given in Figure 1. (Throughout this paper, we abbreviate a sequence of the form X_{1}, …, X_{n} to a vector of the form X̃ when the number n is obvious.) In order to deal with the impurities such as key generation and failure in a rigorous manner, the evaluation function [[t]]_{n} takes an initial sequence number n and either diverges (written ⊥) or returns (i) a value v and a final sequence number n′ (written [v]_{n′}), (ii) fail, or (iii) error. Note that fail denotes a safe, intentional failure while error denotes an unsafe, unintentional error (a run-time type error).

We abbreviate [[t]]_{n} = [v]_{n′} to [[t]] = v when n and n′ are unimportant. For the sake of readability, we also use the syntactic sugarings (let x = t_{1} in t_{2}) =^{def} (λx. t_{2})t_{1} and ⌈t_{1}⌉_{t_{2}} =^{def} (let ⌊x⌋_{t_{2}} =

t ::= x | λx. t | t_{1}t_{2} | {ℓ̃= t̃} | #_{ℓ}(t) | true | false | if t_{1} then t_{2} else t_{3} | i | t_{1} − t_{2} | t > 0 |

⟨τ, α, n⟩ | new⟨τ, α⟩ | ⌊t_{1}⌋_{t_{2}} | let ⌊x⌋_{t_{1}} = t_{2} in t_{3} else t_{4} | fail

τ ::= τ_{1} → τ_{2} | {ℓ̃: τ̃} | bool | int | ⟨τ⟩ | bits
v ::= λx. t | {ℓ̃= ṽ} | true | false | i | ⟨τ, α, n⟩ | ⌊v⌋_{⟨τ,α,n⟩}
V ::= [v]_{n} | ⊥ | fail | error
[[λx. t]]_{n} =^{def} [λx. t]_{n}
[[t_{1}t_{2}]]_{n} =^{def} case [[t_{1}]]_{n} of [λx. t]_{n_{1}} ⇒

(case [[t_{2}]]_{n_{1}} of [v]_{n_{2}} ⇒ [[t[x := v]]]_{n_{2}} | V_{2} ⇒ V_{2})

| [ ] ⇒ error | V_{1} ⇒ V_{1}

[[{ℓ̃= t̃}]]_{n} =^{def} case [[t_{1}]]_{n} of [v_{1}]_{n_{1}} ⇒

… (case [[t_{m}]]_{n_{m−1}} of [v_{m}]_{n_{m}} ⇒ [{ℓ̃= ṽ}]_{n_{m}} | V_{m} ⇒ V_{m})

… | V_{1} ⇒ V_{1}

[[#_{ℓ}(t)]]_{n} =^{def} case [[t]]_{n} of [{ℓ = v, …}]_{n′} ⇒ [v]_{n′} | [ ] ⇒ error | V ⇒ V
[[true]]_{n} =^{def} [true]_{n}
[[false]]_{n} =^{def} [false]_{n}
[[if t_{1} then t_{2} else t_{3}]]_{n} =^{def} case [[t_{1}]]_{n} of [true]_{n′} ⇒ [[t_{2}]]_{n′} | [false]_{n′} ⇒ [[t_{3}]]_{n′}
| [ ] ⇒ error | V ⇒ V
[[i]]_{n} =^{def} [i]_{n}
[[t_{1} − t_{2}]]_{n} =^{def} case [[t_{1}]]_{n} of [i_{1}]_{n_{1}} ⇒

(case [[t_{2}]]_{n_{1}} of [i_{2}]_{n_{2}} ⇒ [i_{1} − i_{2}]_{n_{2}} | [ ] ⇒ error | V_{2} ⇒ V_{2})

| [ ] ⇒ error | V_{1} ⇒ V_{1}

[[t > 0]]_{n} =^{def} case [[t]]_{n} of [i]_{n′} ⇒ [i > 0]_{n′} | [ ] ⇒ error | V ⇒ V
[[⟨τ, α, m⟩]]_{n} =^{def} [⟨τ, α, m⟩]_{n}
[[new⟨τ, α⟩]]_{n} =^{def} [⟨τ, α, n + 1⟩]_{n+1}
[[⌊t_{1}⌋_{t_{2}}]]_{n} =^{def} case [[t_{1}]]_{n} of [v_{1}]_{n_{1}} ⇒

(case [[t_{2}]]_{n_{1}} of [⟨τ, α, m⟩]_{n_{2}} ⇒ [⌊v_{1}⌋_{⟨τ,α,m⟩}]_{n_{2}} | [ ] ⇒ error | V_{2} ⇒ V_{2})

| V_{1} ⇒ V_{1}

[[let ⌊x⌋_{t_{1}} = t_{2} in t_{3} else t_{4}]]_{n} =^{def} case [[t_{1}]]_{n} of [⟨τ, α, m⟩]_{n_{1}} ⇒

(case [[t_{2}]]_{n_{1}} of [⌊v_{2}⌋_{k}]_{n_{2}} ⇒

if k = ⟨τ, α, m⟩ then [[t_{3}[x := v_{2}]]]_{n_{2}} else [[t_{4}]]_{n_{2}} | [ ] ⇒ error | V_{2} ⇒ V_{2})

| [ ] ⇒ error | V_{1} ⇒ V_{1}

[[fail]]_{n} =^{def} fail

Figure 1: Syntax and Semantics

Γ, x : τ ⊢ x : τ  Γ ⊢ true : bool  Γ ⊢ false : bool  Γ ⊢ i : int

\frac{Γ, x : τ_{1} ⊢ t : τ_{2}}{Γ ⊢ λx. t : τ_{1} → τ_{2}}  \frac{Γ ⊢ t_{1} : τ_{1} → τ_{2} Γ ⊢ t_{2} : τ_{1}}{Γ ⊢ t_{1}t_{2} : τ_{2}}  \frac{Γ ⊢ t̃: τ̃}{Γ ⊢ \{ℓ̃= t̃\} : \{ℓ̃: τ̃\}} \frac{Γ ⊢ t : \{ℓ : τ, …\}}{Γ ⊢ #_{ℓ}(t) : τ}

\frac{Γ ⊢ t_{1} : bool Γ ⊢ t_{2} : τ Γ ⊢ t_{3} : τ}{Γ ⊢ if t_{1} then t_{2} else t_{3} : τ}  \frac{Γ ⊢ t_{1} : int Γ ⊢ t_{2} : int}{Γ ⊢ t_{1} − t_{2} : int}  \frac{Γ ⊢ t : int}{Γ ⊢ t > 0 : bool}
Γ ⊢ ⟨τ, α, n⟩ : ⟨τ⟩  Γ ⊢ new⟨τ, α⟩ : ⟨τ⟩  Γ ⊢ fail : τ
\frac{Γ ⊢ t_{1} : τ Γ ⊢ t_{2} : ⟨τ⟩}{Γ ⊢ ⌊t_{1}⌋_{t_{2}} : bits}  \frac{Γ ⊢ t_{1} : ⟨τ_{1}⟩ Γ ⊢ t_{2} : bits Γ, x : τ_{1} ⊢ t_{3} : τ_{2} Γ ⊢ t_{4} : τ_{2}}{Γ ⊢ let ⌊x⌋_{t_{1}} = t_{2} in t_{3} else t_{4} : τ_{2}}

Figure 2: Typing Rules

t_{1} in x else fail). We assume distinction between the names of variables, and apply α-conversion implicitly.

2.2 Type System

The typing rules for the cryptographic λ-calculus are shown in Figure 2. They are standard except for the types given to keys and ciphertexts. The type ⟨τ⟩ describes keys for encrypting and decrypting values of the type τ. The type bits (“bit string”) includes all ciphertexts. The fact that the type of a plaintext is included in the type of the key used to encrypt it, rather than the type of the ciphertext, is the source of the surprising expressive power of our calculus (cf. Section 2.4).

The correctness of the type system with respect to the semantics guarantees that a well-typed program incurs no run-time type error.

Theorem 1 (Type Soundness). Suppose x̃ : τ̃ ⊢ t : τ and let t′ = t[x̃ := ṽ] for any ∅ ⊢ ṽ : τ̃. Then, for any n, we have [[t′]]_{n} = ⊥, fail, or [v]_{n′} for some ∅ ⊢ v : τ and n′ ≥ n.

Proof. By induction on the derivation of x̃ : τ̃ ⊢ t : τ. □

2.3 Example

As a first example of programming in our calculus, consider the following situation. There are three entities S, A and B. The entities S and A share a password α, and the entities S and B share another password β. A wants to send an integer i to B in a secure manner, assuming that S is trustworthy.

To express A’s transmission of i to S under the password α, we use encryption (under α) and application:

A =^{def} S(⌊i⌋_{⟨int,α,0⟩})

To capture S’s actions—receiving the integer i under the password α, and forwarding it to B under the password β—we use abstraction, decryption (under α), encryption (under β), and application:

S =^{def} λx′. let x = ⌈x′⌉_{⟨int,α,0⟩} in B(⌊x⌋_{⟨int,β,0⟩})

Similarly, B’s receipt of i under the password β is expressed using abstraction and decryption:

B =^{def} λy′. let y = ⌈y′⌉_{⟨int,β,0⟩} in t(y)

The whole program works as follows:

[[let B = λy′. (let y = ⌈y′⌉_{⟨int,β,0⟩} in t(y)) in
let S = λx′. (let x = ⌈x′⌉_{⟨int,α,0⟩} in B(⌊x⌋_{⟨int,β,0⟩}))
S(⌊i⌋_{⟨int,α,0⟩})]]
= [[let B = λy′. (let y = ⌈y′⌉_{⟨int,β,0⟩} in t(y)) in
B(⌊i⌋_{⟨int,β,0⟩})]]
= [[t(i)]]

The security of each part of this program is guaranteed by the fact that, to any observer who does not know the passwords α and β, the functions S and B are indistinguishable from the function λ . fail, and the ciphertext ⌊i⌋_{⟨int,α,0⟩} is indistinguishable from the ciphertext ⌊0⌋_{⟨int,α,0⟩}. Details of such reasoning will be presented in Section 3.

2.4 Expressiveness

As we mentioned above, the cryptographic λ-calculus is rather expressive despite the fact that it is simply typed, thanks to the dynamic nature of the type bits. In this section, we illustrate its power by showing how to encode several constructs found in other λ-calculi. In these encodings, secrecy plays no role and a single, public password ε suffices for all encryptions. We write ⟨⟨τ⟩⟩ for the dummy key ⟨τ, ε, 0⟩ using this non-secret password.

The correctness of each encoding E(—) can be stated in the same way.

Theorem 2 (Soundness of Encodings). Suppose x̃ : τ̃ ⊢ t : τ and let t′ = t[x̃ := ṽ] for any ∅ ⊢ ṽ : τ̃, where t, ṽ, τ and τ̃ are terms, values, and types in the source language. Then, ∅ ⊢ E(t′) : E(τ) and [[E(t′)]]_{n} = E([[t′]]_{n}) for any n, where E([v]_{n}) = [E(v)]_{n}, E(⊥) = ⊥ and E(fail) = fail.

Proof. By induction on the derivation of x̃ : τ̃ ⊢ t : τ using the lemmas below, given at the end of each section for each extension introduced in that section. □

2.4.1 Disjoint Sums

A disjoint sum τ_{1} + τ_{2} is the tagged union of the types τ_{1} and τ_{2}. Its syntax, semantics, and typing rules are given below. (To simplify the encoding, we annotate each case expression with its result type τ.)

t ::= … | inl(t) | inr(t) | case t_{1} of inl(x) ⇒ t_{2} [] inr(y) ⇒ t_{3} : τ
τ ::= … | τ_{1} + τ_{2}
v ::= … | inl(v) | inr(v)
[[inl(t)]]_{n} =^{def} case [[t]]_{n} of [v]_{n′} ⇒ [inl(v)]_{n′} | V ⇒ V
[[inr(t)]]_{n} =^{def} case [[t]]_{n} of [v]_{n′} ⇒ [inr(v)]_{n′} | V ⇒ V
[[case t_{1} of inl(x) ⇒ t_{2} [] inr(y) ⇒ t_{3} : τ]]_{n}
=^{def} case [[t_{1}]]_{n} of [inl(v)]_{n′} ⇒ [[t_{2}[x := v]]]_{n′} | [inr(v)]_{n′} ⇒ [[t_{3}[y := v]]]_{n′}
| [ ] ⇒ error | V ⇒ V

\frac{Γ ⊢ t : τ_{1}}{Γ ⊢ inl(t) : τ_{1} + τ_{2}}  \frac{Γ ⊢ t : τ_{2}}{Γ ⊢ inr(t) : τ_{1} + τ_{2}}

\frac{Γ ⊢ t_{1} : τ_{1} + τ_{2} Γ, x : τ_{1} ⊢ t_{2} : τ Γ, y : τ_{2} ⊢ t_{3} : τ}{Γ ⊢ (case t_{1} of inl(x) ⇒ t_{2} [] inr(y) ⇒ t_{3} : τ) : τ}

Since disjoint sums are the dual of products, they can be encoded into the cryptographic calculus by a kind of CPS transformation as follows.

E(τ_{1} + τ_{2}) =^{def} (E(τ_{1}) → bits) → (E(τ_{2}) → bits) → bits
E(inl(t)) =^{def} let x = E(t) in λf. λg. f(x)
E(inr(t)) =^{def} let x = E(t) in λf. λg. g(x)
E(case t_{1} of inl(x) ⇒ t_{2} [] inr(y) ⇒ t_{3} : τ)
=^{def} ⌈E(t_{1})(λx. ⌊E(t_{2})⌋_{⟨⟨E(τ)⟩⟩})(λy. ⌊E(t_{3})⌋_{⟨⟨E(τ)⟩⟩})⌉_{⟨⟨E(τ)⟩⟩}

For the other cases, the encoding works in a homomorphic manner, i.e., along the structure of the type or the term. For example, E(τ_{1} → τ_{2}) = E(τ_{1}) → E(τ_{2}) and E(λx. t) = λx. E(t).

Lemma 3. [[E(case inl(v) of inl(x) ⇒ t_{1} [] inr(y) ⇒ t_{2} : τ)]]_{n} = [[E(t_{1})[x := E(v)]]]_{n} and [[E(case inr(v) of inl(x) ⇒ t_{1} [] inr(y) ⇒ t_{2} : τ)]]_{n} = [[E(t_{2})[y := E(v)]]]_{n} for any v, t_{1}, t_{2}, and n.

We can now—if we like—define the type bool as the disjoint sum {} + {} of the empty record {}. For the sake of presentation, however, we continue to take booleans as primitives.

2.4.2 Recursive Types

A recursive type is a type whose definition mentions itself, like intlist =^{def} {} + {head : int, tail : intlist}. Such types are often written as μα. {} + {head : int, tail : α}, using the least fixedpoint operator μ. In general, a recursive type μα. τ satisfies the equation μα. τ ≡ τ[α := μα. τ]. Its syntax, semantics, and typing rules are given below. Here, we use the simpler iso-recursive presentation (rather than the more powerful equi-recursive one), explicitly inserting the coercions fold and unfold to convert between values of the folded type μα. τ and the unfolded type τ[α := μα. τ]. Again, we provide type annotations to assist the encoding.

t ::= … | fold_{μα. τ} (t) | unfold_{μα. τ} (t)
τ ::= … | α | μα. τ
v ::= … | fold_{μα. τ} (v)
[[fold_{μα. τ} (t)]]_{n} =^{def} case [[t]]_{n} of [v]_{n′} ⇒ [fold_{μα. τ} (v)]_{n′} | V ⇒ V
[[unfold_{μα. τ} (t)]]_{n} =^{def} case [[t]]_{n} of [fold_{μα. τ} (v)]_{n′} ⇒ [v]_{n′} | [ ] ⇒ error | V ⇒ V

\frac{Γ ⊢ t : τ[α := μα. τ]}{Γ ⊢ (fold_{μα. τ} (t)) : μα. τ}  \frac{Γ ⊢ t : μα. τ}{Γ ⊢ unfold_{μα. τ} (t) : τ[α := μα. τ]}

Recursive types can be encoded into the cryptographic λ-calculus by taking values of recursive types to be ciphertexts and the folding and unfolding operations to be encryption and decryption.

E(α)  =^{def} bits
E(μα. τ)  =^{def} bits
E(fold_{μα. τ} (t))  =^{def} ⌊t⌋_{⟨⟨E(τ)⟩⟩}
E(unfold_{μα. τ} (t)) =^{def} ⌈t⌉_{⟨⟨E(τ)⟩⟩}

Lemma 4. [[E(unfold_{μα. τ} (fold_{μα. τ} (v)))]]_{n} = [[E(v)]]_{n} for any v and n.

2.4.3 Recursive Functions

Since recursive types can be encoded, recursive functions can be encoded as well. Using the encoding of recursive types above, the standard call-by-value fixed-point operator

fix_{τ_{1}→τ_{2}} =^{def} λf. (λx. f(λa. unfold_{τ} (x)xa))
(fold_{τ} (λx. f(λa. unfold_{τ} (x)xa)))

with τ = μα. α → τ_{1} → τ_{2} can be implemented as follows, with k = ⟨⟨bits → τ_{1} → τ_{2}⟩⟩.

E(fix_{τ_{1}→τ_{2}}) = λf. (λx. f(λa. ⌈x⌉_{k}xa))⌊λx. f(λa. ⌈x⌉_{k}xa)⌋_{k}

2.4.4 Dynamic Typing

Dynamic typing [2] is a mechanism for injecting values of different types into a single dynamic type dyn in a type-safe manner.

t ::= … | indyn_{τ} (t) | let indyn_{τ} (x) = t_{1} in t_{2} else t_{3}
τ ::= … | dyn
v ::= … | indyn_{τ} (v)
[[indyn_{τ} (t)]]_{n} =^{def} case [[t]]_{n} of [v]_{n′} ⇒ [indyn_{τ} (v)]_{n′} | V ⇒ V
[[let indyn_{τ} (x) = t_{1} in t_{2} else t_{3}]]_{n}
=^{def} case [[t_{1}]]_{n} of [indyn_{τ} (v)]_{n′} ⇒ [[t_{2}[x := v]]]_{n′} | [indyn ( )]_{n′} ⇒ [[t_{3}]]_{n′}
| [ ] ⇒ error | V ⇒ V

\frac{Γ ⊢ t : τ}{Γ ⊢ indyn_{τ} (t) : dyn}  \frac{Γ ⊢ t_{1} : dyn Γ, x : τ ⊢ t_{2} : τ Γ ⊢ t_{3} : τ}{Γ ⊢ let indyn_{τ} (x) = t_{1} in t_{2} else t_{3} : τ}

Thanks to the “dynamic” type bits, it is also straightforward to implement dynamic typing in the cryptographic calculus.

E(dyn) =^{def} bits
E(indyn_{τ} (t)) =^{def} ⌊t⌋_{⟨⟨E(τ)⟩⟩}
E(let indyn_{τ} (x) = t_{1} in t_{2} else t_{3}) =^{def} let ⌊x⌋_{⟨⟨E(τ)⟩⟩} = E(t_{1}) in E(t_{2}) else E(t_{3})

Lemma 5. [[E(let indyn_{τ} (x) = indyn_{τ} (v) in t_{1} else t_{2})]]_{n} = [[E(t_{1})[x := E(v)]]]_{n} and [[E(let indyn_{τ} (x) = v′ in t_{1} else t_{2})]]_{n} = [[E(t_{2})]]_{n} for any n, v and v′ ≠ indyn_{τ} (v).

R_{S}(τ → τ′)φ =^{def} {(λx. t_{1}, λx. t_{2}) | ∀(v_{1}, v_{2}) ∈ R_{S}(τ)φ. (t_{1}[x := v_{1}], t_{2}[x := v_{2}]) ∈ R′_{S}(τ′)φ}
R_{S}({ℓ̃: τ̃})φ =^{def} {({ℓ̃= ṽ_{1}}, {ℓ̃= ṽ_{2}}) | (ṽ_{1}, ṽ_{2}) ∈ R_{S}(τ̃)φ}
R_{S}(bool)φ =^{def} {(b, b) | b = true, false}
R_{S}(int)φ =^{def} {(i, i) | i = …, −2, −1, 0, 1, 2, …}
R_{S}(⟨τ⟩)φ =^{def} {(⟨τ, α, n⟩, ⟨τ, α, n⟩) | α ∉ S}
R_{S}(bits)φ =^{def} {(⌊v_{1}⌋_{⟨τ,α,n⟩}, ⌊v_{2}⌋_{⟨τ,α,n⟩}) | ∅ ⊢ v_{1} : τ ∧ ∅ ⊢ v_{2} : τ ∧ α ∉ S ∧ (v_{1}, v_{2}) ∈ R_{S}(τ)φ
∪ {(⌊v_{1}⌋_{⟨τ_{1},α_{1},n_{1}⟩}, ⌊v_{2}⌋_{⟨τ_{2},α_{2},n_{2}⟩}) | ∅ ⊢ v_{1} : τ_{1} ∧ ∅ ⊢ v_{2} : τ_{2} ∧ α_{1}, α_{2} ∈ S ∧

(v_{1}, v_{2}) ∈ φ(⟨τ_{1}, α_{1}, n_{1}⟩, ⟨τ_{2}, α_{2}, n_{2}⟩)}

R′_{S}(τ)φ =^{def} {(t_{1}, t_{2}) | ∅ ⊢ t_{1} : τ ∧ ∅ ⊢ t_{2} : τ ∧

∀n. ([[t_{1}]]_{n} = [[t_{2}]]_{n} = ⊥ ∨ [[t_{1}]]_{n} = [[t_{2}]]_{n} = fail ∨ ∃v_{1}. ∃v_{2}. ∃n′ ≥ n.

[[t_{1}]]_{n} = [v_{1}]_{n′} ∧ [[t_{2}]]_{n} = [v_{2}]_{n′} ∧ (v_{1}, v_{2}) ∈ R_{S}(τ)φ)}

Figure 3: Logical Relation

3 Parametricity

In this section, we develop a tool for reasoning about information hiding in the cryptographic λ-calculus, adapting the concept of parametricity [24] from the polymorphic λ-calculus [13, 23].

Consider the packages p_{1} =^{def} {c = ⌊1⌋_{k}, f = λx. ⌈x⌉_{k} + 2} and p_{2} =^{def} {c = ⌊3⌋_{k}, f = λx. ⌈x⌉_{k}}, where k = ⟨int, α, n⟩ for some α and n, and t_{1} + t_{2} stands for t_{1} − (0 − t_{2}). A function that does not know the password α cannot distinguish p_{1} and p_{2}, because it cannot decrypt the ciphertexts #_{c}(p_{1}) and #_{c}(p_{2}), and the function applications #_{f}(p_{1})#_{c}(p_{1}) and #_{f}(p_{2})#_{c}(p_{2}), which are the only ways to do anything on the ciphertexts #_{c}(p_{1}) and #_{c}(p_{2}), return the same integer 3.

To formalize such reasoning, we define a relation R_{S}(τ)φ between values of the type τ, where S is a set of “secret” passwords {α̃} and φ maps a pair of secret keys to a relation between plaintexts. Intuitively, two values v_{1} and v_{2} will be related by R_{S}(τ)φ if and only if

• v_{1} and v_{2} do not reveal any information about the secret passwords S, and

• they are indistinguishable by any function that does not know the secret passwords.

The first condition is essential because if the values themselves leak the secret passwords, then the observer can break the abstraction without knowing any secret password in advance. For example, suppose k = ⟨int, α, n⟩ for some α ∈ S and n. Although the ciphertexts ⌊4⌋_{k} and ⌊5⌋_{k} are indistinguishable to any observer who does not know the secret password α, the records {c = ⌊4⌋_{k}, k = k} and {c = ⌊5⌋_{k}, k = k} are distinguishable to the observer λr. ⌈#_{c}(r)⌉_{#_{k}(r)}. Thus, the key k should not be related to itself if the password α is secret.

Just as we can take any relation for values of an abstract type in the parametricity theory of type abstraction (cf. Section 1), we can take any relation for ciphertexts encrypted with secret passwords because they are anyway indistinguishable to the observer. The map φ in the relation R_{S}(τ)φ provides such a relation between values of the type τ_{1} and values of the type τ_{2} for each pair of keys ⟨τ_{1}, α_{1}, n_{1}⟩ and ⟨τ_{2}, α_{2}, n_{2}⟩ with α_{1}, α_{2} ∈ S.

Formally, the relation R_{S}(τ)φ is defined in Figure 3 by induction on the type τ. It is a standard logical relation except for the following points.

• Since the cryptographic calculus is impure (because of key generation, failure, and divergence), we actually define two relations R_{S}(τ)φ and R′_{S}(τ)φ, the former over values (i.e., results of evaluations) and the latter over computations (i.e., closed terms with potential effects).

• Two keys are not related if their passwords are secret, because they would leak the secret and break the first condition (like the second example above).

• Two ciphertexts encrypted with a non-secret key are related if and only if the plaintexts are related.

• Two ciphertexts encrypted with secret keys k_{1} and k_{2} are related if and only if they satisfy the relation φ(k_{1}, k_{2}).

For instance, in the first example above, let us take S = {α}, φ(k, k) = {(1, 3)} and φ(k_{1}, k_{2}) = ∅ when k_{1} ≠ k or k_{2} ≠ k. Then, (⌊1⌋_{k}, ⌊3⌋_{k}) ∈ R_{S}(bits)φ because (1, 3) ∈ φ(k, k) and α ∈ S, and (λx. ⌈x⌉_{k} + 2, λx. ⌈x⌉_{k}) ∈ R_{S}(bits → int)φ because [[(λx. ⌈x⌉_{k} + 2)⌊1⌋_{k}]] = [[(λx. ⌈x⌉_{k})⌊3⌋_{k}]] = 3. Therefore, (p_{1}, p_{2}) ∈ R_{S}({c : bits, f : bits → int})φ.

Thus, we expect that the packages p_{1} and p_{2} are observationally equivalent, in the sense that a function that does not know the password α cannot distinguish them. That is, g(p_{1}) = g(p_{2}) for any g : {c : bits, f : bits → int} → bool where α does not appear in g. In order to prove this fact, it suffices to show (g, g) ∈ R_{S}({c : bits, f : bits → int} → bool)φ, which is a special case of the general theorem below.

Definition 6. knows(t) = {α | α appears in t}.

Theorem 7 (Parametricity). Suppose x̃ : τ̃ ⊢ t : τ. Then, (t[x̃ := ṽ_{1}], t[x̃ := ṽ_{2}]) ∈ R′_{S}(τ)φ for any (ṽ_{1}, ṽ_{2}) ∈ R_{S}(τ̃)φ, provided that S ∩ knows(t) = ∅ and dom(φ) = {(⟨σ_{1}, α_{1}, n_{1}⟩, ⟨σ_{2}, α_{2}, n_{2}⟩) | α_{1}, α_{2} ∈ S}.

Proof. By induction on the derivation of x̃ : τ̃ ⊢ t : τ. Let θ_{1} = [x̃ := ṽ_{1}], θ_{2} = [x̃ := ṽ_{2}], and Γ = x̃ : τ̃.

Case t = x_{i}. Immediate from the assumption that (v_{1}_{i}, v_{2}_{i}) ∈ R_{S}(τ_{i})φ and the fact that v_{1}_{i} and v_{2}_{i} are values.

Case t = λy. t′. Suppose τ = τ′′ → τ′, Γ, y : τ′′ ⊢ t′ : τ′, and (v′_{1}, v′_{2}) ∈ R_{S}(τ′′)φ. Then, by the induction hypothesis, (θ_{1}t′[y := v′_{1}], θ_{2}t′[y := v′_{2}]) ∈ R′_{S}(τ′)φ. Therefore, by the definition of R for arrow types, (θ_{1}t, θ_{2}t) ∈ R_{S}(τ)φ. Thus, since θ_{1}t and θ_{2}t are values, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Case t = t_{a}t_{b}. Suppose Γ ⊢ t_{a} : τ_{b} → τ and Γ ⊢ t_{b} : τ_{b}. Then, by the induction hypothesis, (θ_{1}t_{a}, θ_{2}t_{a}) ∈ R′_{S}(τ_{b} → τ)φ and (θ_{1}t_{b}, θ_{2}t_{b}) ∈ R′_{S}(τ_{b})φ. If the evaluations of θ_{1}t_{a} and θ_{2}t_{a} (or θ_{1}t_{b} and θ_{2}t_{b}) diverge or fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t_{a}]]_{n} = [λy. t′_{1}]_{n_{a}} and [[θ_{2}t_{a}]]_{n} = [λy. t′_{2}]_{n_{a}} where n_{a} ≥ n and (λy. t′_{1}, λy. t′_{2}) ∈ R_{S}(τ_{b} → τ)φ, and [[θ_{1}t_{b}]]_{n_{a}} = [v′_{1}]_{n_{b}} and [[θ_{2}t_{b}]]_{n_{a}} = [v′_{2}]_{n_{b}} where n_{b} ≥ n and (v′_{1}, v′_{2}) ∈ R_{S}(τ_{b})φ. Then, by the definition of R for arrow types, (t′_{1}[y := v′_{1}], t′_{2}[y := v′_{2}]) ∈ R′_{S}(τ)φ. On the other hand, by the definition of the evaluation for function applications, [[θ_{1}t]]_{n} = [[t′_{1}[y := v′_{1}]]]_{n_{b}} and [[θ_{2}t]]_{=}[[t′_{2}[y := v′_{2}]]]_{n_{b}}. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Case t = {ℓ̃ = t̃′}. Suppose τ = {ℓ̃ : τ̃′} and Γ ⊢ t̃′ : τ̃′. Then, by the induction hypothesis, (θ_{1}t̃′, θ_{2}t̃′) ∈ R′_{S}(τ̃′)φ. If the evaluations of θ_{1}t′_{i} and θ_{2}t′_{i} diverge or fail for some i, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t′_{i}]]_{n_{i−1}} = [v′_{1}_{i}]_{n_{i}} and [[θ_{2}t′_{i}]]_{n_{i−1}} = [v′_{2}_{i}]_{n_{i}} where n_{i} ≥ n_{i−1} and (v′_{1}_{i}, v′_{1}_{i}) ∈ R_{S}(τ′_{i})φ for every i. Then, by the definition the evaluation for record constructions, [[θ_{1}t]]_{n_{0}} = [{ℓ̃ = ṽ′_{1}}]_{n_{m}} and [[θ_{2}t]]_{n_{0}} = [{ℓ̃= ṽ′_{2}}]_{n_{m}}. Therefore, by the definition of R for record types, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Case t = #_{ℓ}(t′). By the induction hypothesis, (θ_{1}t′, θ_{2}t′) ∈ R′_{S}({ℓ : τ, …})φ. If the evaluations of θ_{1}t′ and θ_{2}t′ diverge or fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t′]]_{n} = [{ℓ = v′_{1}, …}]_{n′} and [[θ_{2}t′]]_{n} = [{ℓ = v′_{2}, …}]_{n′} where n′ ≥ n and (v′_{1}, v′_{2}) ∈ R_{S}(τ)φ. Then, by the definition the evaluation for record destructions, [[θ_{1}t]]_{n} = [v′_{1}]_{n′} and [[θ_{2}t]]_{n} = [v′_{2}]_{n′}. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Case t = true, false. Immediate from the definition of R for boolean types.

Case t = if t_{a} then t_{b} else t_{c}. By the induction hypothesis, (θ_{1}t_{a}, θ_{2}t_{a}) ∈ R′_{S}(bool)φ. If the evaluations of θ_{1}t_{a} and θ_{2}t_{a} diverge or fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t_{a}]]_{n} = [b_{1}]_{n′} and [[θ_{2}t_{a}]]_{n} = [b_{2}]_{n′} where n′ ≥ n and (b_{1}, b_{2}) ∈ R_{S}(bool)φ. Then, by the definition of R for boolean types, b_{1} = b_{2}. Let us consider the case b_{1} = b_{2} = true. (The case b_{1} = b_{2} = false is similar.) By the definition the evaluation for conditional branches, [[θ_{1}t]]_{n} = [[θ_{1}t_{b}]]_{n′} and [[θ_{2}t]]_{n} = [[θ_{2}t_{b}]]_{n′}. On the other hand, by the induction hypothesis, (θ_{1}t_{b}, θ_{2}t_{b}) ∈ R′_{S}(τ)φ. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Case t = i. Immediate from the definition of R for integer types.

Case t = t_{a} − t_{b}. By the induction hypothesis, (θ_{1}t_{a}, θ_{2}t_{a}) ∈ R′_{S}(int)φ and (θ_{1}t_{b}, θ_{2}t_{b}) ∈ R′_{S}(int)φ. If the evaluations of θ_{1}t_{a} and θ_{2}t_{a} (or θ_{1}t_{b} and θ_{2}t_{b}) diverge of fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t_{a}]]_{n} = [i_{1}]_{n_{a}} and [[θ_{2}t_{a}]]_{n} = [i_{2}]_{n_{a}} where n_{a} ≥ n and (i_{1}, i_{2}) ∈ R_{S}(int)φ, and [[θ_{1}t_{b}]]_{n_{a}} = [j_{1}]_{n_{b}} and [[θ_{2}t_{b}]]_{n_{a}} = [j_{2}]_{n_{b}} where n_{b} ≥ n_{a} and (j_{1}, j_{2}) ∈ R_{S}(int)φ. Then, by the definition of R for integer types, i_{1} = i_{2} and j_{1} = j_{2}. On the other hand, by the definition of the evaluation for integer subtractions, [[θ_{1}t]]_{n} = [i_{1} − j_{1}]_{n_{b}} and [[θ_{2}t]]_{n} = [i_{2} − j_{2}]_{n_{b}}. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(int)φ.

Case t = t′ > 0. By the induction hypothesis, (θ_{1}t′, θ_{2}t′) ∈ R′_{S}(int)φ. If the evaluations of θ_{1}t′ and θ_{2}t′ diverge of fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t′]]_{n} = [i_{1}]_{n_{a}} and [[θ_{2}t′]]_{n} = [i_{2}]_{n_{a}} where n_{a} ≥ n and (i_{1}, i_{2}) ∈ R_{S}(int)φ. Then, by the definition of R for integer types, i_{1} = i_{2}. On the other hand, by the definition the evaluation for integer comparisons, [[θ_{1}t]]_{n} = [i_{1} > 0]_{n_{a}} and [[θ_{2}t]]_{n} = [i_{2} > 0]_{n_{a}}. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(bool)φ.

Case t = ⟨τ′, α′, n′⟩. By the assumption that S ∩ knows(t) = ∅, α′ ∉ S. Therefore, by the definition of R for key types, (t, t) ∈ R_{S}(⟨τ′⟩)φ. Thus, since t is a value, (t, t) ∈ R′_{S}(⟨τ′⟩)φ.

Case t = new⟨τ′, α′⟩. By the definition of the evaluation for key generations, [[t]]_{n} = [⟨τ′, α′, n + 1⟩]_{n+1} for any n. On the other hand, by the assumption that S ∩ knows(t) = ∅, α′ ∉ S. Therefore, by the definition of R for key types, (⟨τ′, α′, n + 1⟩, ⟨τ′, α′, n + 1⟩) ∈ R_{S}(⟨τ′⟩)φ. Thus, (t, t) ∈ R′_{S}(⟨τ′⟩)φ.

Case t = ⌊t_{a}⌋_{t_{b}}. Suppose Γ ⊢ t_{a} : τ_{a} and Γ ⊢ t_{b} : ⟨τ_{a}⟩. Then, by the induction hypothesis, (θ_{1}t_{a}, θ_{2}t_{a}) ∈ R′_{S}(τ_{a})φ and (θ_{1}t_{b}, θ_{2}t_{b}) ∈ R′_{S}(⟨τ_{a}⟩)φ. If the evaluations of θ_{1}t_{a} and θ_{2}t_{a} (or θ_{1}t_{b} and θ_{2}t_{b}) diverge or fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t_{a}]]_{n} = [v′_{1}]_{n_{a}} and [[θ_{2}t_{a}]]_{n} = [v′_{2}]_{n_{a}} where n_{a} ≥ n and (v′_{1}, v′_{2}) ∈ R_{S}(τ_{a})φ, and [[θ_{1}t_{b}]]_{n_{a}} = [k_{1}]_{n_{b}} and [[θ_{2}t_{b}]]_{n_{a}} = [k_{2}]_{n_{b}} where n_{b} ≥ n and (k_{1}, k_{2}) ∈ R_{S}(⟨τ_{a}⟩)φ. Then, by the definition of R for key types, k_{1} = k_{2} = ⟨τ_{a}, α′, n′⟩ for some α′ ∉ S and n′. On the other hand, by the definition of the evaluation for encryptions, [[θ_{1}t]]_{n} = [⌊v′_{1}⌋_{k_{1}}]_{n_{b}} and [[θ_{2}t]]_{n} = [⌊v′_{2}⌋_{k_{2}}]_{n_{b}}. Therefore, by the definition of R for ciphertext types, (θ_{1}t, θ_{2}t) ∈ R′_{S}(bits)φ.

Case t = (let ⌊x⌋_{t_{a}} = t_{b} in t_{c} else t_{d}). Suppose Γ ⊢ t_{a} : ⟨τ′⟩ and Γ ⊢ t_{b} : bits. Then, by the induction hypothesis, (θ_{1}t_{a}, θ_{2}t_{a}) ∈ R′_{S}(⟨τ′⟩)φ and (θ_{1}t_{b}, θ_{2}t_{b}) ∈ R′_{S}(bits)φ. If the evaluations of θ_{1}t_{a} and θ_{2}t_{a} (or θ_{1}t_{b} and θ_{2}t_{b}) diverge or fail, then so do the evaluations of θ_{1}t and θ_{2}t, and the theorem follows from the definition of R′. Otherwise, suppose [[θ_{1}t_{a}]]_{n} = [k_{1}]_{n_{a}} and [[θ_{2}t_{a}]]_{n} = [k_{2}]_{n_{a}} where n_{a} ≥ n and (k_{1}, k_{2}) ∈ R_{S}(⟨τ′⟩)φ, and [[θ_{1}t_{b}]]_{n_{a}} = [⌊v′_{1}⌋_{k′_{1}}]_{n_{b}} and [[θ_{2}t_{b}]]_{n_{a}} = [⌊v′_{2}⌋_{k′_{2}}]_{n_{b}} where n_{b} ≥ n and (⌊v′_{1}⌋_{k′_{1}}, ⌊v′_{2}⌋_{k′_{2}}) ∈ R_{S}(bits)φ. Then, by the definition of R for key types, k_{1} = k_{2} = ⟨τ_{a}, α′, n′⟩ for some α′ ∉ S and n′. By the definition of R for ciphertext types, the following two sub-cases are possible:

Sub-case (k_{1} = k_{2} = k′_{1} = k′_{2}) ∧ (v′_{1}, v′_{2}) ∈ R_{S}(τ′)φ. By the definition of the evaluation for decryptions, [[θ_{1}t]]_{n} = [[θ_{1}t_{c}[x := v′_{1}]]]_{n_{b}} and [[θ_{2}t]]_{n} = [[θ_{2}t_{c}[x := v′_{2}]]]_{n_{b}}. On the other hand, by the induction hypothesis, (θ_{1}t_{c}[x := v′_{1}], θ_{2}t_{c}[x := v′_{2}]) ∈ R′_{S}(τ)φ. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Sub-case (k_{1} ≠ k′_{1})∧(k_{2} ≠ k′_{2}). By the definition of the evaluation for decryptions, [[θ_{1}t]]_{n} = [[θ_{1}t_{d}]]_{n_{b}} and [[θ_{2}t]]_{n} = [[θ_{2}t_{d}]]_{n_{b}}. On the other hand, by the induction hypothesis, (θ_{1}t_{d}, θ_{2}t_{d}) ∈ R′_{S}(τ)φ. Therefore, (θ_{1}t, θ_{2}t) ∈ R′_{S}(τ)φ.

Case t = fail. Immediate from the definition of R′. □

From the parametricity theorem above, the non-interference property below follows immediately. It states that values encrypted with secret passwords cannot be distinguished from one another by any function ignorant of the secret passwords.

Corollary 8 (Non-Interference). Suppose ∅ ⊢ t : bits → bool and α_{1}, α_{2} ∉ knows(t). Then, [[t⌊v_{1}⌋_{k_{1}}]]_{n} = [[t⌊v_{2}⌋_{k_{2}}]]_{n} for any n, k_{1} = ⟨τ_{1}, α_{1}, n_{1}⟩, k_{2} = ⟨τ_{2}, α_{2}, n_{2}⟩, ∅ ⊢ v_{1} : τ_{1}, and ∅ ⊢ v_{2} : τ_{2}.

Proof. Let S = {α_{1}, α_{2}}, φ(k_{1}, k_{2}) = {(v_{1}, v_{2})}, and φ(k′_{1}, k′_{2}) = ∅ whenever (k′_{1}, k′_{2}) ≠ (k_{1}, k_{2}). Then, (t, t) ∈ R_{S}(bits → bool)φ by Theorem 7 and (⌊v_{1}⌋_{k_{1}}, ⌊v_{2}⌋_{k_{2}}) ∈ R_{S}(bits)φ by the definition of R_{S}(bits)φ. Therefore, by the definition of R_{S}(bits → bool)φ, we have (t⌊v_{1}⌋_{k_{1}}, t⌊v_{2}⌋_{k_{2}}) ∈ R′_{S}(bool)φ. Thus, by the definition of R′_{S}(bool)φ, [[t⌊v_{1}⌋_{k_{1}}]]_{n} = [[t⌊v_{2}⌋_{k_{2}}]]_{n}. □

More generally, related terms can be proved as follows to be indistinguishable to any observer who does not know the secret passwords.

Definition 9. Two closed terms t_{1} and t_{2} of type τ are said to be observationally equivalent with respect to a set S of secret passwords, written t_{1} =^{obs}_{S} t_{2} : τ, if and only if [[t(t_{1})]]_{n} = [[t(t_{2})]]_{n} for any n and t with ∅ ⊢ t : τ → bool and S ∩ knows(t) = ∅.

Corollary 10 (Soundness of Parametricity). (t_{1}, t_{2}) ∈ R′_{S}(τ)φ implies t_{1} =^{obs}_{S} t_{2} : τ for any t_{1}, t_{2}, τ, S, and φ with dom(φ) = {(⟨τ_{1}, α_{1}, n_{1}⟩, ⟨τ_{2}, α_{2}, n_{2}⟩) | α_{1}, α_{2} ∈ S}.

Proof. Immediate from Theorem 7 and the definition of the logical relation for arrow types. □

The reason why we include passwords (in addition to sequence numbers) in keys can now be explained more precisely. Consider two terms t_{1} =^{def} (let k_{1} = new⟨int, α⟩ in ⌊1⌋_{k_{1}}) and t_{2} =^{def} (let k_{2} = new⟨int, α⟩ in ⌊2⌋_{k_{2}}), for example. Then, t_{1} =^{obs}_{{α}} t_{2} : bits. Without the password α, it would be hard to specify the values of the secret keys k_{1} and k_{2}, because we would have to determine their sequence numbers, which depend on the contexts.

Example 11. Suppose p_{1} =^{def} {c = ⌊1⌋_{k}, f = λx. ⌈x⌉_{k} + 2} and p_{2} =^{def} {c = ⌊3⌋_{k}, f = λx. ⌈x⌉_{k}}

where k = ⟨int, α, n⟩ for some α and n. Then, as we saw in the first example at the beginning of this section, (p_{1}, p_{2}) ∈ R_{S}(τ)φ where τ = {c : bits, f : bits → int}, S = {α}, φ(k, k) = {(1, 3)}, and φ(k_{1}, k_{2}) = ∅ for (k_{1}, k_{2}) ≠ (k, k). Therefore, p_{1} =^{obs}_{S} p_{2} : τ by Corollary 10.

Example 12. Suppose k = ⟨int, α, n⟩, α ∈ S, and (4, 5) ∈ φ(k, k). Then, (⌊4⌋_{k}, ⌊5⌋_{k}) ∈ R_{S}(bits)φ but (k, k) ∉ R_{S}(⟨int⟩)φ, so ({c = ⌊4⌋_{k}, k = k}, {c = ⌊5⌋_{k}, k = k}) ∉ R_{S}({c : bits, k : ⟨int⟩})φ as we saw in the second example at the beginning of this section. Indeed, ⌊4⌋_{k} =^{obs}_{S} ⌊5⌋_{k} : bits but

{c = ⌊4⌋_{k}, k = k} ≠^{obs}_{S} {c = ⌊5⌋_{k}, k = k} : {c : bits, k : ⟨int⟩}.

The next example suggests how to enforce the abstractness of polymorphic types (e.g., a value of the type ∀α. α → α is the universal identity function) by wrapping a term with encryption and decryption. Section 4 develops this intuition in greater detail.

Example 13. Suppose k = ⟨τ, α, n⟩ and ∅ ⊢ f : bits → bits, with α ∉ knows(f). Then, [[⌈f⌊v⌋_{k}⌉_{k}]] = v for any ∅ ⊢ v : τ, provided that the evaluation does not fail or diverge.

Proof. Let S = {α}, φ(k, k) = {(v, v)}, and φ(k_{1}, k_{2}) = ∅ when (k_{1}, k_{2}) ≠ (k, k). Then, by the definition of the logical relation for ciphertexts, (⌊v⌋_{k}, ⌊v⌋_{k}) ∈ R_{S}(bits)φ. At the same time, by Theorem 7, (f, f) ∈ R_{S}(bits → bits)φ. Therefore, by the definition of the logical relation for arrow types, ([[f⌊v⌋_{k}]], [[f⌊v⌋_{k}]]) ∈ R_{S}(bits)φ. On the other hand, since the decryption ⌈f⌊v⌋_{k}⌉_{k} does not fail, [[f⌊v⌋_{k}]] = ⌊v′⌋_{k} for some v′. Thus, we have (⌊v′⌋_{k}, ⌊v′⌋_{k}) ∈ R_{S}(bits)φ, which implies v = v′ by the definition of the logical relation for ciphertexts. Therefore, [[⌈f⌊v⌋_{k}⌉_{k}]] = [[⌈⌊v′⌋_{k}⌉_{k}]] = v′ = v.

□

4 Encoding Type Abstraction

In the previous section, we adapted the parametricity theory of type abstraction for the cryptographic λ-calculus, providing a high-level tool for reasoning about “cryptographic abstraction.” An even more attractive scenario would be one where we could simply write our programs in terms of polymorphism (for simplicity), and then translate uses of polymorphism into encryption to allow our programs to operate in a more flexible setting (including networking, etc.) with a broader range of attackers while preserving the abstraction guarantees of the original program. In this section, we propose such an encoding of the polymorphic λ-calculus into the cryptographic calculus. We begin in Section 4.1 with a naive version that illustrates most of the ideas but does not protect itself from malicious functions that may be passed in from the environment. In Section 4.2 we show how to add such protection.

The source language of the encoding is the standard polymorphic λ-calculus (System F) [13, 23] with existential types, with two minor changes:

• Each type application (e_{1} : ∀α. T)[e_{2}] is annotated with the type ∀α. T of the term e_{1}, so that the encoding can be defined on typed terms instead of their typing derivation trees. (This type annotation will be elided when it is unimportant.)

• The primitive fail, the divergence ⊥, and the global counter increment inc are included for the sake of convenience, since those effects are also present in the target language. Alternatively, we could exclude them from the source language and weaken the conjecture of full abstraction (Conjecture 15) to “full abstraction modulo effects,” i.e., the encodings of equivalent terms are equivalent except for failure, divergence, and sequence numbers.

In the encoding, we assume that all bound type variables are pairwise distinct by α-conversion.

4.1 Naive Encoding

Before presenting an encoding that preserves type abstraction, let us consider an encoding that just preserves well-typedness of terms. This is already non-trivial, since we are translating a polymorphic language into a monomorphic one. Consider, for example, the term

let id : ∀α. α → α = Λα. λx : α. x in {i = id[int]123, b = id[bool]true}

in the source language. If we only erase the types, we get an ill-typed term:

let id = λ . λx. x in {i = id{}123, b = id{}true}

Instead, as we did in the encoding of recursive types, we encode each type variable α as the ciphertext type bits and insert encryption and decryption when we use values of universal types (and, dually, when we make values of existential types). In the present example, the universal type ∀α. α → α is encoded as the type {} → bits → bits, the type abstraction Λα. λx : α. x is encoded as the function λ . λx. x of type {} → bits → bits, and the instantiations id[int] and id[bool] are encoded as functions λz. ⌈id{}⌊z⌋_{⟨⟨int⟩⟩}⌉_{⟨⟨int⟩⟩} and λz. ⌈id{}⌊z⌋_{⟨⟨bool⟩⟩}⌉_{⟨⟨bool⟩⟩} of types int → int and bool → bool, respectively. These translations together yield the following well-typed term:

let id = λ . λx. x
in {i = (λz. ⌈id{}⌊z⌋_{⟨⟨int⟩⟩}⌉_{⟨⟨int⟩⟩})123,
b = (λz. ⌈id{}⌊z⌋_{⟨⟨bool⟩⟩}⌉_{⟨⟨bool⟩⟩})true}

Formally, the encoding E(e) is given in Figure 4. Type abstractions and type applications are encoded as abstractions and applications of the empty record {}, so that the evaluation order is preserved. The coercions C^{+} and C^{−} insert the encryption and decryption, respectively, to convert between (the encodings of) values of abstract types (such as α → α) and concrete types (such as int → int) by η-expansion. More specifically, if α = T′ and k : ⟨E(T′)⟩, then the coercions C_{α}^{±}(x, k, T) convert between (the encodings of) values of the abstract type T and a concrete type T [α := T′] by η-expanding the value x along the type T. For example, consider a function f of type T = α → α in the source language. In order to instantiate its encoding f′ = E(f) of type bits → bits in the target language, say, with α = int, the coercion C_{α}^{−}(f′, k, α → α) η-expands it to a function λy. ⌈f′⌊y⌋_{k}⌉_{k} of type int → int with k : ⟨int⟩.

4.2 Better Encoding

Although the encoding above suffices as far as only “good citizens” translated from the source language are concerned, it does not protect type abstractions from malicious attackers hand-coded in the target language, because not all terms of type E(T) (such as {} → bits → bits) in the target language behave like encodings of terms of the type T (such as ∀α. α → α) in the source language. For example, consider the terms e_{1} =^{def} λf : (∀α. α → α). f and

e_{2} =^{def} λf : (∀α. α → α). Λβ. let f′ : β → β = f[β] in λx : β. let y : β = f′x in x

of type T =^{def} (∀α. α → α) → (∀α. α → α). In the source language, they are indistinguishable because [[f[τ]v]] = v for any f : ∀α. α → α and v : τ unless the evaluation fails or diverges. On the

E(Λα. e) =^{def} λ . E(e)
E((e : ∀α. T_{1})[T_{2}]) =^{def} let x = E(e){} in C_{α}^{−}(x, ⟨⟨E(T_{2})⟩⟩, T_{1})
E(pack T_{1}, e as ∃α. T_{2}) =^{def} let x = E(e) in C_{α}^{+}(x, ⟨⟨E(T_{1})⟩⟩, T_{2})
E(open e_{1} as α, x in e_{2}) =^{def} let x = E(e_{1}) in E(e_{2})
E(x) =^{def} x
E(λx : T. e) =^{def} λx. E(e)
E(e_{1}e_{2}) =^{def} E(e_{1})E(e_{2})
E({ℓ̃= ẽ}) =^{def} {ℓ̃= E(ẽ)}
E(#_{ℓ}(e)) =^{def} #_{ℓ}(E(e))
E(if e_{1} then e_{2} else e_{3}) =^{def} if E(e_{1}) then E(e_{2}) else E(e_{3})
E(true) =^{def} true
E(false) =^{def} false
E(i) =^{def} i
E(e_{1} − e_{2}) =^{def} E(e_{1}) − E(e_{2})
E(e > 0) =^{def} E(e) > 0
E(fail) =^{def} fail
E(⊥) =^{def} (λx. x⌊x⌋_{⟨⟨bits→{}⟩⟩})(λx. ⌈x⌉_{⟨⟨bits→{}⟩⟩}x)
E(inc) =^{def} let = new⟨{}, ε⟩ in {}
E(α) =^{def} bits
E(∀α. T) =^{def} {} → E(T)
E(∃α. T) =^{def} E(T)
E(T_{1} → T_{2}) =^{def} E(T_{1}) → E(T_{2})
E({ℓ̃: T̃}) =^{def} {ℓ̃: E(T̃)}
E(bool) =^{def} bool
E(int) =^{def} int
C_{α}^{+}(x, k, α) =^{def} ⌊x⌋_{k}
C_{α}^{−}(x, k, α) =^{def} ⌈x⌉_{k}
C_{α}^{±}(x, k, β) =^{def} x  (if α ≠ β)
C_{α}^{±}(x, k, ∀β. T) =^{def} λ . let y = x{} in C_{α}^{±}(y, k, T)
C_{α}^{±}(x, k, ∃β. T) =^{def} C_{α}^{±}(x, k, T)
C_{α}^{±}(x, k, T_{1} → T_{2}) =^{def} λa. let r = x(C_{α}^{∓}(a, k, T_{1})) in C_{α}^{±}(r, k, T_{2})
C_{α}^{±}(x, k, {ℓ̃: T̃}) =^{def} let ỹ = #ℓ̃(x) in {ℓ̃= C_{α}^{±}(ỹ, k, T̃)}
C_{α}^{±}(x, k, bool) =^{def} x
C_{α}^{±}(x, k, int) =^{def} x

Figure 4: Naive Encoding

T (e : T) =^{def} let x = E(e) in G^{+}(x, T)
G^{±}(x, α) =^{def} x
G^{+}(x, ∀α. T) =^{def} λ . let y = x{} in G^{+}(y, T)
G^{−}(x, ∀α. T) =^{def} λ . let k = new⟨bits, γ⟩ in

let y = x{} in

let z = C_{α}^{−}(y, k, T) in G^{−}(z, T)

G^{+}(x, ∃α. T) =^{def} let k = new⟨bits, γ⟩ in

let z = C_{α}^{+}(x, k, T) in G^{+}(z, T)

G^{−}(x, ∃α. T) =^{def} G^{−}(x, T)
G^{±}(x, T_{1} → T_{2}) =^{def} λy. let a = G^{∓}(y, T_{1}) in

let r = xa in G^{±}(r, T_{2})

G^{±}(x, {ℓ̃: T̃}) =^{def} let ỹ = #ℓ̃(x) in {ℓ̃= G^{±}(ỹ, T̃)}
G^{±}(x, bool) =^{def} x
G^{±}(x, int) =^{def} x

Figure 5: Better Encoding

other hand, their naive encodings t_{1} = λf. f and

t_{2} = λf. λ . let f′ = f{} in λx. let = f′x in x

of type τ = ({} → bits → bits) → ({} → bits → bits) are distinguishable, say, to the observer

λF. ⌈F (λ . λx. ⌊true⌋_{⟨⟨bool⟩⟩}){}⌊false⌋_{⟨⟨bool⟩⟩}⌉_{⟨⟨bool⟩⟩}

of type τ → bool.

We can improve this naive encoding by wrapping all values coming from the outside of the encoding with encryption and decryption, and thereby forcing them to behave as they should, so that the decryption fails if they do not. For instance, in the example above, we can wrap the incoming function f like

t′_{2} = λf. let f = λ . (let k = new⟨bits, γ⟩ in
let f′ = f{} in λx. ⌈f′⌊x⌋_{k}⌉_{k})
in …

so that it does nothing but behaving as a function of type ∀α. α → α (cf. Example 13 in Section 3).

Formally, the better encoding T (e : T) is given in Figure 5. To protect type abstractions, the guard G^{±}(x, T) wraps incoming values of universal types (and, dually, outgoing values of existential types) by η-expanding the variable x along the type T and inserting encryption and decryption using a single secret password γ. Note that it never changes the types of the values that it wraps— for instance, in the example above, both t_{2} and t′_{2} have type τ—since it encrypts values of the type bits. This double encryption is not a waste of work: the first encryption (in the naive encoding) focused on well-typedness, while this second encryption (in this better encoding) aims at protection.

The “correctness” of this encoding can be formalized as follows.

Definition 14. (e_{1} =^{obs} e_{2} : T) ⟺^{def} (∅ ⊢ e_{1} : T) ∧ (∅ ⊢ e_{2} : T) ∧ [[e(e_{1})]]_{n} = [[e(e_{2})]]_{n} for any n and ∅ ⊢ e : T → bool.

Conjecture 15 (Full Abstraction). For any e_{1} and e_{2}, e_{1} =^{obs} e_{2} : T if and only if T (e_{1} : T) =^{obs}_{{γ}} T (e_{2} : T).

We leave it for future work to determine whether this conjecture is true or false. It is not straightforward for at least the following reasons:

• The target language is much more expressive than the source language. Consider, for instance, two functions F_{1} and F_{2} of type (int → int) → bool. Even if [[E(F_{1})f]] = true and [[E(F_{2}) f]] = false for some function f : int → int in the target language, we cannot conclude that F_{1} and F_{2} are inequivalent in the source language, because the function f might be undefinable. Neither does this imply that the encoding is not fully-abstract, because the “test” for the function f might also be undefinable.

• As far as we are aware, it remains an open problem to find any fully-abstract model of the polymorphic λ-calculus. Indeed, this was a hard problem even for the simply typed λ-calculus (with recursion) [14, pp. 212–215].

5 Related Work

The history of abstraction is as long as the history of programming languages. More than 27 years ago, Morris [18] informally presented the idea of protecting type abstractions by “sealing” values of the abstract types. Our encoding of polymorphism into cryptography in Section 4 can be regarded as a formalization of his idea.

Parametricity was first formalized by Reynolds [24] and further popularized by Wadler [26]. Although it was developed primarily in the setting of universal types, it can be applied easily to the setting of abstract types, because abstract types can be interpreted as existential types [16] and existential types can be encoded into universal types. Alternatively, parametricity can be extended directly to existential types [16, 20].

Abadi, Fournet, and Gonthier [4–6] have studied process calculi with security features such as authentication and private communication, and presented fully-abstract encodings of these systems into process calculi with cryptographic primitives (adaptations of the spi calculus [1, 7] and the join calculus [11, 12]). As their work itself shows, however, direct reasoning about such calculi is not easy. Boreale, De Nicola, and Pugliese’s theory [8] of trace-based equivalence in spi-calculus would mitigate the difficulty.

Zdancewic, Grossman, and Morrisett [28] developed a variant of the simply typed λ-calculus that preserves abstractions between multiple principals by distinguishing them through the syntax and the type system. They also gave a syntactic proof of (an adaptation of) parametricity in their calculus, using the small-step semantics of their calculus. It would be interesting to see whether and how their syntactic approach applies to our cryptographic framework and vice versa.

Heintze and Riecke [15] proposed a typed λ-calculus with information flow control, and proved a non-interference property (that a value of high security does not leak to any context of low security) by using a logical relation like parametricity as we did in Section 3. While their calculus is highlevel and uses static typing to keep secrecy, our calculus is low-level and uses dynamic encryption to hide information. As a result, it is forbidden in their scheme to, say, communicate a secret value over a public network, because the potential illegal access leads to a static type error.

Lillibridge and Harper [personal communication, July 2000] have independently developed a typed seal calculus quite similar to our cryptographic λ-calculus, and studied encodings of various constructs such as recursive types and polymorphism. The main thrust of their work is finding various alternative implementations of the seal primitives in terms of lower-level mechanisms such as exceptions and references and vice versa, rather than establishing techniques for reasoning about properties of programs in their calculus or protecting translations of high-level programs from lowlevel attackers.

6 Conclusion

We have (i) developed a λ-calculus with cryptography, (ii) adapted the parametricity theory of polymorphism to this calculus, and (iii) proposed an encoding of type abstraction into encryption. Besides investigating whether the encoding in Section 4.2 is fully abstract, at least the following issues will be interesting for further research.

Dynamic Typing and Polymorphism. It is known that dynamic typing does not to coexist well with polymorphism, because it breaks the type abstraction of polymorphism [3]. By implementing polymorphism with cryptography, however, it would be possible to allow the coexistence without losing the abstraction.

Aliasing and Information Hiding. It is also known that language features such as references cells and communication channels break type abstractions in subtle ways via aliasing [19]. For example, in an extension of the polymorphic λ-calculus with reference cells, a function

bogus id = Λα. let r : α option ref = ref(None) in
λx : α. case !r of None ⇒ (r := Some(x); x) | Some(y) ⇒ y

of type ∀α. α → α does not behave as the universal identity function, e.g. in the program let f : int → int = bogus id[int] in (f1, f2). It would be interesting to see how such phenomenon affects the information hiding that cryptography achieves.

Public-Key Cryptography. Although we have focused on shared-key cryptography so far, it is natural to wonder what public-key cryptography corresponds to in term of the type theory. A possible answer to this question might involve bounded quantification [9].

Conventional upper-bounded quantification corresponds roughly to digital signatures or trademarks [18]. If a package exports an abstract type α ≤ τ, then clients of the package can read α-values without help from the package, but only authorized code inside the package can create elements of α.

Conversely, a lower-bounded abstract type α ≥ τ roughly corresponds to a public key for encrypting values of type τ, because those who do not know the concrete type (i.e., the private key) can make a value of the type α (i.e., a ciphertext) but cannot use it. For example, using a “public key” α ≥ int, we can program transmission of a secret datum i : int to a “remote host” f : α → τ′ over a “public network” g : α → α, as f(g(coerce_{α}(i))). Because the type α is abstract, the function g must return the argument as it is, or just diverge and discard it (which a real network might also do).

Encoding Encryption into Type Abstraction. As the reverse of the encoding in Section 4, it also seems possible to implement encryption using type abstraction with some extensions such as references and dynamic typing. The following program in Standard ML illustrates this intuition, implementing public-key cryptography in terms of existential polymorphism. The exn type is used for dynamic typing and functor application is used for fresh key generation.

type ciphertext = exn exception DecryptionFailure

signature CRYPT = sig type plaintext

val encrypt : plaintext → ciphertext val decrypt : ciphertext → plaintext

end

functor Crypt (type plaintext) : CRYPT = struct type plaintext = plaintext

exception C of plaintext fun encrypt x = C x fun decrypt (C x) = x

| decrypt = raise DecryptionFailure

end

In this program, the functor Crypt takes the place of the fresh key generator, and the functions encrypt and decrypt play the role of the encryption and decryption keys, respectively. For example, it works as follows.

- structure IntCrypt1 = Crypt (type plaintext = int);

structure IntCrypt1 : CRYPT

- structure IntCrypt2 = Crypt (type plaintext = int);

structure IntCrypt2 : CRYPT

- val c = IntCrypt1.encrypt 123;

val c = C(-) : ciphertext

- IntCrypt1.decrypt c;

val it = 123 : IntCrypt1.plaintext

- IntCrypt2.decrypt c;

uncaught exception DecryptionFailure

Since it is possible to interpret the module system of Standard ML in terms of universal and existential polymorphism [25], it would be possible as well to encode cryptography into polymorphism (with some extensions) by generalizing this example.

Encoding Subtyping into Cryptography. As a variation on our encoding of parametric polymorphism into cryptography, we might consider implementing subtype polymorphism in terms of cryptography. The idea would be to encrypt the “private” part of a value. For instance, the coercion between a sub record type {b : bool, i : int} and a super record type {b : bool} can be simulated by encrypting and decrypting the second element i, e.g. like

let upcast = λr. {b = #_{b}(r), other = ⌊#_{i}(r)⌋_{k}} in let downcast = λr. {b = #_{b}(r), i = ⌈#_{other}(r)⌉_{k}} in downcast(f(upcast(r′))) where r′ is a record of type {b : bool, i : int}, f is a function of type {b : bool, other : bits} → {b : bool, other : bits}, and k is a key of type ⟨int⟩. This trick is reminiscent of the treatment of record subtyping in terms of row polymorphism [22, 27].

Concurrency and Distribution. Last but not least, we would like to consider adaptating these ideas to concurrent and/or distributed calculi with cryptographic primitives, such as Abadi and Gordon’s spi-calculus [1, 7]. This adaptation is challenging because the semantics of these languages is typically given in a small-step style, with no notion of “the value of a program.” Pierce and Sangiorgi’s treatment of parametric polymorphism in π-calculus [19], Boreale, De Nicola, and Pugliese’s theory of trace-based equivalence in spi-calculus [8], and Pitts and Ross’ work on big-step semantics of process calculi [21] may provide clues.

Acknowledgements

Some of the ideas presented here originated in a coffee-break conversation with Greg Morrisett. Martín Abadi offered useful pointers to related literature and insightful technical suggestions. Mark Lillibridge helped us understand the relation with his typed seal calculus and gave us valuable comments on a late draft of the manuscript. Atsushi Igarashi provided useful comments on a previous version of the paper.

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.

[2] Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Gordon D. Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237–268, 1991.

[3] Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111–130, 1995.

[4] Martín Abadi, Cédric Fournet, and Georges Gonthier. Secure implementation of chan-

    nel abstractions. Available at http://pauillac.inria.fr/~fournet/papers/secure-

implementation.ps.gz, 1999. Preliminary papers on this work appeared in Thirteenth Annual IEEE Symposium on Logic in Computer Science, pp. 74–88 and 1999 IEEE Symposium on Security and Privacy, pp. 105–116.

[5] Martín Abadi, Cédric Fournet, and Georges Gonthier. A top-down look at a secure message. In Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, 1999.

[6] Martín Abadi, Cédric Fournet, and Georges Gonthier. Authentication primitives and their compilation. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 302–315, 2000.

[7] Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999.

[8] Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic

processes, 1999. Available at ftp://rap.dsi.unifi.it/pub/papers/spi.ps.gz. An ex-

tended and revised version of the paper that appeared in 14th Annual IEEE Symposium on Logic in Computer Science, pp. 157–166.

[9] Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471–522, 1985.

[10] Danny Dolev, Cynthia Dwork, and Moni Naor. Non-malleable cryptography. Technical report, Weizmann Institute of Science, 2000. Avalable at http://www.wisdom.weizmann.ac.il:81

/Dienst/UI/2.0/Describe/ncstrl.weizmann il%2fCS95-27. A preliminary version of this

work appeared in Proceedings of the Twenty-Third Annual ACM Symposium on Theory of Computing, pp. 542–552.

[11] Cédric Fournet and Georges Gonthier. The reflexive CHAM and the join-calculus. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 372–385, 1996.

[12] Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, and Didier Rémy. A calculus of mobile agents. In CONCUR ’96, volume 1119, pages 406–421, 1996.

[13] Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[14] Carl A. Gunter. Semantics of Programming Languages. MIT Press, 1992.

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

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

[17] John C. Mitchell and Gordon D. Plotkin. Abstract types have existential types. ACM Transactions on Programming Languages and Systems, 10(3):470–502, 1988.

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

[19] Benjamin C. Pierce and Davide Sangiorgi. Behavioral equivalence in the polymorphic picalculus. Journal of the ACM, 47(3):531–586, 2000.

[20] Andrew M. Pitts. Existential types: Logical relations and operational equivalence. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 309–326. Springer-Verlag, 1998.

[21] Andrew M. Pitts and Joshua R. X. Ross. Process calculus based upon evaluation to committed form. Theoretical Computer Science, 195:155–182, 1998.

[22] Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press, 1994.

[23] John C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, pages 408–425. Springer-Verlag, 1974.

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

[25] Claudio V. Russo. Types For Modules. PhD thesis, University of Edinburgh, 1998. Available

at http://www.dcs.ed.ac.uk/home/cvr/ECS-LFCS-98-389.html.

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

[27] Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93(1):1–15, 1991.

[28] Steve Zdancewic, Dan Grossman, and Greg Morrisett. Principals in programming languages: A syntactic proof technique. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming, pages 197–207, 1999.