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 -