ILC: A calculus for composable, computational cryptography

Kevin Liao, Matthew A. Hammer, Andrew Miller

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

Abstract

The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness. In this paper, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC-interactive Turing machines (ITMs)-by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC's strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy.

Original languageEnglish (US)
Title of host publicationPLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsKathryn S. McKinley, Kathleen Fisher
PublisherAssociation for Computing Machinery
Pages640-654
Number of pages15
ISBN (Electronic)9781450367127
DOIs
StatePublished - Jun 8 2019
Event40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 - Phoenix, United States
Duration: Jun 22 2019Jun 26 2019

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
CountryUnited States
CityPhoenix
Period6/22/196/26/19

Fingerprint

Turing machines
Cryptography
Network protocols
Concretes
Chemical analysis

Keywords

  • Process calculus
  • Provable security
  • Type systems
  • Universal composability

ASJC Scopus subject areas

  • Software

Cite this

Liao, K., Hammer, M. A., & Miller, A. (2019). ILC: A calculus for composable, computational cryptography. In K. S. McKinley, & K. Fisher (Eds.), PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 640-654). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery. https://doi.org/10.1145/3314221.3314607

ILC : A calculus for composable, computational cryptography. / Liao, Kevin; Hammer, Matthew A.; Miller, Andrew.

PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ed. / Kathryn S. McKinley; Kathleen Fisher. Association for Computing Machinery, 2019. p. 640-654 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

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

Liao, K, Hammer, MA & Miller, A 2019, ILC: A calculus for composable, computational cryptography. in KS McKinley & K Fisher (eds), PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Association for Computing Machinery, pp. 640-654, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, United States, 6/22/19. https://doi.org/10.1145/3314221.3314607
Liao K, Hammer MA, Miller A. ILC: A calculus for composable, computational cryptography. In McKinley KS, Fisher K, editors, PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery. 2019. p. 640-654. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/3314221.3314607
Liao, Kevin ; Hammer, Matthew A. ; Miller, Andrew. / ILC : A calculus for composable, computational cryptography. PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. editor / Kathryn S. McKinley ; Kathleen Fisher. Association for Computing Machinery, 2019. pp. 640-654 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).
@inproceedings{dc81d3fea2ed427aa7b6fb766ab453b7,
title = "ILC: A calculus for composable, computational cryptography",
abstract = "The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness. In this paper, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC-interactive Turing machines (ITMs)-by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC's strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy.",
keywords = "Process calculus, Provable security, Type systems, Universal composability",
author = "Kevin Liao and Hammer, {Matthew A.} and Andrew Miller",
year = "2019",
month = "6",
day = "8",
doi = "10.1145/3314221.3314607",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "640--654",
editor = "McKinley, {Kathryn S.} and Kathleen Fisher",
booktitle = "PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation",

}

TY - GEN

T1 - ILC

T2 - A calculus for composable, computational cryptography

AU - Liao, Kevin

AU - Hammer, Matthew A.

AU - Miller, Andrew

PY - 2019/6/8

Y1 - 2019/6/8

N2 - The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness. In this paper, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC-interactive Turing machines (ITMs)-by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC's strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy.

AB - The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness. In this paper, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC-interactive Turing machines (ITMs)-by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC's strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy.

KW - Process calculus

KW - Provable security

KW - Type systems

KW - Universal composability

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

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

U2 - 10.1145/3314221.3314607

DO - 10.1145/3314221.3314607

M3 - Conference contribution

AN - SCOPUS:85067645049

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 640

EP - 654

BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

A2 - McKinley, Kathryn S.

A2 - Fisher, Kathleen

PB - Association for Computing Machinery

ER -