Summer School

The SAC Summer School will be held on September 27-28, 2021, in an online setting. The purpose of the SAC Summer School is to provide participants with an opportunity to gain in-depth knowledge of specific areas of cryptography related to the current SAC topics by bringing together world-class researchers who will give extended talks in their areas of specialty. The SAC Summer School is open to all attendees, and may be of particular interest to students, postdocs, and other early-career researchers.

The full program is held on ResearchSeminars.org which allows you to change the date/time to your local time zone.

Publishing on YouTube

In order to accommodate time differences of SAC 2021 summer school attendees, we plan to record and publish some of the summer school lectures if possible, on the conference YouTube channel. Your participation in the event is considered as a consent to being recorded and your video published on YouTube. If you have any concerns, please reach out to us as soon as possible.


Zoom Session

The Zoom Session for the summer school (separate from the conference) is available at the following link:


NB: The meeting is password protected to registered attendees. You will receive an email with the password after registration.

Machine-Checked Cryptography with EasyCrypt and Jasmin - Topic 1

Part #1 by François Dupressoir, University of Bristol

Part #2 by Benjamin Grégoire, Inria - Univérsité Côte d'Azur and Vincent Laporte, Inria

EasyCrypt is a toolset for construction and verification of game-based cryptographic proofs. It has been used to develop proofs of the proofs of the AWS Key Management service as well as a verification backend for verified assembly implementations of cryptographic primitives written in the Jasmin language. This pair of lectures will explain how to use EasyCrypt and Jasmin in combination to obtain high-assurance assembly implementations of cryptography—with formal cryptographic security guarantees against adversary that can observe (some) leakage. We will do so by looking at a simple symmetric encryption example, with exercises building up to a full symmetric encryption scheme. Part I will focus on formally defining and proving algorithmic security. Part II will focus on developing assembly implementations and proving them correct and secure.



Communication Privacy - Topic 2


Introduction to anonymous communication with mix networks by Ania M. Piotrowska, Nym Technologies


Abstract: Network traffic is a source of privacy-sensitive information, both in terms of content and metadata. Encryption is only the first step in the efforts to achieve privacy in the online world, since it can only protect the confidentiality of our communication but does not hide the network metadata. Exposing the metadata allows for the unique identification of users and tracking of their online activities. Anonymous communication networks hide the network metadata and the relationship between communicating parties on the Internet. Tor has become very popular since its inception in 2004. However, it has become apparent that the security it provides is fragile against powerful adversaries. In this lecture, we will first review the basics of how anonymous communications and resistance to traffic analysis is achieved in traditional mix network and onion routing. Next, we will look into modern mix network designs that attempt to provide strong anonymity while tackling the scalability and latency issues.


Secure Messaging Protocols – Then, Now, and Next by Britta Hale, Naval Postgraduate School (NPS)

Messaging security has been a topic of increasing interest within cryptographic research, with offered guarantees of E2EE, forward secrecy, and post-compromise security. Despite a great deal of research analyzing the confidentiality properties of secure messaging protocols, e.g. the Signal protocol, entity authentication has largely been abstracted away. This implies direct consequences for an active adversary threat case. Furthermore, modern messaging applications often rely on out-of-band communication to achieve entity authentication, with human users actively verifying and attesting to long-term public keys. This is done primarily to reduce reliance on trusted third parties (by replacing that role with the user) but implies that an accurate security picture must take this interaction into account. This lecture will cover the basics of ratcheted messaging techniques, both for one-to-one connections and for messaging groups (e.g. the MLS protocol), and associated security guarantees. Current user-mediated entity authentication techniques for one-to-one protocols will be covered, potential improvements, and correlated authentication considerations for group messaging.