Cryptology ePrint Archive: Report 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.

Category / Keywords: foundations / provable security, universal composability, process calculus, type systems

Original Publication (with major differences): PLDI 2019

Date: received 16 Apr 2019, last revised 7 Nov 2020

Contact author: kevliao at mit edu

Available format(s): PDF | BibTeX Citation

Version: 20201107:191124 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]