### ILC: A Calculus for Composable, Computational Cryptography

Kevin Liao, Matthew A. Hammer, and Andrew Miller

##### 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 pi-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.

Available format(s)
Category
Foundations
Publication info
Published elsewhere. MAJOR revision.PLDI 2019
DOI
10.1145/3314221.3314607
Keywords
provable securityuniversal composabilityprocess calculustype systems
Contact author(s)
kevliao @ mit edu
History
2020-11-07: revised
See all versions
Short URL
https://ia.cr/2019/402

CC BY

BibTeX

@misc{cryptoeprint:2019/402,
author = {Kevin Liao and Matthew A.  Hammer and Andrew Miller},
title = {ILC: A Calculus for Composable, Computational Cryptography},
howpublished = {Cryptology ePrint Archive, Paper 2019/402},
year = {2019},
doi = {10.1145/3314221.3314607},
note = {\url{https://eprint.iacr.org/2019/402}},
url = {https://eprint.iacr.org/2019/402}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.