Since the disclosure of Spectre attacks in 2018, both academia and industry have made considerable efforts to defend against all variants of transient execution attacks, the class of attacks to which Spectre belongs to. The first part of this presentation will be dedicated to discovering how these attacks change the way we reason about threat models in security. The second part of the presentation will introduce a new generic formal processor model - called ProSpeCT - to prevent transient execution attacks by construction. ProSpeCT has also been implemented on top of an open-source RISC-V processor and will be presented in Usenix Security 23 in a joint work with Lesly-Ann Daniel, Marton Bognar, Job Noorman, Sébastien Bardin, and Frank Piessens.
We formalize the simulation paradigm of cryptography in terms of category theory and show that protocols secure against abstract attacks form a symmetric monoidal category (≈ can be composed sequentially and in parallel). This gives an abstract model of composable security definitions in cryptography that is not tied to any particular machine model. Our model is able to incorporate computational security, set-up assumptions and various attack models such as colluding or independently acting subsets of adversaries in a modular, flexible fashion. We conclude by using string diagrams to rederive the security of the one-time pad and no-go results concerning the limits of bipartite and tripartite cryptography, ruling out e.g., composable commitments and broadcasting.
In this talk, I will give an overview of techniques to compile Sigma protocols—a popular class of interactive cryptographic proofs—to non-interactive proofs that guarantee security when used in any larger protocol context. The aim of the talk will be to provide an introduction to the area to system designers who typically use cryptographic tools as a black box, while also providing insight into some interesting technical subtleties that I uncovered in a recent work.
In this talk, Sofía will present FrodoPIR, a highly configurable, stateful, singleserver Private Information Retrieval (PIR) scheme that involves an offline phase that is completely client-independent.
This seminar presents research on anonymous credentials with Publicly Auditable Privacy Revocation (PAPR). PAPR credentials simultaneously provide conditional user privacy and auditable privacy revocation for credential systems.
Felix will introduce PrePaMS, an efficient participation management system that supports prerequisite checks and reward procedures in a privacy-preserving way.
By using a set of proven cryptographic primitives and mechanisms,
participations are protected so that service providers and organizers cannot
derive the identity of participants even within the reward process.
In this talk, I will present DenIM (Deniable Instant Messaging), a novel
protocol built on the idea of hiding traffic to make it unobservable to
an adversary by piggybacking it on observable traffic. We posit that
resilience to traffic analysis must be directly supported by major IM
services themselves, and must be done in a low-latency manner without
breaking existing features. Hence, DenIM is designed both for
compatibility and performance; DenIM is a variant of the Signal
protocol—commonly used for strong encryption in instant messaging
services, and, DenIM’s bandwidth overhead scales with the volume of
regular traffic, as opposed to scaling with time or the number of users.
Alley will argue in favor of using the real/ideal paradigm for defining security in a programming languages context, even when systems are entirely non-probabilistic.