Manchester Seminar Series: Security, Cryptography and Quantum Information

Decentralized protocols often use signature adaptation to conditionally release a cryptographic secret to the public. However, standard primitives are inherently anonymous: anyone holding the correct witness can complete the authorization, and the identity of the completer remains hidden. Accountable systems, conversely, require joint authorization where only a designated counterparty can finalize the signature and release the secret.

We introduce Identity-Bound Witness Extractable Signatures (IWES), a novel primitive that allows a Sender to issue a pre-signature locked to a specific Receiver. To complete the signature, the Receiver must inject a witness explicitly bound to its public identity. This completed signature publicly reveals the witness, attributing the final action to the Receiver while allowing the witness to serve as a cryptographic key.

We demonstrate the utility of IWES by applying it to Ethereum’s enshrined Proposer-Builder Separation (ePBS), directly resolving the critical Payload Timeliness vulnerability. Currently, ePBS relies on a Payload Timeliness Committee to subjectively vote on whether a Builder revealed a payload after a Proposer committed to a block header. By integrating IWES, the Proposer’s pre-signature is locked to the winning Builder. To finalize the consensus signature, the Builder must release a witness that is itself the payload decryption key. This aligns economic incentives so that a rational Builder gains nothing by withholding the payload. Consequently, payload availability becomes an objective, slashable property of the block signature, eliminating the need for a dedicated committee.

Finally, we provide a construction of IWES based on the hardness of the Module-LWE and Module-SIS assumptions, and validate it through a portable C implementation. Our benchmarks demonstrate that the construction produces post-quantum signatures of approximately 22 KB and the overhead on the entire ePBS pipeline is under 11 ms, comfortably within Ethereum’s slot and bandwidth constraints.

A test oracle is the mechanism that decides whether a test passes, but it is not always available, especially when a specification does not exist or is difficult to write down. This talk starts from the semantics of test cases and explores how to construct a test oracle, when a specification is unavailable, from three sources: the semantics of the input language, other systems that can be mapped to, and AI models. These semantics-driven oracle construction techniques have uncovered thousands of real defects in real-world systems, from SMT solvers, compilers, and databases to the AI models themselves, and a testing agent built on this approach has been deployed in industry.

Chengyu Zhang is a Lecturer in the Department of Computer Science at Loughborough University. He was previously a postdoctoral researcher at ETH Zurich. His research spans software engineering, programming languages, and artificial intelligence, with a focus on providing solutions to ensure the reliability of modern intelligent software. His research has uncovered over 2,000 bugs in real-world software systems and has resulted in more than 20 publications in top-tier venues. He has served as a Co-Chair of the PLDI, OSDI, and USENIX ATC Artifact Evaluation committees, a Program Committee member for ICSE, FSE, ASE, ISSTA, PLDI, and OOPSLA, and a reviewer for TOSEM, TSE, TOPLAS, and TKDE. His work has been recognised by a PLDI Distinguished Paper Award and a Google Open-Source Peer Bonus, and supported by Amazon, Darktrace, and Ant Group.

(M/R)-LWE systems have to be aware of maliciously generated/altered key material, as decryption failures can reveal secret information. In systems such as ML-KEM, encapsulator key material is checked via the Fujisaki-Okamoto transform to prevent adversarial interference. However, no checks are required for decapsulator key material. This means that if an adversary is able to modify the public value used by the decapsulator they can produce a "poisoned key" which still works correctly for the overwhelming majority of legitimate inputs, but for which the decapsulator can arrange exchanges that leak information about the decapsulators private key even when the Fujisaki-Okamoto protection is in place.

Secure aggregation is a fundamental primitive for privacy-preserving federated learning, allowing a server to compute aggregates of client updates without learning any individual client data. Recent protocols have explored committee-based designs to reduce client overhead and support weakly connected participants. Yet existing approaches still incur significant communication and computation costs that scale with the number of clients or the size of model updates.

I will present Lighthouse, a new secure aggregation protocol that supports one-shot client communication while achieving constant server–committee communication and computation overhead, independent of both the number of clients and the dimension of the input vectors. The key technical ingredient is a novel application of recent advances in batched threshold encryption, enabling succinct server–committee interaction while preserving security and correctness. I will also discuss an extension that supports dynamic client participation, an important requirement for large-scale federated learning systems.

Paper: https://eprint.iacr.org/2026/346.pdf

Speaker bio: Alireza Kavousi recently completed his PhD in Computer Science at University College London. His research focuses on distributed cryptography and its applications to blockchain systems. He has published in security and cryptography venues including USENIX Security, IEEE S&P, NDSS, and Asiacrypt.

Digital computing is at a crossroads. Flipping a single bit in modern semiconductor devices consumes over a million times more energy than the theoretical minimum, while moving that bit across a chip requires an order of magnitude more than that. The rapid and widespread deployment of artificial intelligence has further intensified the demand for computing paradigms that combine high performance with ultralow power consumption, especially in areas such as healthcare, autonomous systems, and authentication, where low power, low latency, and data privacy are critical.

In this talk, I will explore how spintronics offers a path towards more efficient computing. I will begin by discussing our work on Fe50Rh50, a material with unusual magnetic behaviour that can be harnessed for high-density data storage and terahertz signal generation. I will then introduce two emerging information carriers in magnetic systems. The first are skyrmions, which can be thought of as nanoscale magnetic whirlpools that are stable, compact, and easy to manipulate. The second are magnons, which are wave-like excitations that propagate through a magnetic material. Both can be leveraged to carry information without the need to move electrons. I will discuss how we are working to control and functionalise these excitations for use in neuromorphic hardware, with the aim of enabling new computing architectures that are both powerful and energy efficient.

Software failures continue to cause severe economic and safety consequences, and testing alone is insufficient: stronger guarantees demand formal methods. As critical infrastructure runs on millions of lines of C, C++, and now Rust, regulators and industry are converging on the same conclusion. This talk traces how one family of tools, the CProver ecosystem, has spent two decades solving this problem, and where the work goes next.

We begin with the security motivation by introducing soundness, completeness, and bounded versus unbounded verification through short C examples that assume no prior background in formal methods. From there, we walk through the core technique shared by every CProver tool: lower the program to an intermediate representation called GOTO, symbolically execute it up to a bound to obtain a loop-free trace, encode that trace as an SMT formula, and let a decision procedure either prove the property or return a concrete counterexample.

From this shared backbone an entire family has grown: CBMC, ESBMC, 2LS, CSeq, and Kani. Each keeps the same pipeline and specialises one stage. We will look at how they diverged historically, where they are used in industry and what they still do not share under the hood. The talk closes on recent work giving GOTO formal operational semantics, turning symbolic execution and SMT encoding into precisely specified procedures and enabling interoperability between CBMC, ESBMC, and Kani through the GOTO Transcoder.

"Neuromorphic computing" is a term used to describe systems that are engineered with the structure of biological nervous systems in mind but the exact relationship between neuromorphic computing and other fields, such as machine learning, is often not clear. This talk will give an introduction and a high-level conceptualisation of neuromorphic computing as a field of study before highlighting Edward's current research into neuromorphic approaches to event-based vision using spiking neural networks. This talk is intended to spark discussion; interruption and questions will be enthusiastically encouraged.

Deploying autonomous robots in safety-critical domains requires architectures that ensure operational effectiveness and safety compliance. In this talk, we present an architecture for developing reliable and verifiable autonomous robots in such domains. It features two distinct subsystems: an Intelligent Control System responsible for normal operations, and a Safety System that provides formally verifiable, independent oversight. We demonstrate this approach on an autonomous inspection robot in a simulated nuclear environment, where the Safety System is programmed to stop the robot whenever it detects that it is too close to an obstacle. The Safety System and its integration are formally verified and validated through simulation and lab experiments. Results show that this approach supports reliable, safety-assured autonomy and provides a robust framework that can be extended to additional requirements and a range of applications.

Reference: D. C. Benjumea, M. Farrell, and L. A. Dennis, “Safe-ROS: An architecture for Autonomous Robots in Safety-Critical Domains,” in Proceedings Seventh International Workshop on Formal Methods for Autonomous Systems, Paris, 17th to 19th of November 2025, vol. 436 of Electronic Proceedings in Theoretical Computer Science, pp. 48–68, Open Publishing Association, 2025. https://doi.org/10.4204/EPTCS.436.6

This talk is about an unpublished conjecture on recovering a point in a metric space from limited information. Perhaps someone in the audience will find a proof.

Random beacons serve as fundamental cryptographic infrastructure for generating publicly verifiable, unpredictable randomness in distributed systems, with particular significance in blockchain-based applications requiring fair and tamper-resistant entropy sources. However, premature leakage of randomness poses a significant threat to applications that rely on the beacon, such as RANDAO. In particular, agents participating in the beacon protocol might profit from learning the random out a priori even without tempering the output. This incentivises rational agents to form coalitions that break the underlying security assumptions of the beacon protocol to learn the random output. In this work, we propose and analyse a random beacon protocol for a rational setting. We show that our protocol returns even if all participating parties behave rationally and might form a grand coalition of all parties. To this end, we outline smart contracts for our protocol that offer bounties for rational parties that can betray their coalition. Therefore, these contracts build a mechanism that establishes mutual distrust between the rational parties, which ultimately stabilises honest behaviour and disincentivises coalitions.

Sparse neural networks promise inference-time efficiency, yet training them effectively remains a fundamental challenge. Despite advances in pruning methods that create sparse architectures, understanding why some sparse structures are better trainable than others with the same level of sparsity remains poorly understood. Aiming to develop a systematic approach to this fundamental problem, we propose a novel theoretical framework based on the theory of graph limits, particularly graphons, that characterises sparse neural networks in the infinite-width regime. Our key insight is that connectivity patterns of sparse neural networks induced by pruning methods converge to specific graphons as networks' width tends to infinity, which encodes implicit structural biases of different pruning methods.

Based on this, we derive a Graphon Neural Tangent Kernel (Graphon NTK) to study the training dynamics of sparse networks in the infinite width limit. Graphon NTK provides a general framework for the theoretical analysis of sparse networks. We empirically show that the spectral analysis of Graphon NTK correlates with observed training dynamics of sparse networks, explaining the varying convergence behaviours of different pruning methods. In addition, we also prove two fundamental theoretical results: a Universal Approximation Theorem for sparse networks that depends only on the intrinsic dimension of active coordinate subspaces; and a Graphon-NTK generalisation bound demonstrating how the limit graphon modulates the kernel geometry to align with informative features.

Overall, our framework provides theoretical insights into the impact of connectivity patterns on the trainability of various sparse neural networks. As such, it transforms the study of sparse neural networks from combinatorial graph problems into a rigorous framework of continuous operators, offering a new mechanism for analysing expressivity and generalisation in sparse neural networks.

Anamorphic cryptography enables parties to communicate covertly even against a "dictator" who holds all secret keys and monitors network traffic. To avoid pre-shared keys, Persiano et al. proposed the notion of Public-Key Anamorphic Encryption (PK-AE). However, PK-AE is structurally demanding: it requires a single ciphertext to simultaneously carry both a regular and a covert message, a rigid constraint that has limited instantiations to complex, non-standard schemes.

In this work, we propose a modular alternative that decouples the generation of a covert payload from its transport. We introduce the Anamorphic Kernel, a minimal primitive that creates a hidden cryptographic instance within a standard one. To a dictator, the kernel's public key appears to be a standard key for a regular scheme; to the receiver, it reveals a hidden sub-parameter set that allows for the decryption of pseudorandom payloads. We instantiate this primitive based on the LWE assumption, by surreptitiously embedding a smaller LWE instance within a standard Regev public matrix.

We then demonstrate how the kernel's pseudorandom payloads can be transported via standard protocols. First, we construct a transport layer using a Key Encapsulation Mechanism (KEM), where the kernel payload is carried within the encapsulation ciphertext. This construction resists active dictator attacks, as any attempt to "sanitize" the ciphertext destroys the session key and breaks protocol correctness. Second, we introduce Anamorphic Secret Sharing, where the kernel payload is transported within the coefficients of a Shamir sharing polynomial. Our results shift the paradigm of anamorphic cryptography from monolithic scheme design to a flexible, modular architecture.

The Internet is currently engaged in a huge cryptographic change as we look to deprecate quantum vulnerable cryptography such as RSA and elliptic curves in favour of new post-quantum algorithms. Although some excellent classical cryptanalysis has been done against the new designs, relatively little work has been done on their quantum security.

This session will talk through some simple quantum algorithms and suggest how they might be modifiable to attack a mathematical problem known as Learning Parity with Errors which underlies many post-quantum methods.