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, \emph{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.