Social media memes are a challenging domain for hate detection because they intertwine visual and textual cues into culturally nuanced messages. To tackle these challenges, we introduce TRACE, a hierarchical multimodal framework that leverages visually grounded context augmentation, along with a novel caption-scoring network to emphasize hate-relevant content, and parameter-efficient fine-tuning of CLIP’s text encoder. Our experiments demonstrate that selectively fine-tuning deeper text encoder layers significantly enhances performance compared to simpler projection-layer fine-tuning methods. Specifically, our framework achieves state-of-the-art accuracy (0.807) and F1-score (0.806) on the widely-used Hateful Memes dataset, matching the performance of considerably larger models while maintaining efficiency. Moreover, it achieves superior generalization on the MultiOFF offensive meme dataset (F1-score 0.673), highlighting robustness across meme categories. Additional analyses confirm that robust visual grounding and nuanced text representations significantly reduce errors caused by benign confounders. We publicly release our code to facilitate future research.

We systematically scrutinise all the facets of privacy in the 5G delegated-authentication procedure called AKMA (Authentication and Key Management for Applications based on 3GPP credentials in the 5G Systems). We define, in general terms, a privacy-threat model and privacy requirements for this protocol. Using these definitions, we find numerous privacy failings in the AKMA protocol. We propose a patch, called AKMAp, which imposes minimal changes on AKMA, yet it attains all our privacy requirements. We also formalise and analyse all of this in terms of formal privacy-verification in the Dolev-Yao model; to this end, we use the Tamarin prover to systematically carried out our formal analyses of AKMA and AKMAp.

Open and disaggregated O-RAN architectures foster flexibility and vendor diversity in 5G/6G networks but simultaneously expose novel attack surfaces exploitable by sophisticated adversaries. Traditional rule-based or signature-driven detection mechanisms struggle against multi-stage, polymorphic threats in such dynamic environments. This paper proposes TwinGuard, a proactive defence framework that integrates a real-time Digital Twin of a live 5G O-RAN deployment with reinforcement learning (RL) for intelligent threat anticipation and mitigation. Our system mirrors critical KPIs, including throughput, PRB utilisation, SINR, and latency, into the Digital Twin, where an RL agent trained via Proximal Policy Optimisation (PPO) learns optimal mitigation strategies. In our prototype, the RL agent identifies and blocks malicious handover attacks within 100 ms, maintaining service continuity and outperforming a DQN-based baseline. In a second prototype deployed on a containerised OpenAirInterface (OAI) 5G Core and FlexRIC-controlled RAN testbed, our xApp swiftly mitigates an E2 subscription flooding attack in under 100 ms, reducing abnormal PRB utilisation from 95% to nominal levels. TwinGuard demonstrates the feasibility and effectiveness of closed-loop, AI-driven cybersecurity in O-RAN systems, offering a blueprint for future trustworthy and resilient 6G networks.

Online voting for independent elections is generally supported by trusted election providers. Typically these providers do not offer any way in which a voter can verify their vote, and hence the providers are trusted with ballot privacy and in ensuring correctness. Despite the desire to offer online voting for political elections, this lack of transparency and verifiability is often seen as a significant barrier to the large-scale adoption of online elections. Adding verifiability to an online election increases transparency and integrity, as well as allowing voters to verify that the vote they cast has been recorded correctly and included in the tally. However, replacing existing online systems with those that provide verifiable voting requires new algorithms and code to be deployed, and this presents a significant business risk to commercial election providers, as well as the societal risk for official elections selecting for public office. In this paper we present the first step in an incremental approach which minimises the business risk but demonstrates the advantages of verifiability, by developing an implementation of key elements of a Selene-based verifiability layer and adding it to an operational online voting system. Selene is a verifiable voting protocol that publishes votes in plaintext alongside a voter's tracker. These trackers enable voters to confirm that their votes have been captured correctly by the system, such that the election provider does not know which tracker has been allocated to which voter. This results in a system where even a “dishonest but cautious” election authority running the system cannot be sure of changing the result in an undetectable way, and hence gives stronger guarantees on the integrity of the election than were previously present. We explore the challenges presented by adding a verifiability layer to an operational system. The system was used in two initial trials conducted within real contested elections. We conclude by outlining the further steps in the road-map towards the deployment of a fully trustworthy online voting system.

We define and formalise a generic cryptographic construction that underpins coupling of companion devices, e.g., biometrics-enabled devices, with main devices (e.g., PCs), in a user-aware manner, mainly for on-demand authentication and secure storage for applications running on the main device. We define the security requirements of such constructions, provide a full instantiation in a protocol-suite and prove its computational as well as Dolev-Yao security. Finally, we implement our protocol suite and one password-manager use-case.

Swarm attestation protocols extend remote attestation by allowing a verifier to efficiently measure the integrity of software code running on a collection of heterogeneous devices across a network. Many swarm attestation protocols have been proposed for a variety of system configurations. However, these protocols are currently missing explicit specifications of the properties guaranteed by the protocol and formal proofs of correctness. In this paper, we address this gap in the context of list swarm attestation protocols, a category of swarm attestation protocols that allow a verifier to identify the set of healthy provers in a swarm. We describe the security requirements of swarm attestation protocols. We focus our work on the SIMPLE+ protocol, which we model and verify using the Tamarin prover. Our proofs enable us to identify two variations of SIMPLE+: (1) we remove one of the keys used by SIMPLE+ without compromising security, and (2) we develop a more robust design that increases the resilience of the swarm to device compromise. Using Tamarin, we demonstrate that both modifications preserve the desired security properties.

Users accessing services are often required to provide personal information, for example, age, profession and location, in order to satisfy access polices. This personal information is evident in the application of e-ticketing where discounted access is granted to visitor attractions or transport services if users satisfy policies related to their age or disability or other defined over attributes. We propose a privacy-preserving electronic ticket scheme using attribute-based credentials to protect users' privacy. The benefit of our scheme is that the attributes of a user are certified by a trusted third party so that the scheme can provide assurances to a seller that a user's attributes are valid. The scheme makes the following contributions: (1) users can buy different tickets from ticket sellers without releasing their exact attributes; (2) two tickets of the same user cannot be linked; (3) a ticket cannot be transferred to another user; (4) a ticket cannot be double spent. The novelty of our scheme is to enable users to convince ticket sellers that their attributes satisfy the ticket policies and buy discounted tickets anonymously. This is a step towards identifying an e-ticketing scheme that captures user privacy requirements in transport services. The security of our scheme is proved and reduced to a well-known complexity assumption. The scheme is also implemented and its performance is empirically evaluated.

Direct Anonymous Attestation (Daa) is a set of cryptographic schemes used to create anonymous digital signatures. To provide additional assurance, Daa schemes can utilise a Trusted Platform Module (Tpm) that is a tamper-resistant hardware device embedded in a computing platform and which provides cryptographic primitives and secure storage. We extend Chen and Li's Daa scheme to support: 1) signing a message anonymously, 2) self-certifying Tpm keys, and 3) ascertaining a platform's state as recorded by the Tpm's platform configuration registers (PCR) for remote attestation, with explicit reference to Tpm2.0 API calls. We perform a formal analysis of the scheme and are the first symbolic models to explicitly include the low-level Tpm call details. Our analysis reveals that a fix pro-posed by Whitefield et al. to address an authentication attack on an Ecc-Daa scheme is also required by our scheme. Developing a fine-grained, formal model of a Daa scheme contributes to the growing body of work demonstrating the use of formal tools in supporting security analyses of cryptographic protocols. We additionally provide and benchmark an open-source C++implementation of this Daa scheme supporting both a hardware and a software Tpm and measure its performance.

LoRaWAN (Low-power Wide-Area Networks) is the main specification for application-level IoT (Internet of Things). The current version, published in October 2017, is LoRaWAN 1.1, with its 1.0 precursor still being the main specification supported by commercial devices such as PyCom LoRa transceivers. Prior (semi)-formal investigations into the security of the LoRaWAN protocols are scarce, especially for Lo-RaWAN 1.1. Moreover, amongst these few, the current encodings [4], [9] of LoRaWAN into verification tools unfortunately rely on much-simplified versions of the LoRaWAN protocols, undermining the relevance of the results in practice. In this paper, we fill in some of these gaps. Whilst we briefly discuss the most recent cryptographic-orientated works [5] that looked at LoRaWAN 1.1, our true focus is on producing formal analyses of the security and correctness of LoRaWAN, mechanised inside automated tools. To this end, we use the state-of-the-art prover, Tamarin. Importantly, our Tamarin models are a faithful and precise rendering of the LoRaWAN specifications. For example, we model the bespoke nonce-generation mechanisms newly introduced in LoRaWAN 1.1, as well as the “classical” but shortdomain nonces in LoRaWAN 1.0 and make recommendations regarding these. Whilst we include small parts on device-commissioning and application-level traffic, we primarily scrutinise the Join Procedure of LoRaWAN, and focus on version 1.1 of the specification, but also include an analysis of Lo-RaWAN 1.0. To this end, we consider three increasingly strong threat models, resting on a Dolev-Yao attacker acting modulo different requirements made on various channels (e.g., secure/insecure) and the level of trust placed on entities (e.g., honest/corruptible network servers). Importantly, one of these threat models is exactly in line with the LoRaWAN specification, yet it unfortunately still leads to attacks. In response to the exhibited attacks, we propose a minimal patch of the LoRaWAN 1.1 Join Procedure, which is as backwards-compatible as possible with the current version. We analyse and prove this patch secure in the strongest threat model mentioned above. This work has been responsibly disclosed to the LoRa Alliance, and we are liaising with the Security Working Group of the LoRa Alliance, in order to improve the clarity of the LoRaWAN 1.1 specifications in light of our findings, but also by using formal analysis as part of a feedback-loop of future and current specification writing.

This paper discusses an approach for incremental change to an online voting system, introducing a verifiability layer based on the Selene protocol to a trusted-third-party-based system, resulting in a fully verifiable and transparent e-voting system. The paper also describes how to use Distributed Ledger Technology as a component of the implementation of Selene to manage the verifiability data in a distributed way for resilience and trust.

An anonymous single sign-on (ASSO) scheme allows users to access multiple services anonymously using one credential. We propose a new ASSO scheme, where users can access services anonymously through the use of anonymous credentials and unlinkably through the provision of designated verifiers. Notably, verifiers cannot link a user's service requests even if they collude. The novelty is that when a designated verifier is unavailable, a central authority can authorize new verifiers to authenticate the user on behalf of the original verifier. Furthermore, a central verifier can also be authorized to de-anonymize users and trace their service requests. We formalize the scheme along with a security proof and provide an empirical evaluation of its performance. This scheme can be applied to smart ticketing where minimizing the collection of personal information of users is increasingly important to transport organizations due to privacy regulations such as general data protection regulations (GDPRs).

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

Abstract In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.

Abstract Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can be indicated as convergent (to be made internal) or anticipated (treatment deferred to a later refinement step). All such steps are accompanied with precise proof obligations. However, no behavioural semantics has been provided to validate the proof obligations, and no formal justification has previously been given for the application of these rules in a refinement chain. Behavioural semantics expresses a clear relationship between the first and last machines in a refinement chain. The framework we present provides a coherent justification for Abrial’s approach to refinement in Event-B, and its generalisation to interface extension: adding events to the interface. In this paper, we give a behavioural semantics for Event-B refinement, with a treatment for the first time of splitting events and of anticipated events, adding to the well-understood treatment of convergent events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement. It turns out that the appropriate CSP refinement relationship is influenced by the particular Event-B development strategy taken. We present two such strategies, one allowing, the other disallowing interface extensions.

Social Networks were created to allow users to maintain circles of friends and acquaintances. Over time, they have come to be used to share data objects such as pictures between friends. There have been several approaches to formalize social networks in order to specify complicated access control policies for such objects. These approaches have involved a combination of existing logic with custom languages, with new operators being introduced when more complex policies needed to be expressed. In this paper we demonstrate that set theoretic notation provides a convenient syntax for specifying a social network and the associated access control policies. We demonstrate that our notation enables us to extend the range of policies that can be articulated. We also demonstrate that our notation is simpler and more concise than existing approaches.

Abstract CSP || B is an integration of two well known formal notations: CSP and B. It provides a method for modelling systems with both complex state (described in B machines) and control flow (described as CSP processes). Consistency checking within this approach verifies that a controller process never calls a B operation outside its precondition. Otherwise the behaviour of the operation cannot be predicted. In previous work, this check was carried out by manually decomposing the model before preprocessing the CSP processes to perform a hand-written weakest precondition proof. In this paper, a framework is described that mechanises consistency checking in a theorem prover and removes the need for preprocessing. This work is based on an existing PVS embedding of the CSP traces model, but it is extended by introducing a notion of state so that the interaction between processes and machines can be analysed. Numerous rules have been defined (and proved) which enable consistency checking and decomposition via PVS proof. These rules also formally justify the relaxation of previous constraints on CSP || B architectures, thereby widening the scope of CSP || B modelling. The PVS embedding and rules presented in this paper are not only applicable to CSP || B specifications, but to other combined approaches which use a non-blocking semantics for the state-based operations.

Abstract The introduction of probabilistic behaviour into the B-method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected values of the machine state can be expressed and verified. This paper explores the application of probabilistic B to a simple case study: tracking the volume of liquid held in a tank by measuring the flow of liquid into it. The flow can change as time progresses, and sensors are used to measure the flow with some degree of accuracy and reliability, modelled as non-deterministic and probabilistic behaviour respectively. At the specification level, the analysis is concerned with the expectation clause in the probabilistic B machine and its consistency with machine operations. At the refinement level, refinement and equivalence laws on probabilistic GSL are used to establish that a particular design of sensors delivers the required level of reliability.

Abstract Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and controller behaviour). This approach is driven by the desire to exploit existing tool support for both CSP and B, and by the need for compositional proof techniques. This paper is concerned with the theory underpinning the approach, and proves a number of results for the development and verification of systems described using a combination of CSP and B. In particular, new results are obtained for the use of the hiding operator, which is essential for abstraction. The paper provides theorems which enable results obtained (possibly with tools) on the CSP part of the description to be lifted to the combination. Also, a better understanding of the interaction between CSP controllers and B machines in terms of non-discriminating and open behaviour on channels is introduced, and applied to the deadlock-freedom theorem. The results are illustrated with a toy lift controller running example.