Helen Treharne

Girish A. Koushik, Helen Treharne, Diptesh Kanojia

Social media platforms are increasingly dominated by long-form multimodal content, where harmful narratives are constructed through a complex interplay of audio, visual, and textual cues. While automated systems can flag hate speech with high accuracy, they often function as "black boxes" that fail to provide the granular, interpretable evidence, such as precise timestamps and target identities, required for effective human-in-the-loop moderation. In this work, we introduce TANDEM, a unified framework that transforms audio-visual hate detection from a binary classification task into a structured reasoning problem. Our approach employs a novel tandem reinforcement learning strategy where vision-language and audio-language models optimize each other through self-constrained cross-modal context, stabilizing reasoning over extended temporal sequences without requiring dense frame-level supervision. Experiments across three benchmark datasets demonstrate that TANDEM significantly outperforms zero-shot and context-augmented baselines, achieving 0.73 F1 in target identification on HateMM (a 30% improvement over state-of-the-art) while maintaining precise temporal grounding. We further observe that while binary detection is robust, differentiating between offensive and hateful content remains challenging in multi-class settings due to inherent label ambiguity and dataset imbalance. More broadly, our findings suggest that structured, interpretable alignment is achievable even in complex multimodal settings, offering a blueprint for the next generation of transparent and actionable online safety moderation tools.

Girish A. Koushik, Diptesh Kanojia, Helen Treharne

Social media platforms enable the propagation of hateful content across different modalities such as textual, auditory, and visual, necessitating effective detection methods. While recent approaches have shown promise in handling individual modalities, their effectiveness across different modality combinations remains unexplored. This paper presents a systematic analysis of fusion-based approaches for multimodal hate detection, focusing on their performance across video and image-based content. Our comprehensive evaluation reveals significant modality-specific limitations: while simple embedding fusion achieves state-of-the-art performance on video content (HateMM dataset) with a 9.9% points F1-score improvement, it struggles with complex image-text relationships in memes (Hateful Memes dataset). Through detailed ablation studies and error analysis, we demonstrate how current fusion approaches fail to capture nuanced cross-modal interactions, particularly in cases involving benign confounders. Our findings provide crucial insights for developing more robust hate detection systems and highlight the need for modality-specific architectural considerations. The code is available at https://github.com/gak97/Video-vs-Meme-Hate.

Girish A. Koushik, Helen Treharne, Aditya Joshi et al.

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.

Chris Culnane, Christopher J. P. Newton, Helen Treharne

Even though passwordless authentication to online accounts offers greater security and protection from attack, passwords remain prevalent. Passwordless authentication adoption is impacted by the slow adoption of external hardware keys required to generate the security keys within the authentication protocol. We have developed a virtual WebAuthn authenticator in order to provide an extensible open source platform for understanding the associated standards of WebAuthn and CTAP2. Our authenticator provides secure software authentication for devices that do not have access to a physical hardware interface. Our authenticator also provides an alternative to an external physical hardware key and supports the use of a trusted platform module (TPM) on a device to generate the security keys within a WebAuthn protocol.

Abideen Tetlay, Helen Treharne, Tom Ascroft et al.

Rolling out a new security mechanism in an organisation requires planning, good communication, adoption from users, iterations of reflection on the challenges experienced and how they were overcome. Our case study elicited users' perceptions to reflect on the adoption and usage of the two factor authentication (2FA) mechanism being rolled out within our higher education organisation. This was achieved using a mixed method research approach. Our qualitative analysis, using content and thematic coding, revealed that initially SMS was the most popular 'second factor' and the main usability issue with 2FA was the getting the authenticator app to work; this result was unexpected by the IT team and led to a change in how the technology was subsequently rolled out to make the authenticator app the default primary second factor. Several lessons were learnt about the information users needed; this included how to use the technology in different scenarios and also a wider appreciation of why the technology was beneficial to a user and the organisation. The case study also highlighted a positive impact on the security posture of the organisation which was measure using IT service request metrics.

Mohammed Alsadi, Matthew Casey, Constantin Catalin Dragan et al.

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, so the providers are trusted with ballot privacy and 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, allowing voters to verify that their vote 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. 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 uses trackers to enable voters to confirm that their votes have been captured correctly while protecting voter anonymity. This results in a system where even the election authority running the system cannot change the result in an undetectable way, and 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. We describe the results of two initial trials, which obtained that survey respondents found this form of verifiability easy to use and that they broadly appreciated it. We conclude by outlining the further steps in the road-map towards the deployment of a fully trustworthy online voting system.

Jinguang Han, Liqun Chen, Steve Schneider et al.

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 service requests of a user even if they collude. The novelty is that when a designated verifier is unavailable, a central authority can authorise new verifiers to authenticate the user on behalf of the original verifier. Furthermore, if required, a central verifier is authorised to deanonymise users and trace their service requests. We formalise the scheme along with a security proof and provide an empirical evaluation of its performance. This scheme can be applied to smart ticketing where minimising the collection of personal information of users is increasingly important to transport organisations due to privacy regulations such as General Data Protection Regulations (GDPR).

Jinguang Han, Liqun Chen, Steve Schneider et al.

Anonymous Single-Sign-On authentication schemes have been proposed to allow users to access a service protected by a verifier without revealing their identity which has become more important due to the introduction of strong privacy regulations. In this paper we describe a new approach whereby anonymous authentication to different verifiers is achieved via authorisation tags and pseudonyms. The particular innovation of our scheme is authentication can only occur between a user and its designated verifier for a service, and the verification cannot be performed by any other verifier. The benefit of this authentication approach is that it prevents information leakage of a user's service access information, even if the verifiers for these services collude which each other. Our scheme also supports a trusted third party who is authorised to de-anonymise the user and reveal her whole services access information if required. Furthermore, our scheme is lightweight because it does not rely on attribute or policy-based signature schemes to enable access to multiple services. The scheme's security model is given together with a security proof, an implementation and a performance evaluation.

Jinguang Han, Liqun Chen, Steve Schneider et al.

Electronic tickets (e-tickets) are electronic versions of paper tickets, which enable users to access intended services and improve services' efficiency. However, privacy may be a concern of e-ticket users. In this paper, a privacy-preserving electronic ticket scheme with attribute-based credentials is proposed to protect users' privacy and facilitate ticketing based on a user's attributes. Our proposed 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; (5) the security of the proposed scheme is formally proven and reduced to well known (q-strong Diffie-Hellman) complexity assumption; (6) the scheme has been implemented and its performance empirically evaluated. To the best of our knowledge, our privacy-preserving attribute-based e-ticket scheme is the first one providing these five features. Application areas of our scheme include event or transport tickets where users must convince ticket sellers that their attributes (e.g. age, profession, location) satisfy the ticket price policies to buy discounted tickets. More generally, our scheme can be used in any system where access to services is only dependent on a user's attributes (or entitlements) but not their identities.

Jorden Whitefield, Liqun Chen, Frank Kargl et al.

Research on vehicular networking (V2X) security has produced a range of security mechanisms and protocols tailored for this domain, addressing both security and privacy. Typically, the security analysis of these proposals has largely been informal. However, formal analysis can be used to expose flaws and ultimately provide a higher level of assurance in the protocols. This paper focusses on the formal analysis of a particular element of security mechanisms for V2X found in many proposals: the revocation of malicious or misbehaving vehicles from the V2X system by invalidating their credentials. This revocation needs to be performed in an unlinkable way for vehicle privacy even in the context of vehicles regularly changing their pseudonyms. The REWIRE scheme by Forster et al. and its subschemes BASIC and RTOKEN aim to solve this challenge by means of cryptographic solutions and trusted hardware. Formal analysis using the TAMARIN prover identifies two flaws with some of the functional correctness and authentication properties in these schemes. We then propose Obscure Token (OTOKEN), an extension of REWIRE to enable revocation in a privacy preserving manner. Our approach addresses the functional and authentication properties by introducing an additional key-pair, which offers a stronger and verifiable guarantee of successful revocation of vehicles without resolving the long-term identity. Moreover OTOKEN is the first V2X revocation protocol to be co-designed with a formal model.

Jens Bendisposto, Philipp Koerner, Michael Leuschel et al.

We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ZeroMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.

Steve Schneider, Helen Treharne, Heike Wehrheim et al.

Refinement in Event-B supports the development of systems via proof based step-wise refinement of events. This refinement approach ensures safety properties are preserved, but additional reasoning is required in order to establish liveness and fairness properties. In this paper we present results which allow a closer integration of two formal methods, Event-B and linear temporal logic. In particular we show how a class of temporal logic properties can carry through a refinement chain of machines. Refinement steps can include introduction of new events, event renaming and event splitting. We also identify a general liveness property that holds for the events of the initial system of a refinement chain. The approach will aid developers in enabling them to verify linear temporal logic properties at early stages of a development, knowing they will be preserved at later stages. We illustrate the results via a simple case study.