UC/EasyUC Summer School

Dates: August 11-14, 2025
Location: Duan Family Center for Computing & Data Sciences at Boston University (665 Comm Ave) on the 16th floor in room 1646. The building is accessible via public transit: take the MBTA Green Line B to the BU East stop. While parking at BU is not recommended, there are some visitor parking lots.
Registration: Free, but required via this Google form. Important note: As of August 3, we have reached our in-person capacity for the summer school. Any further registrations will be interpreted as Zoom only (unless space opens up via cancellations, in which case we will notify registrants).

Since its first draft formulation 25 years ago, the Universally Composable (UC) security framework has been used to specify and analyze the security of cryptographic protocols in multiple scenarios, quickly becoming the gold standard for cryptographic security, while also being used for specifying and analyzing non-cryptographic computing systems. The framework eventually matured with a definitive exposition in the Journal of the ACM.

In the last decade and a half, there has been a great deal of interest in mechanizing proofs of cryptographic security using proof assistants, such as EasyCrypt. Even more recently, researchers have turned their attention to mechanizing proofs of UC Security. One such effort is EasyUC, which provides a domain specific language (DSL) for UC. The implementation of the UC DSL provides a typechecker that catches many errors that may lurk in paper-and-pencil UC models, an interpreter that lets UC designers experiment with their models, and a translator into EasyCrypt, where sequence of games security proofs can be carried out. There is also a graphical user interface for generating skeleton UC DSL code.

From August 11-14 2025, the originator of UC, Ran Canetti, and the designers and developers of EasyUC including Alley Stoughton are joining forces to hold a summer school at the Duan Family Center for Computing & Data Sciences of Boston University. The summer school will feature lectures on both UC and EasyUC, as well as tutorial sessions in which participants can learn to use the EasyUC tools and/or create paper-and-pencil UC models and analyses. There will be breakout sessions on more advanced topics, including advances in the theory and application of UC, using the UC DSL for modeling system security, and carrying out sequence of games proofs in EasyUC.

The school welcomes a broad range of participants who will benefit from exposure to a variety of aspects of UC and its mechanization via EasyUC, as we bring these two research areas together for four days of learning, collaboration and hands-on practice.

Logistics

The is no fee for attending the summer school, but neither are we able to offer support for travel or accommodation. We will however enable synchronous online participation via Zoom, as well as asynchronous viewing of recordings of lectures.

For those attending in person, the lectures and breakout sessions will be held in the Duan Family Center for Computing & Data Sciences. A number of fast and slow food restaurants are within easy walking distance of the venue. We will have coffee and light snacks available at the venue.

Participants must register for the summer school via this web link. If you anticipate wanting to give a short talk on the third of fourth day of the school, please indicate this on the registration form.

You can also email the organizers at: uc-easyuc-summer-school+owners@googlegroups.com

There are a number of hotels near the summer school venue, but one good option is the Hyatt Regency Boston/Cambridge, which is located at 575 Memorial Drive in Cambridge. Here is the booking link.

Schedule

The schedule for Monday and Tuesday is final, and the schedule for Wednesday and Thursday is currently tentative. Some of the completed talks have slides available.

Monday, August 11

9:20-9:30 Alley Stoughton – Welcome (slides)
9:30-10:45 Ran Canetti – UC I: The basic model (slides)
10:45-11:15 Break
11:15-12:30 Ran Canetti – UC II: The general model. ITMs (syntax and semantics), protocols, protocol emulation, and realizing ideal functionalities (slides)
12:30-1:45 Lunch
1:45-3:00 Alley Stoughton – EasyUC Introduction (slides)
3:00-3:30 Break
3:30-4:45 Alley Stoughton – Modeling UC Designs Using the UC DSL (slides)
4:45-5:00 Break
5:00-5:30 End of Day Discussion

Tuesday, August 12

9:30-10:45 Ran Canetti – UC III: The general model, continued. The UC operation and theorem, useful conventions, example ideal functionalities (slides)
10:45-11:15 Break
11:15-12:30 Ran Canetti – UC IV: More ideal functionalities, global functionalities, and non-interactive functionalities (slides)
12:30-1:45 Lunch
1:45-3:00 Alley Stoughton – Experimenting with UC Designs using the UC DSL Interpreter (slides)
3:00-3:30 Break
3:30-4:45 Michael Clark – Graphical Design of UC DSL Models (slides)
4:45-5:00 Break
5:00-5:30 End of Day Discussion

Wednesday, August 13

9:40-10:05 Nikki Sigurdson – Countersign: Ultra-private P2P Authentication for Bitcoin
10:05-10:30 Anitha Gollamudi – ILA: Correctness via Type Checking for Fully Homomorphic Encryption
10:30-11:00 Break
11:00-12:15 Alley Stoughton – Sequences of Games Security Proofs in EasyCrypt (slides)
12:15-1:30 Lunch
1:30-3:00 Michael Clark and Tony Pierce – Tutorial: Using the UCPACT Web Application
3:00-3:30 Break
3:30-4:45 Ran Canetti – UC V (slides)

Thursday, August 14

9:30-11:00 Robert Graham – Modeling the Needham-Schroeder Public-Key Protocol in EasyUC (slides)
11:00-11:30 Break
11:30-12:45 Megan Chen – UC Security in the Global ROM (slides)
12:45-2:00 Lunch
2:00-3:00 Tomislav Petrovic – UC DSL to EasyCrypt Translator (slides)
3:00-3:30 Break
3:30-4:45 Alley Stoughton – Working With Malicious Parties in Real/Ideal Security Proofs in EasyCrypt (slides)

Selected Talk Abstracts

Robert Graham – Modeling the Needham-Schroeder Public-Key Protocol in EasyUC

Abstract: The Needham-Schroeder Public-Key Protocol is a classic example of a protocol that works fine in isolation but not when composed with itself. This talk presents the protocol, what security goals it is intended to achieve and how it fails to achieve them. It then presents two EasyUC models and discusses some of the difficulties given the current tooling.

Riverside Research – Tutorial: Using the UCPACT Web Application

Abstract: Want to get some help using the web application? We’ll have multiple developers of the tool on hand to answer questions, help you get it installed, help you build out a model, and answer any questions you may have. Please try to get it installed following the instructions on
github.com/riversideresearch/ucpact prior to the session. We recommend starting using single-user mode with the default profile. It would also be helpful to come with a protocol in mind to create a model around.

Anitha Gollamudi – ILA: Correctness via Type Checking for Fully Homomorphic Encryption

Abstract: RLWE-based Fully Homomorphic Encryption (FHE) schemes add some small noise to the message during encryption. The noise accumulates with each homomorphic operation. When the noise exceeds a critical value, the FHE circuit produces an incorrect output. This makes developing FHE applications quite subtle, as one must closely track the noise to ensure correctness. However, existing libraries and compilers offer limited support to statically track the noise. Additionally, FHE circuits are also plagued by wraparound errors that are common in finite modulus arithmetic. These two limitations of existing compilers and libraries make FHE applications too difficult to develop with confidence.

In this work, we present a correctness-oriented IR, Intermediate Language for Arithmetic circuits, for type-checking circuits intended for homomorphic evaluation. Our IR is backed by a type system that tracks low-level quantitative bounds (e.g., ciphertext noise) without using the secret key. Using our type system, we identify and prove a strong functional correctness criterion for ILA circuits. Additionally, we have designed ILA to be maximally general: our core type system does not directly assume a particular FHE scheme, but instead axiomitizes a model of FHE. We instantiate this model with the exact FHE schemes (BGV, BFV and TFHE), and obtain functional correctness for free.

We implement a concrete type checker ILA, parameterized by the noise estimators for three popular FHE libraries (OpenFHE, SEAL and TFHE-rs). Additionally, our novel algorithm for inferring the placement of modulus switching, a common noise management operation, uses the ILA type checker as a validation framework to ensure the correctness of the optimization. Evaluation shows that ILA type checker is sound (always detects noise overflows), practical (noise estimates are tight) and efficient.

Joint work with Tarakaram Gollamudi (Independent) and Joshua Gancher (Northeastern).

Alley Stoughton – Sequences of Games Security Proofs in EasyCrypt

Abstract: Security proofs in EasyCrypt generally follow the sequence of games — also known as game hopping — approach. We’ll dive into an example of such a proof, first at a high level, and then surveying the actual EasyCrypt code.

Tomislav Petrovic – UC DSL to EasyCrypt Translator

Abstract: We’ll give an introduction to the features and use of the translator from the UC DSL into EasyCrypt.

Alley Stoughton – Working With Malicious Parties in Real/Ideal Security Proofs in EasyCrypt

Abstract: We’ll consider an example of how we can work with malicious parties in real/ideal security proofs in EasyCrypt. The examples uses security via indirection, making use of a trusted computing base providing indirect access to objects. It also shows how a pull or polling (versus push) model of communication can work in EasyCrypt.

Reading, Documentation, and Tools

Organizers

Michael Clark (Riverside Research)
Alley Stoughton (Boston University)
Mayank Varia (Boston University)

Acknowledgments

We acknowledge the support from the National Science Foundation (NSF) under grant CNS-1801564 “Towards Mechanized Proofs of Composable Security Properties” and from the Defense Advanced Research Projects Agency (DARPA) under Contract No. N66001-22-C-4020. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of NSF or DARPA.