Rigorous Systems Seminar

Upcoming Talks

• Wednesday, 16 September 2026 at 2pm in CMT.01 and Teams

  There will be two 25 minute talks. See below for titles and abstracts.

  
  
• Speaker: Lewis Cox

  Title: Nuclear Power Plant Modeling and Threat Analysis from a Cyber Security Perspective

  Abstract

  Given both the increasing digitisation and necessity of Nuclear Power Plants (NPPs), their cyber security has never been more important. NPPs require specific cyber security approaches due to their complex and sensitive nature as a Cyber-Physical System (CPS). This paper reports on the modeling of NPPs for cyber security threat analysis based on the Stuxnet case study and established literature. We conducted the modeling and analysis using the risk and attacks analysis platform ATSyRA which provides languages to express new domain abstractions and goal description and automates model verification, reachability analysis and visualisations. In this paper, we present our general NPP modeling domain language, its application to the Stuxnet case study and discuss our abstraction and analysis approach.

  Bio

  Lewis Cox completed his BSc Computer Science at Heriot-Watt University in 2026. He will be presenting this work resulting from his Honours project at the SENSEI Workshop of the SAFECOMP Conference. DOI: 10.1007/978-3-032-35506-5_42

  
  
• Speaker: Tin Tironsakkul

  Title: Complying with the Right to Be Forgotten in Smart Mobility Data Sharing: A Delete-Only Redactable Consortium Blockchain

  Abstract

  The immutability of blockchain, while ideal as an alternative solution for decentralised data sharing and enhancing data authenticity in smart mobility, clashes fundamentally with growing demands for data mutability driven by privacy regulations. This tension threatens the practical adoption of blockchain in privacy-sensitive smart mobility ecosystems. To reconcile this conflict, we propose a novel data redaction approach designed for consortium blockchains. Our solution introduces a fine-grained, controlled, and accountable delete-only redaction function. The proposed protocol enables data subjects or trusted authorities to initiate the deletion of sensitive message data within transactions using a digital signature. The redaction request is subsequently validated and approved by a subset of trusted authorities via an accountable threshold signature scheme, ensuring transparency and non-repudiation. Performance analysis of the proof-of-concept implementation demonstrates minimal overhead in efficiency and scalability, which illustrates that our proposed protocol satisfies requirements for smart mobility applications.

  Bio

  Tin Tironsakkul was a research fellow at the University of Aberdeen, UK, contributing to cutting-edge research in blockchain and smart contracts with a focus on privacy-enhancing technologies. His postdoc research was part of the "Secure, Privacy-aware, and Trusted Data Share in Smart Mobility" project. Tironsakkul earned his PhD from Heriot-Watt University, where he focused on blockchain forensic analysis and privacy-enhancing technologies, underscoring his deep expertise in ensuring secure and private digital systems. Tin presented this work at SECRYPT 2026. DOI: 10.5220/0015184100004103

  
  

Past Talks

• 9 September 2026 at 2pm in CMT.01

  Speaker: Rolando Trujillo Rasua (Universitat Rovira i Virgili, Tarragona, Spain)

  Title: Can you be fooled by C2PA provenance? A formal analysis of the C2PA standard

  Abstract

  The Coalition for Content Provenance and Authenticity (C2PA), which includes major companies such as Adobe and Microsoft, defines a technical standard that describes how the modification history of a digital asset must be recorded. In this talk, I'll present a concise overview of the standard and develop a formal specification of C2PA's verification and editing mechanisms. Grounded on the standard's stated goals, I'll introduce an adversary model and define two provenance security properties: a stronger lineage authenticity property, requiring that provenance data unambiguously identifies the specific assets used at every step, and a weaker credential authenticity property, concerning the authenticity of provenance data. We can show that C2PA does not satisfy lineage authenticity: an attacker can provide the same provenance data for different editing histories. This creates an evidentiary ambiguity that the provenance data cannot resolve. I'll describe simple updates to the standard that restore lineage authenticity; updates that we formally prove correct.

  
  
• 6 July 2026

  Speaker: Janis Bailitis

  Title: Towards Quantitative Logics in Rocq

  Abstract

  Quantitative logics (QLs) are logics whose truth values go beyond 0 and 1. Notable examples include fuzzy logics interpreted in [0,∞], which give propositions like "x is much larger than 10" a meaningful truth value. Despite growing importance, for example in verification of machine learning, QLs lack a general formal theory. Addressing this issue, inspired by a Rocq mechanisation of selected QLs due to Affeldt et al., we envisage a general and reusable library for QLs mechanised in Rocq, containing the previous mechanisations as case studies.

  In this talk, we will briefly present the proposed structure of the library with a focus on intervals of real numbers, a key ingredient to many QLs, mechanised using the MathComp-analysis library. Then, we will discuss work in progress on mechanising Quantitative Linear Logic within our library, which is a recently proposed QL by Capucci et al. generalising multiplicative-additive linear logic.

  
  
• 22 June 2026

  Speaker: Mathews George

  Title: A Tactic for Pattern Matching in Autosubst

  Abstract

  Reasoning about binders in a proof assistant requires additional overhead compared to paper-based proofs. Autosubst enables automatic equality-checking up to the σ-calculus for assumption-free equalities, allowing users of proof assistants to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without β-reduction, solutions of matching may not be unique. In this talk, we present a work-in-progress method for automatically pattern matching against assumptions evaluated on standard case studies, including the benchmarks POPLMark and POPLMark Reloaded challenges.

  
  
• 22 June 2026

  Speaker: Yukang Xie

  Title: A Dataflow-Driven Processor for Lazy Functional Programming Languages

  Abstract

  Specialised hardware for functional languages has a long history, driven by the hope of running expressive languages like Haskell more efficiently than conventional machines allow. Recent designs have made progress, but they share a stubborn limitation: the natural way to run these programs - graph reduction - is sequential, with each step depending on the last. This makes it hard to speed things up through pipelining.

  This talk presents Ouros, a processor that takes a different approach. Instead of a central logic deciding what happens next, processor components work in a data-driven manner. Ouros also splits work into lightweight threads automatically, without help from the programmer or compiler - something that was previously impractical because managing threads cost too much. In Ouros, creating and synchronising a thread each take a single cycle.

  I'll also describe the garbage collector, which cleans up memory in the background, with its algorithm verified by bounded model checking, and close with results from simulation and FPGA prototyping.

  
  
• 15 June 2026 at 11am in IF G.03, University of Edinburgh

  Speaker: Sophie Pinchinat (IRISA, Université de Rennes)

  Title: A Journey Through the Formal Aspects of Attack-Defence Trees

  Abstract

  Attack-defence trees (ADTs) are classical graphical models to reason about a hierarchical decomposition of a main attack goal into a combinations of sub-goals (that are in turn decomposed, and so on). ADTs are one of the oldest method to conduct risk analysis that is still highly recommended, e.g. by NATO, but also by the National Cyber Security Centre of the UK Government, as they help security experts to exhibit optimal countermeasures to protect the system under study/design.

  Originally, ADTs have been constructed manually in a highly informal manner: the node labels are plain textual descriptions of what the expert has is mind, and the meaning of sub-goal combinators (classically OR, AND and sequentialAND) is left open to the designer intuitive interpretation. The academic world has developed various formal settings to better handle ADTs, hoping for diverse (semi-)automated techniques.

  In this talk, we focus on a piece of work, started a decade ago, that shows formal approaches to assist experts in constructing ADTs, with an accurate account of the computational complexity of decision problems relevant to the use of ADTs in practice.

  Bio

  Sophie Pinchinat is a Distinguished Professor at the University of Rennes and leads the research team Logic and Application (LogicA) at the IRISA laboratory. Her main research interests are in formal methods, artificial intelligence, multi-agent systems, security with a focus on the foundations of attack-defence trees and attack existence problems in dynamic attack graphs, planning, mathematical logic, automata, dynamic epistemic reasoning, and multi-player games. She is developing the ATSyRA software (Attack Tree Synthesis for Risk Analysis https://atsyra2.irisa.fr/), an academic prototype platform that hosts several functionalities: the modelling language ABS (for Action-Based Systems) to specify dynamic cyberphysical systems, tools inherited from model checking and automated planning to specify attack objectives and generate attack scenarios, and an assistant tool for handling the design and analysis of attack trees. All these developments are supported by strong theoretical publications in highly ranked conferences and journals, both in theoretical computer science and in security.

  
  
• 8 June 2026

  Speaker: Freya Murphy (University of Surrey)

  Title: Verifying Account Ecosystems with Graph Transformations

  Abstract

  Account ecosystems comprise a set of resources, including online accounts, devices, and credentials, that jointly impact a user's or organisation's security. Prior work shows that users frequently overlook subtle dependencies within these ecosystems, leading to security breaches that are difficult to detect using analysis techniques focused on isolated components.

  This talk introduces resource access graphs (RAGs), a formal model for the automated analysis of dynamic account ecosystems. To capture the dynamic nature of account ecosystems, we define a transition system based on graph rewriting with RAGs as states in which both user actions and adversarial capabilities are modelled as graph transformation rules. Security properties are specified in computation tree logic (CTL), allowing automated analysis.

  The approach is demonstrated on a simple Apple account ecosystem with the recent security feature Stolen Device Protection (SDP). The analysis reveals limitations in SDP, affecting both the integrity and availability of a user's Apple Account.