ECE/CS 598 AM: Cryptography with Ideal Functionalities

Spring 2022
Times
: Tu Th 9:30am – 10:50am
Location: 2015 Electrical & Computer Eng Bldg (Jan 25 and later)
Zoom link for synchronous lectures (see Piazza)
Piazza: piazza.com/illinois/spring2022/ece598am

Instructor: Andrew Miller        Office hours: Thursdays 3pm-4pm, and by appointment
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 m

any 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.

Reference texts (all free available online):
Security and Composition of Cryptographic Protocols: A Tutorial (Canetti 2006). https://eprint.iacr.org/2006/465
– Pragmatic MPC http://securecomputation.org/
– Python-SaUCy https://github.com/amiller/ece598-uc-contracts
– Course slides and course notes from Canetti 2004 http://courses.csail.mit.edu/6.897/spring04/materials.html

Schedule:

Week 1: 

– [Tuesday] Intro to the Course, Intro to UC   (slides) (Scribe Notes)
Scribe: Mingjia Huo

– [Thursday] UC in More Detail, Commitments with Random Oracle (slides)

Reading:
– Real/Ideal from Ch. 2.3 of Pragmatic MPC  http://securecomputation.org/docs/ch2-definingmpc.pdf
– Recap some cryptography, such as Garbled Circuits protocol (Ch 3) of Pragmatic MPC
– Canetti’s UC tutorial (Ch 1-3)
– Set up the Python-SaUCy (and/or Haskell-SaUCy) development environment

Week 2: 

– [Tuesday] UC Security in more detail  (Slides) (Scribe Notes)
Finish RO Commitment, Composition Theorem, ITMs
Scribe: Peiyao Sheng

– [Thursday] ITMs in more detail. (Slides) (Scribe Notes)
Scribe: Bolton Bailey

Reading:
– Canetti’s UC tutorial (Ch 4-5)
– Scribe notes L1-2 from Canetti Spring04

– Canetti’s proof of Universal Composability from https://eprint.iacr.org/2000/067

Week  3: 

– [Tuesday] Efficient Commitments based on CRS   (Slides)
Scribe: Milind Kumar

– [Thursday] Adversarial Scheduling, Arithmetic Black Box (Slides)
Scribe: Nerla Jean-Louis

Reading:
– Improving UC commitments paper https://eprint.iacr.org/2013/123.pdf
MPC protocol background (Beaver protocol from Pragmatic MPC) 

 

Week 4: 

– [Tuesday] Impossibility Proof of Commitments in Plain Model (Slides) (Scribe Notes)
Scribe: Tzu-Bin Yan
– [Thursday] Multiparty Computation (Slides)
Scribe: Yuechun Yang

Reading:
– Impossibility proof from https://eprint.iacr.org/2001/055.pdf
– 3.2 from Canetti paper 3.2 Polynomial time ITMs and parameterized systems
– Polynomial Runtime and Composability  https://eprint.iacr.org/2009/023.pdf

Week 5: 

– [Tuesday] In more detail: Import and polynomial runtime. Eventual Delivery channels
Scribe: 

– [Thursday] Finishing MPC, Polynomial Runtime (Slides)
Scribe: Tom Yurek

Reading: Bracha broadcast

** CRS-based Commitments programming project due ** 

== Tentative Schedule: ==

Week 6:

– [Tuesday] Student presentation 1
Presenter: Fangqi Han:    Synchronous Protocols and F_Clock (eprint)
Scribe: Mingjia Huo

 

– [Thursday] Student presentation 2
Presenter: Nerla Jean-Louis:   Systemizing Ballot Privacy in E-Voting  (eprint)
Scribe: Jasleen Malvai

***Project Proposals Due***

Week 7:

– [Tuesday Mar 1] Student presentations 3
Presenter: Tzu-Bin Yan:  Enforcing confinement in Distributed Storage (eprint)
Scribe: Amit Agarwal

– [Thursday] Student presentation 2
Presenter:  Presenter: Nerla Jean-Louis:   Systemizing Ballot Privacy in E-Voting  (eprint)

Week 8:

– [Tuesday Mar 8]: Student presentations 5
Presenter: Amit Agarwal:  Practical UC with Global Random Oracle

– [Thursday] Reliable Broadcast (Bracha’s Protocol) (slides)
Presenter: Mingjia APECS https://dl.acm.org/doi/pdf/10.1145/3460120.3484804
Scribe: Fangqi Han
– Discussion

SPRING BREAK

Week 9:

– [Tuesday Mar 22] Student presentation 6
Presenter: Mingjia APECS https://dl.acm.org/doi/pdf/10.1145/3460120.3484804

 

– [Thursday] Student presentations 7

Presenter: Yunqi Li: C0C0
Scribe: Peiyao Sheng

Week 10:

– [Tuesday Mar 29] Student presentations 8
Presenter: Peiyao Sheng: Adaptively secure broadcast, revisited

– [Thursday Mar 31] Lecture:  UC Secure Signatures  https://eprint.iacr.org/2003/240.pdf

(Andrew’s slides)

Project Checkpoints Due

Week 11:

Student presentations 9-10
– [Tuesday Apr 5]

Office hours! We can discuss the programming assignment

– [Thursday]
Presenter: Bolton Bailey:   Perun

Programming Project strictly due!

Week 12:

Student Presentations
– [Tuesday Apr 12]  
Presenter:   Andrew Miller and Surya Bakshi.

– The simplest Payment Channel in UC.  (slides)
Background reading: Payment Channels in UC blogpost
– Explanation of Sprites State Channels with Surya Bakshi.

– [Thursday]
Presenter:  Jasleen: Probabilistic Termination in UC 

Week 13:

– [Tuesday Apr 19]  class cancelled, prof sick

– [Thursday Apr 21] Most functionalities are either complete or useless (slides)

Week 14:

– [Tuesday Apr 26] Guest Lecture – Kristina Hostáková (ETH Zurich)

– [Thursday Apr 28] Guest Lecture – Thomas Kerber (IOHK)

Week 15

– [Tuesday Mar 3] 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%

More references and resources

– Existing introductions to UC include a video lecture series Canetti’s video lecture series
https://www.bu.edu/macs/workshops/uc-hackathon/

– 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

– 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

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