paper announcement: Relating Cryptography and Polymorphism

We are pleased to announce our paper "Relating Cryptography and
Polymorphism", available at:


Comments welcome.  Enjoy,

        Eijiro Sumii  
        Benjamin Pierce


		Relating Cryptography and Polymorphism

		    Benjamin Pierce   Eijiro Sumii
		      University of Pennsylvania


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

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