Note that the program is preliminary and subject to change.

8.30 Registration opens

9.00 Welcome

9.10 Invited talk I

  • SIM-AC: Modular, Composable, Bug-free Proofs For Adaptive Compromise
    Joseph Jaeger (Georgia Institute of Technology)
    Abstract

10.30 Coffee break

11.00 Game-based security

  • Non-Committing Encryption as a QROM Playground
    Hans Heum (NTNU – Norwegian University of Science and Technology)
    Abstract
  • Please Mind the Gap: From Cryptographic Security Proofs to Attack Trees
    Jeremias Mechler (KASTEL Security Research Labs, Karlsruhe Institute of Technology)
    Abstract
  • Enhancing Cryptographic Proofs: A Blended Approach to CryptoBox in EasyCrypt
    Charlotte Mylog (NTNU Trondheim)
    Abstract

12.30 Lunch break

13.30 Invited talk II

  • Mechanizing Cryptographic Reductions by Bi-Deduction
    Adrien Koutsos (Inria Paris)
    Abstract

15.00 Coffee break

15.30 Simulation-based security

  • Universal Composability with Effect Handlers
    Jesse Sigal (University of Edinburgh)
    Abstract
  • Universal Composability with Global Generic Groups
    Jan Bobolz (University of Edinburgh)
    Abstract

17.00 End of day

Abstracts

SIM-AC: Modular, Composable, Bug-free Proofs For Adaptive Compromise

Invited Speaker: Joseph Jaeger (Georgia Institute of Technology)

This talk covers a sequence of works introducing and using new definitions capturing simulation-based security under adaptive compromise (SIM-AC) for pseudorandom functions, encryption schemes, and key-encapsulation mechanisms. These definitions are impossible in the standard model but are nonetheless valuable for simplifying and modularizing common ideal model proof techniques (which in proofs is often omitted or has subtle bugs). Applications of SIM-AC include searchable encryption, password-authenticated key exchange, and garbled circuits. Some of these applications require SIM-AC to have a composability property which is achieved by (somewhat bizarrely) allowing attackers to program ideal primitives.

Mechanizing Cryptographic Reductions by Bi-Deduction

Invited Speaker: Adrien Koutsos (Inria Paris)

Cryptographic protocols are used to secure many applications. The goal of a cryptographic proof is to obtain formal guarantees on the level of security provided by such a protocol. Mechanization allows for the highest level of guarantees, by having a formal computer program verify the cryptographic arguments themselves. This approach has seen a growing interest in the last years, notably with the utilization of program logics to verify cryptographic games encoded as imperative programs (e.g. as in EasyCrypt).
The first goal of this talk is to present an alternative approach to mechanize cryptographic arguments. This approach, implemented in the Squirrel proof assistant, relies on a different encoding of cryptographic proofs: games are represented by pure instead of imperative programs, and cryptographic arguments are directly captured at a logical level. In particular, some of Squirrel logical rules corresponds to reductions to cryptographic hardness assumptions. Unfortunately, these rules are complex to design and implement; so far, these tasks are manual, error-prone, and limited to a small set of cryptographic assumptions (e.g. IND-CCA and PRF). The second goal of this talk is to present some recent work that aim at providing a formal, systematic and highly-automated method for deriving rules from cryptographic games. Our method relies on synthesizing (parts of) an adversary w.r.t. some cryptographic game through the notion of bi-deduction, and has been implemented in Squirrel.

Non-Committing Encryption as a QROM Playground

Speaker: Hans Heum (NTNU)
Author: Hans Heum

(Non-interactive) Non-Committing Encryption (NCE) is a very strong security goal, even unachievable in the non-programmable random oracle model, and yet it has turned out to be a useful intermediary notion in many security proofs.
The necessity of programming ideal objects like random oracles makes constructing post-quantum NCE an interesting challenge. In this talk, we report on work-in-progress in showing the post-quantum security of the canonical NCE construction (when instantiated with quantum-safe primitives). Limiting ourselves to the CPA setting, we show that even a baseline proof of security requires us to pull out “every tool in the QROM toolbox” to tackle challenges like the recording and programming of random oracle queries, with even more esoteric tools, such as fully-quantum security notions, seemingly needed to achieve a tighter reduction.

Please Mind the Gap: From Cryptographic Security Proofs to Attack Trees

Speaker: Jeremias Mechler (KASTEL Security Research Labs, Karlsruhe Institute of Technology)
Authors: Jeremias Mechler, Felix Dörre, Eva Hetzel, Christian Martin and Jörn Müller-Quade

Models such as the Universal Composability (UC) framework due to Canetti (FOCS 2001) allow to establish strict security guarantees of cryptographic protocols via proofs. However, when implementing and deploying a cryptographic protocol, there often is a gap between the model and the real system. As a consequence, the system may not be secure, even though the protocol provably is. An established methodology to analyze (in contrast to prove) the security of complex systems are so-called attack trees, first proposed by Schneier. In contrast to formal models with well-defined semantics, they enable security analyses without formal specifications of the system or the security goal. In this talk, we discuss first results of ongoing work, insights and challenges that arise from combining cryptographic security proofs and attack tress.

Enhancing Cryptographic Proofs: A Blended Approach to CryptoBox in EasyCrypt

Speaker: Charlotte Mylog (NTNU)
Author: Charlotte Mylog

This ongoing work revisits the proof of CryptoBox from Dupressoir et al. (CSF 2022) which served as an illustration of how to exploit the desirable properties of state separating proofs (SSPs) when mapping them to EasyCrypt concepts. SSPs, introduced by Brzuska et al. (Asiacrypt 2018), extend the game-based approach by breaking down monolithic games into smaller, stateful packages and introducing a modular reasoning.
We develop a new proof for the same result, using a pragmatic, but systematic combination of SSP and code-based game-based concepts. This introduces a blended proof approach with the help of the practical example of CryptoBox. Instead of using a big initial deconstruction as in SSPs, our approach divides this process into sequential steps preserving the modularity and local reasoning. We discuss how this proves to be beneficial for both the manual verification and the formalization of proofs using tools like EasyCrypt.
This research is part of a project whose goal is to compare different proof approaches on criteria such as readability, verifiability, and simplicity as well as their alignment with EasyCrypt’s logics.

Universal Composability with Effect Handlers

Speaker: Jesse Sigal (University of Edinburgh)
Authors: Markulf Kohlweiss, Sam Lindley, Sabine Oechsner and Jesse Sigal

The Universal Composability (UC) framework of Canetti (FOCS 2001) and other similar frameworks allow one to express and reason about cryptographic protocol security in a composable way. Composability is aided through a prescribed cooperative concurrency structure based on token passing and message passing. Unfortunately, UC requires computation to be described by interactive Turing machines (ITMs), which are inconvenient from both an implementation and formal reasoning perspective. Alternatives to ITMs have been explored in EasyCrypt’s pWhile language (Canetti, Stoughton, Varia CSF 2019 and Barbosa et. al. CCS 2021) as well as in Haskell (Liao, Hammer, Miller PLDI 2019). What they all have in common is that they closely follow the verbose UC way of expressing interaction via token passing. In this talk, we will present ongoing work on a new approach to expressing UC-style protocol security by modelling token passing and message passing as effects, with the help of effect handlers. It will introduce effect handlers and discuss their use to model and implement a UC-style system with cooperative concurrency in a direct and understandable style.

Universal Composability with Global Generic Groups

Speaker: Jan Bobolz (University of Edinburgh)
Authors: Jan Bobolz, Pooya Farshim, Markulf Kohlweiss and Akira Takahashi

Security proofs in the generic group model are usually done without regard to the composability of the proven constructions, and hence do not necessarily guarantee that two constructions working over the same (generic) group can be combined, or even just run concurrently. That raises the natural question: how can we model composability of generic group model constructions?
To answer this, we introduce the restricted observable global generic group functionality G-oGG. This UC functionality supports a notion of observability, which is carefully designed to allow simulators to observe all relevant G-oGG queries, while being able to make queries hidden from the environment. This design is inspired by the domain-separation approach of restricted observable global random oracles. However, while domain separation is relatively simple in the random oracle case, domain separation for generic groups is more difficult, as one can combine group elements of different sessions/domains (whereas random oracle images cannot be meaningfully combined).
In the talk, we are going to
(1) give an explanation of the general concept of domain separation for global observable functionalities (applicable to both random oracles and generic groups),
(2) introduce our functionality G-oGG and motivate how our design decisions enable meaningful security proofs, and
(3) point out an incompatibility of some generic-group protocols with G-oGG, and show how to solve this issue using a custom composition theorem.