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.