ECE/CS 598 AM: Cryptography with Ideal Functionalities

Spring 2022
: Tu Th 9:30am – 10:50am
Location: 2015 Electrical & Computer Eng Bldg (Jan 25 and later)
Zoom link for synchronous lectures (see Piazza)

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


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).
– Pragmatic MPC
– Python-SaUCy
– Course slides and course notes from Canetti 2004


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)

– Real/Ideal from Ch. 2.3 of Pragmatic MPC
– 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

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

– Canetti’s proof of Universal Composability from

Week  3: 

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

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

– Improving UC commitments paper
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

– Impossibility proof from
– 3.2 from Canetti paper 3.2 Polynomial time ITMs and parameterized systems
– Polynomial Runtime and Composability

Week 5: 

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

– [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
Scribe: Fangqi Han
– Discussion


Week 9:

– [Tuesday Mar 22] Student presentation 6
Presenter: Mingjia APECS


– [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

(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


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

– The 7th version of the Universal Composability paper by Ran Centti is an authoritative reference for the underlying theoretical framework
    Canetti 2000

– Programmer’s Guide to Universal Composability (the documentation for Haskell-SaUCy and Python-SaUCy, developed along the way as course notes).

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
– CRS model and commitments another way
– JointUC and GlobalUC
– Most Functionalities are complete or nothing


Applications I
– Multiparty Computation / Secure Function Evaluation
– Key Exchange Needham-Schroeder-Lowe
– Rational Protocol Design
– Blockchain application models
Lotteries, Channels
– Voting
– Symmetric Encryption

Formal Models of UC

– Polynomial runtime and Import Tokens

– EasyUC


– Symbolic UC


– Abstract Cryptography

– NomosUC 

– Probabilistic Termination

– Reentrant functionalities 


Applications II

– Bounded delay channels and eventual delivery guarantees

– Synchronous protocols and F_clock

– Broadcast protocols

– Blockchain backbone models

– Trusted hardware enclaves


Universal Composability and Smart Contract Protocols

– Hawk and the smart contract model

– General state channels

– Perun

– Bitcoin model

– Financially Fair MPC

– Instantaneous Poker