Federated space missions such as Artemis and LunaNet need secure, interoperable communication across independently governed agencies, and public key infrastructure (PKI) is the natural foundation. Yet current CCSDS guidance adopts the terrestrial X.509 Internet profile without adaptation, bringing an extensive, unrestricted feature set to resource-constrained spacecraft, and the transition to post-quantum cryptography inflates certificates and revocation data further. This talk examines the standardisation gap. It compares post-quantum certificate formats for a federation, proposes a minimal certificate profile, and asks whether the emerging IETF C509 encoding offers enough benefit to justify adoption: our evaluation with the first open-source native C509 toolkit shows roughly 40% smaller traditional certificates, 60% smaller revocation lists and about 80% less parser code, but savings that plateau at around 200 bytes once post-quantum keys and signatures dominate. The talk closes with what remains unsolved, certificate validation on constrained and intermittently connected assets, and with delegated validation, the subject of an experiment selected for ESA’s CyberCUBE in-orbit cybersecurity platform. The talk is based on work with the European Space Agency, published at Security for Space Systems (3S) 2025 as “Towards Minimal Certificates for Federated Space Public Key Infrastructure”.

Use cases for blockchain-based cryptocurrencies have evolved beyond simple transfers into complex financial applications. Traditionally, these applications are implemented using blockchain-specific features. As a drawback, the same application required multiple implementations, each tailored to a different blockchain. This increases efforts in development, security analysis and limits the deployment of applications on blockchains with restricted features. An alternative consists of implementing the application logic in an off-chain cryptographic protocol. The protocol would output one (or more) payment authorization as required by the logic of the application. These protocols solely depend on the payment authorization mechanism of the blockchain. This enables implementing applications in a blockchain-agnostic manner. Moreover, automatic formal verification tools can help prove the security guarantees of these off-chain protocols. Ultimately, blockchain-agnostic off-chain protocols would enable applications to be implemented once, analyzed once and be deployed on virtually all blockchains. To achieve this vision, remaining challenges are that not all blockchains share the same authorization mechanism, and the existing verification tools fail to capture subtle functionality beyond cryptography (e.g., time when an authorization can be included in the blockchain) that is nevertheless crucial for the security of off-chain protocols. Our research aims to fill these gaps by investigating how to design off-chain protocols over a unified cryptographic foundation for payment authorizations, and their security analysis with automatic formal verification tools.

Arithmetic theories are first-order logics about number systems, such as the integers or the real numbers. They represent a fundamental branch in mathematical logic, and play a pivotal role in various areas of computer science. Their applications span both theoretical and practical domains, including control theory, mechanical engineering, compiler optimization, and program verification.

This talk overviews my recent work on designing procedures for arithmetic theories featuring non-linear functions such as exponentiation and trigonometric functions. As we will see, handling these functions comes at the cost of abandoning many of the fundamental properties of (integer) linear programming, to the point that even the seemingly straightforward task of encoding solutions becomes challenging. We will explore how to circumvent these problems, obtaining efficient algorithms (in theory and/or in practice).

The talk is based on the current progress and future objectives of my Marie-Curie Fellowship.

In this talk (which includes an extended introduction so that even non-cryptographers can follow along) we explore Homomorphic Signatures for NP (HSNP). HSNPs allow us to verify that a signed result is indeed the outcome of a specified (potentially complex) computation on signed inputs. This powerful notion was introduced by Fiore and Tucker at CCS 2022, where they combined zero-knowledge SNARKs (for succinct proof of correct computation) with linearly homomorphic signatures (LHS) to verify operations on streaming data. Although their approach was very flexible, the verification step of their LHS was quite costly. We address this limitation by introducing a new, more efficient LHS, significantly reducing the verification overhead. By retaining Fiore and Tucker’s modular design, our solution yields a streamlined HSNP, particularly advantageous for processing data that arrives in consecutive samples, such as sliding window statistics, histograms, and financial forecasts.

[No advanced knowledge of cryptography needed! Content suitable for a general audience].

End-to-end encryption (E2EE) stands as the gold standard for digital privacy. But how does this cryptographic shield truly work—and why does it matter for businesses and individuals alike?

We dive into the true meaning of E2EE, presenting why simple mechanisms to achieve authenticity and confidentiality do not suffice. We will borrow examples from cloud storage and secure messaging to understand how protocols can self-heal after breaches, ensuring past and future data stays locked even if current keys are leaked. Then, we will walk through the architecture of the Signal Protocol – the backbone of WhatsApp, Facebook Messenger, Signal, and others – whose ephemeral keys and resilience against device compromise set the benchmark for modern secure messaging. Finally, we will look at the additional challenges imposed by group conversations and how these can be addressed in practice.