Relating Cryptography and Polymorphism
Benjamin C. Pierce, Eijiro Sumii · 2000
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