Logical relations for encryption (extended abstract)

Eijiro Sumii; B. C. Pierce

doi:10.1109/CSFW.2001.930151

Logical relations for encryption (extended abstract)

Eijiro Sumii, B. C. Pierce

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

22 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Proceedings of the Computer Security Foundations Workshop
Pages	256-269
Number of pages	14
DOIs	https://doi.org/10.1109/CSFW.2001.930151
Publication status	Published - 2001 Oct 1
Externally published	Yes
Event	14th IEEE Computer Security Foundations Workshop (CSFW-14) - Cape Brenton, NS, United States Duration: 2001 Jun 11 → 2001 Jun 13

Publication series

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

Other

Other	14th IEEE Computer Security Foundations Workshop (CSFW-14)
Country/Territory	United States
City	Cape Brenton, NS
Period	01/6/11 → 01/6/13

ASJC Scopus subject areas

Software

Access to Document

10.1109/CSFW.2001.930151

Cite this

@inproceedings{18567751b1724308a1d289564b025cae,

title = "Logical relations for encryption (extended abstract)",

abstract = "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.",

author = "Eijiro Sumii and Pierce, {B. C.}",

year = "2001",

month = oct,

day = "1",

doi = "10.1109/CSFW.2001.930151",

language = "English",

isbn = "0769511473",

series = "Proceedings of the Computer Security Foundations Workshop",

pages = "256--269",

booktitle = "Proceedings of the Computer Security Foundations Workshop",

note = "14th IEEE Computer Security Foundations Workshop (CSFW-14) ; Conference date: 11-06-2001 Through 13-06-2001",

}

TY - GEN

T1 - Logical relations for encryption (extended abstract)

AU - Sumii, Eijiro

AU - Pierce, B. C.

PY - 2001/10/1

Y1 - 2001/10/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0034837908&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0034837908&partnerID=8YFLogxK

U2 - 10.1109/CSFW.2001.930151

DO - 10.1109/CSFW.2001.930151

M3 - Conference contribution

AN - SCOPUS:0034837908

SN - 0769511473

T3 - Proceedings of the Computer Security Foundations Workshop

SP - 256

EP - 269

BT - Proceedings of the Computer Security Foundations Workshop

T2 - 14th IEEE Computer Security Foundations Workshop (CSFW-14)

Y2 - 11 June 2001 through 13 June 2001

ER -

Logical relations for encryption (extended abstract)

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this