ECE/CS 598 AM: Cryptography with Ideal Functionalities

Spring 2021
Times: Tu Th 9:00am
Location: TBD
Instructor: Andrew Miller        Office hours: TBD
Teaching Assistant (unofficial): Surya Bakshi    Office hours: TBD

The Ideal Functionalities model (or “Universal Composability” (UC)) is considered the gold standard for defining security in many cryptographic tasks, such as multiparty computation and zero knowledge proofs. It can be considered a unification of property-based definition styles, where instead of describing one property at a time (i.e., one game for confidentiality, one game for integrity, and so on), we give a concrete instance of an idealized program that exhibits all these properties at once. While UC is broadly adopted in cryptography, it has yet to gain traction elsewhere in software engineering and in distributed systems. 

The aim of this course is to explore the connections between UC in cryptography versus in other domains like fault tolerant systems, and to see what UC can offer to software engineers concerned with implementing large systems and not just modelling small primitives. 

The course will give a self contained introduction to UC, making use of our research software prototypes, Haskell-SaUCy and Python-SaUCy, which are programming frameworks that implement UC. We’ll then survey the UC-based cryptography literature for a range of cryptographic tasks, including well known applications like key exchange and multiparty computation, as well as more challenging cases like non-interactive primitives and smart contract blockchain protocols. Using the software frameworks as a secret weapon, we’ll try to improve on and simplify prior UC proofs.

The course is built on recent research efforts to provide software tools for UC, ILC (PLDI’19) and is supported by NSF grants #1801321 “Automated Support for Writing High-Assurance Smart Contracts” and #1943499 “CAREER: Composable Programming Abstractions for Secure Distributed Computing and Blockchain Applications.”

Prerequisites:

It is not necessary to have background knowledge of Ideal Functionalities and UC. However, some mathematical maturity and familiarity with cryptography is expected, such as experience writing traditional game-based security proofs.

Tentative Schedule:

Week 1: 

– Intro

– Interactive Turing Machines

Reading: Haskell-SaUCy or Python-SaUCy

Week 2: 

– The UC Emulation definition

Reading: Canetti UC

– Modelling protocols with functionalities: Commitments using Random Oracles

Week  3: 

– More examples: an MPC protocol with preprocessing

Reading: Shreyas Gandlur bsc thesis

– More examples: commitments based on trapdoor cryptography

Week 4: 

– Impossibility proofs: No commitments in the plain model

Reading: Paper https://eprint.iacr.org/2001/055.pdf

– In rigorous detail: Import and polynomial runtime

NomosUC

Week 5: 

– Student presentation 1

– Extensions: Asynchronous channels

Reading: Bracha broadcast

Week 6:

– Student presentation 2

– Real world application: Blockchain smart contracts and payment channels

Week 7:

Student presentations 3-4

Week 8:

Student presentations 5-6

Week 9:

– Guest Lecture

– Student presentations 7

Week 10:

– Student presentations 8

– Guest lecture

Week 11:

Student presentations 9-10

Week 12:

Wrap up

Week 13:

Project presentations

Week 14:

Project presentations

 

 

Grading:
40%: The course will include a combination of instructor lectures and student presentations of papers from the UC reading list. Students will also contribute scribe notes that may be included in future versions of this course.
Presentation: 25%
Scribe notes: 5%
Paper reviews: 10%

20%: Programming projects based on Python-SaUCy or Haskell-SaUCy intended to find new ways to understand UC proofs, to simplify UC proofs, and to test UC proofs
Implement an ideal functionality model from a reading list paper: 10%
Implement a simulator and test from a paper: 10%

40%: Final project centered around creating a UC model and proof for an existing (or new) cryptographic protocol, including a software artifact based on the UC model. (Note: It is not necessary to create a new research contribution for this project, a new proof of an existing protocol is fine)
– Project Proposal:  10%
– Project Checkpoints (2x) 30%
– Written report 30%
– Presentation 30%

Textbooks / references:
– Programmer’s Guide to Universal Composability (the documentation for Haskell-SaUCy and Python-SaUCy, developed along the way as course notes).
Haskell-SaUCy https://github.com/amiller/haskell-saucy
Python-SaUCy https://github.com/sbaks0820/uc-contracts
– The 7th version of the Universal Composability paper by Ran Centti is an authoritative reference for the underlying theoretical framework
    Canetti 2000 https://eprint.iacr.org/2000/067
– Existing introductions to UC include a video lecture series Canetti’s video lecture series
https://www.bu.edu/macs/workshops/uc-hackathon/

Detailed Topics and Tentative Reading list

Introduction to Universal Composability
– Interactive Turing Machines model
– Universal Composability with static corruptions
– Dummy Lemma
– Composition Theorem
– Random Oracle model and folklore commitment
– Impossibility of Commitments in the Plain Model
https://eprint.iacr.org/2001/055.pdf
– CRS model and commitments another way
– JointUC and GlobalUC
CR02 https://eprint.iacr.org/2002/047
CDPW06 http://www.cs.cornell.edu/~rafael/papers/cdpw.pdf
– Most Functionalities are complete or nothing

 

Applications I
– Multiparty Computation / Secure Function Evaluation
– Key Exchange Needham-Schroeder-Lowe https://eprint.iacr.org/2002/059
– PAKE   https://link.springer.com/chapter/10.1007/978-3-030-56784-2_10
– Rational Protocol Design https://eprint.iacr.org/2013/496.pdf
– Blockchain application models
Lotteries, Channels
– Voting https://eprint.iacr.org/2002/002.pdf
– Symmetric Encryption https://eprint.iacr.org/2009/055.pdf

Formal Models of UC

– Polynomial runtime and Import Tokens

– EasyUC https://eprint.iacr.org/2019/582

– IPDL  https://eprint.iacr.org/2021/147.pdf

– Symbolic UC  https://kodu.ut.ee/~unruh/publications/symbolic-uc.html

– IITMs, GNUc  https://eprint.iacr.org/2013/025.pdf https://eprint.iacr.org/2011/303.pdf

– Abstract Cryptography  https://crypto.ethz.ch/publications/files/MauRen11.pdf

– NomosUC 

– Probabilistic Termination https://www.iacr.org/archive/crypto2016/98160232/98160232.pdf

– Reentrant functionalities 

 

Applications II

– Bounded delay channels and eventual delivery guarantees  https://eprint.iacr.org/2016/208.pdf

– Synchronous protocols and F_clock https://www.iacr.org/archive/tcc2013/77850475/77850475.pdf

– Broadcast protocols https://dl.acm.org/doi/abs/10.1145/1993806.1993832

– Blockchain backbone models https://dl.acm.org/doi/pdf/10.1145/3243734.3243848

– Trusted hardware enclaves https://www.iacr.org/archive/eurocrypt2017/10210256/10210256.pdf

 

Universal Composability and Smart Contract Protocols

– Hawk and the smart contract model https://eprint.iacr.org/2015/675.pdf

– General state channels https://dl.acm.org/doi/abs/10.1145/3243734.3243856

– Perun https://ieeexplore.ieee.org/document/8835315

– Bitcoin model https://eprint.iacr.org/2019/778.pdf

– Financially Fair MPC https://eprint.iacr.org/2015/574

– Instantaneous Poker https://www.iacr.org/archive/asiacrypt2017/106240274/106240274.pdf