Tue 25 Jun 2019 10:00 - 10:20 at 224AB - Type Systems II Chair(s): Jeffrey S. Foster

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.

Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

10:00 - 11:00
Type Systems IIPLDI Research Papers at 224AB
Chair(s): Jeffrey S. Foster Tufts University
ILC: A Calculus for Composable, Computational Cryptography
PLDI Research Papers
Kevin Liao , Matthew Hammer None, Andrew Miller University of Illinois at Urbana-Champaign, USA
Proving Differential Privacy with Shadow Execution
PLDI Research Papers
Yuxin Wang , Zeyu Ding Pennsylvania State University, USA, Guanhong Wang Pennsylvania State University, USA, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University, Danfeng Zhang Pennsylvania State University
Media Attached
Data-Trace Types for Distributed Stream Processing Systems
PLDI Research Papers
Konstantinos Mamouras University of Pennsylvania, Caleb Stanford University of Pennsylvania, Rajeev Alur University of Pennsylvania, Zachary G. Ives University of Pennsylvania, Val Tannen University of Pennsylvania, USA
Media Attached