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.

This paper investigates ER(r^Z), that is the extension of the existential theory of the reals by an additional unary predicate r^Z for the integer powers of a fixed computable real number r > 0. If all we have access to is a Turing machine computing r, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when:

1. r is known to be transcendental, or
2. r is a root of some given integer polynomial (that is, r is algebraic). In other words, knowing the algebraicity of r suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that r enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of ER(r^Z) is
3. in EXPSPACE if r is an algebraic number, and
4. in 3EXP if r is a logarithm of an algebraic number, Euler’s e, or the number pi, among others. To establish our results, we first observe that the satisfiability problem of ER(r^Z) reduces in exponential time to the problem of solving quantifier-free instances of the theory of the reals where variables range over r^Z. We then prove that these instances have a small witness property: only finitely many integer powers of r must be considered to find whether a formula is satisfiable. Our complexity results are shown by relying on well-established machinery from Diophantine approximation and transcendental number theory, such as bounds for the transcendence measure of numbers. As a by-product of our results, we are able to remove the appeal to Schanuel’s conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler’s e and the aversion factor is a fixed algebraic number, the problem is (unconditionally) in EXP.

With the increasing popularity of blockchains, cryptocurrencies are now accepted for the purchase of digital goods, such as e-books or gift cards. A contingent payment is a cryptographic protocol that models digital purchases, and it involves a buyer and a seller. The buyer owns crypto-coins, and the seller owns a digital product. Contingent payment ensures that the buyer and the seller can exchange coins and product securely. However, observers of the blockchain might learn which buyer purchased from which seller based on the information contained in the transaction. Is it possible to extend contingent payment so that the relationship between buyer and seller is hidden? In this talk, I will present how contingent payment works, as well as coin mixing, practical technique to hide the relationship between a sender and a receiver in a transaction regardless of the blockchain. Then, I will show that existing coin mixing schemes cannot be applied to contingent payment as they lead to devastating attacks. My presentation ends with MixBuy, the first protocol that hides the relationship between buyer and seller in a contingent payment, regardless of the blockchain. This talk is related to the paper: https://eprint.iacr.org/2024/953, which will be presented at The 25th Privacy Enhancing Technologies Symposium in 2025.