Abstract
Decryption errors play a crucial role in the security of KEMs based on Fujisaki-Okamoto because the concrete security guarantees provided by this transformation directly depend on the probability of such an event being bounded by a small real number. In this paper we present an approach to formally verify the claims of statistical probabilistic bounds for incorrect decryption in lattice-based KEM constructions. Our main motivating example is the PKE encryption scheme underlying ML-KEM. We formalize the statistical event that is used in the literature to heuristically approximate ML-KEM decryption errors and confirm that the upper bounds given in the literature for this event are correct. We consider FrodoKEM as an additional example, to demonstrate the wider applicability of the approach and the verification of a correctness bound without heuristic approximations. We also discuss other (non-approximate) approaches to bounding the probability of ML-KEM decryption.

Abstract
The relationship of a patient with a hospital from admission to discharge is often kept in a series of textual documents that describe the patient’s journey. These documents are important to analyze the different steps of the clinical process and to make aggregated studies of the paths of patients in the hospital. In this paper, we explore the potential of Large Language Models (LLMs) to generate realistic and comprehensive patient journeys in European Portuguese, addressing the scarcity of medical data in this specific context. We employed Google’s Gemini 1.5 Flash model and utilized a dataset of 285 European Portuguese published case reports from the SPMI website, published by the Portuguese Society of Internal Medicine, as references for generating synthetic medical reports. Our methodology involves a sequential approach to generating a synthetic patient journey. Initially, we generate an admission report, followed by a discharge report. Subsequently, we generate a comprehensive patient journey that integrates the admission, multiple daily progress reports, and the discharge into a cohesive narrative. This end-to-end process ensures a realistic and detailed representation of the patient’s clinical pathway as a patient’s journey. The generated reports were rigorously evaluated by medical and linguistic professionals, as well as automatic metrics to measure the inclusion of key medical entities, similarity to the case report, and correct Portuguese variant. Both qualitative and quantitative evaluations confirmed that the generated synthetic reports are predominantly written in European Portuguese without the loss of important medical information from the case reports. This work contributes to developing high-quality synthetic medical data for training LLMs and advancing AI-driven healthcare applications in under-resourced language settings.

Abstract
The interaction between code and language shapes emergence and innovation in computational systems, turning them not merely into a series of connected structures but into narrative spaces. Interactive Digital Narratives (IDNs) are characterized by a tension between the control exerted by the system to engage readers and the autonomy that readers desire over the narrative's direction. This results in a ludic paradox, where the role of the narrative system is to enable and facilitate play while simultaneously being capable of communicating the outcomes of the readers' actions. On the other hand, the reader must be able to participate actively by playing along the system's rules. Based on the notion of interpassivity, which refers to the delegation of the cognitive activity to the object, thus transforming the reader into a passive observer of the system's interactions, this paper aims to explore the interplay between interpassivity and interactivity. As we navigate IDNs, we engage with narratives that challenge and empower readers, that create immersive and enriching experiences, and transform their relationships with the computational system. This contributes to understanding the pleasure of playing and the reader's role. Based on the premise that readers can derive pleasure from automation but also yearn for control over the narrative, we can investigate the playful interaction between humans and machines. This paper will analyze Emissaries (2015-2017), defined by its creator, Ian Cheng, as a video game that plays itself, and where the reader can seemingly only visualize the work. In this case study, we will look for narrative mechanics and the specificity of the medium in which the IDN is instantiated. We will discuss how the computational system actively shapes the narrative without direct reader input and consequently propose a reconceptualization of the concept of interpassivity and its relationship with interactivity.

Abstract

Abstract
We revisit the privacy and security analyses of FIDO2, a widely deployed standard for passwordless authentication on the Web. We discuss previous works and conclude that each of them has at least one of the following limitations: (i) impractical trusted setup assumptions, (ii) security models that are inadequate in light of state of the art of practical attacks, (iii) not analyzing FIDO2 as a whole, especially for its privacy guarantees. Our work addresses these gaps and proposes revised security models for privacy and authentication. Equipped with our new models, we analyze FIDO2 modularly and focus on its component protocols, WebAuthn and CTAP2, clarifying their exact security guarantees. In particular, our results, for the first time, establish privacy guarantees for FIDO2 as a whole. Furthermore, we suggest minor modifications that can help FIDO2 provably meet stronger privacy and authentication definitions and withstand known and novel attacks.

Abstract
This study aims to explore how civil society contributes to the promotion, governance, and sustainability of urban forests, particularly through its interactions with local governments and the private sector. Drawing on a qualitative analysis of 118 urban forest projects in Portugal, the research identifies the key civil society actors involved and examines mechanisms of collaboration in urban forest governance. Findings highlight that sustainable urban forests are most effective when managed as socioecological systems co-governed by multiple stakeholders. Practices such as knowledge co-production, participatory policy design, and community-driven action emerged as central elements. NGOs, associations, and universities play a crucial role as intermediaries, forming “green social infrastructures” that connect technical expertise with local aspirations. The study also reveals innovative forms of adaptive governance, including living labs and regenerative multi-actor networks. However, it identifies a critical weakness: the lack of formal integration of these collaborative practices into urban planning instruments. Theoretically, the study reinforces hybrid and experimental governance frameworks. Practically, it calls for public policies that institutionalise collaborative networks, ensuring continuity and systemic impact. The role of government as a strategic facilitator is emphasised to link grassroots innovation with long-term urban planning. © 2025 Elsevier B.V., All rights reserved.