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
Times are displayed in time zone: Tijuana, Baja California change

10:00 - 11:00: Type Systems IIPLDI Research Papers at 224AB
Chair(s): Jeffrey S. FosterTufts University
10:00 - 10:20
PLDI Research Papers
Kevin Liao, Matthew HammerNone, Andrew MillerUniversity of Illinois at Urbana-Champaign, USA
10:20 - 10:40
PLDI Research Papers
Yuxin Wang, Zeyu DingPennsylvania State University, USA, Guanhong WangPennsylvania State University, USA, Daniel KiferDept. of Computer Science and Engineering, Penn State University, Danfeng ZhangPennsylvania State University
Media Attached
10:40 - 11:00
PLDI Research Papers
Konstantinos MamourasUniversity of Pennsylvania, Caleb StanfordUniversity of Pennsylvania, Rajeev AlurUniversity of Pennsylvania, Zachary G. IvesUniversity of Pennsylvania, Val TannenUniversity of Pennsylvania, USA
Media Attached