[Prev][Next][Index][Thread]
paper announcement: Relating Cryptography and Polymorphism
We are pleased to announce our paper "Relating Cryptography and
Polymorphism", available at:
http://www.yl.is.s.u-tokyo.ac.jp/~sumii/pub/infohide.ps.gz
Comments welcome. Enjoy,
Eijiro Sumii
Benjamin Pierce
======================================================================
Relating Cryptography and Polymorphism
Benjamin Pierce Eijiro Sumii
University of Pennsylvania
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
lambda-calculus_, a simply typed lambda-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 lambda-calculus.
This theory is useful for proving equivalences in our calculus; for
instance, it implies the 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
lambda-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.