The theory of _relational parametricity_ and its _logical relations_
proof technique are powerful tools for reasoning about information
hiding in the polymorphic lambda-calculus.  We investigate the
application of these tools in the security domain by defining a
_cryptographic lambda-calculus_---an extension of the standard
lambda-calculus with primitives for encryption, decryption, and key
generation---and introducing logical relations for this calculus that
can be used to prove behavioral equivalences between programs
involving 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.