Logical relations for encryption (extended abstract)

Eijiro Sumii, B. C. Pierce

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Citations (Scopus)


The theory of relational parametricity and its logical relations proof technique are powerful tools for reasoning about information hiding in the polymorphic λ-calculus. We investigate the application of these tools in the security do-main by defining a cryptographic λ-calculus - an extension of the standard simply typed λ-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 that rely on 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.

Original languageEnglish
Title of host publicationProceedings of the Computer Security Foundations Workshop
Number of pages14
Publication statusPublished - 2001 Oct 1
Externally publishedYes
Event14th IEEE Computer Security Foundations Workshop (CSFW-14) - Cape Brenton, NS, United States
Duration: 2001 Jun 112001 Jun 13

Publication series

NameProceedings of the Computer Security Foundations Workshop
ISSN (Print)1063-6900


Other14th IEEE Computer Security Foundations Workshop (CSFW-14)
Country/TerritoryUnited States
CityCape Brenton, NS

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Logical relations for encryption (extended abstract)'. Together they form a unique fingerprint.

Cite this