Paper 2019/402
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.
Metadata
- Available format(s)
-
PDF
- 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
- 2019-04-22: received
- See all versions
- Short URL
- https://ia.cr/2019/402
- License
-
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},
url = {https://eprint.iacr.org/2019/402}
}