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

10:00 - 11:00: PLDI Research Papers - Type Systems II at 224AB
Chair(s): Jeffrey S. FosterTufts University
pldi-2019-papers10:00 - 10:20
Kevin Liao, Matthew HammerNone, Andrew MillerUniversity of Illinois at Urbana-Champaign, USA
pldi-2019-papers10:20 - 10:40
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
pldi-2019-papers10:40 - 11:00
Konstantinos MamourasUniversity of Pennsylvania, Caleb StanfordUniversity of Pennsylvania, Rajeev AlurUniversity of Pennsylvania, Zachary G. IvesUniversity of Pennsylvania, Val TannenUniversity of Pennsylvania, USA
Media Attached