Events

Title:Seems Legit: Automated Analysis of  Subtle Attacks on Protocols that Use Signatures

Abstract: The standard definition of security for digital signatures—existential unforgeability—does not ensure certain properties that protocol designers might expect. For example, in many modern signature schemes, one signature may verify against multiple distinct public keys. It is left to protocol designers to ensure that the absence of these properties does not lead to attacks. Modern automated protocol analysis tools are able to provably exclude large classes of attacks on complex real-world protocols such as TLS 1.3 and 5G. However, their abstraction of signatures (implicitly) assumes much more than existential unforgeability, thereby missing several classes of practical attacks. We give a hierarchy of new formal models for signature schemes that captures these subtleties, and thereby allows us to analyse (often unexpected) behaviours of real-world protocols that were previously out of reach of symbolic analysis. We implement our models in the Tamarin Prover, yielding the first way to perform these analyses automatically, and validate them on several case studies. In the process, we find new attacks on DRKey and SOAP’s WS-Security, both protocols which were previously proven secure in traditional symbolic models.

Title: Generalized Abelian Complexities for Pisot-Type Substitutive Sequences

Abstract: Two finite words are said to be abelian equivalent if one is a permutation of the letters of the other. For an infinite word, one can investigate the associated complexity function, called Abelian complexity, which is a classical object of study in combinatorics on words. In particular, many works study the abelian complexity of automatic sequences, where a longstanding conjecture states that the abelian complexity of an automatic sequence is a regular sequence. We have studied when the abelian complexity can be computed efficiently, in particular using the theorem prover Walnut. To this end, we study words that are fixed points of Pisot-type substitution and prove that these words satisfy the conjecture. If time permits, I will present k-abelian complexities, which are intermediate complexities between the abelian complexity and the factor complexity. I will also explain how our results can be extended to these
complexities and how we can obtain a two-dimensional linear representation of some examples. This talk is based on joint work with J-M Couvreur, M. Delacourt, N. Ollinger, J. Shallit, and M. Stipulanti (arXiv: 2504.13584).

There will be a pre-seminar presenting relevant background at the beginning graduate level starting at 1:30pm.

Title: Parameter robust preconditioning

Abstract: The discretization of a partial differential equation (PDE) results in a linear system and iterative solvers are typically used to solve these linear systems, especially if these linear systems are large. Krylov subspace methods are an important class of iterative methods but for these methods to be effective they must be combined with a preconditioner. However, finding a good preconditioner for a given discretization of a PDE is a nontrivial task and so in the first part of this talk I will summarize some useful results from the literature that use a Functional Analysis framework to identify preconditioners for symmetric PDEs.

Title:The Heron-Rota-Welsh conjecture via Lorentzian polynomials

Abstract:The Heron-Rota-Welsh conjecture asserts that the characteristic polynomial of a matroid has log-concave coefficients. This conjecture was open since the 1970s until it was proven by Adiprasito, Huh, and Katz in 2018 using their newly developed combinatorial Hodge theory. Their proof was groundbreaking, but rather complicated. In this talk, we will give a proof of this fact using Lorentzian polynomials, which otherwise will use nothing more than basic theory of matroids, linear algebra, and convexity.