You are looking at a specific version 20201107:191124 of this paper. See the latest version.

Paper 2019/402

ILC: A Calculus for Composable, Computational Cryptography

Kevin Liao and 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
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.