Abstract
SPHINCS+ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conservative option for post-quantum signatures, but the original tight proofs of security were flawed- as reported by Kudinov, Kiktenko and Fedorov in 2020. In this work, we formally prove a tight security bound for SPHINCS+ using the EasyCrypt proof assistant, establishing greater confidence in the general security of the scheme and that of the parameter sets considered for standardization. To this end, we reconstruct the tight security proof presented by Hulsing and Kudinov (in 2022) in a modular way. A small but important part of this effort involves a complex argument relating four different games at once, of a form not yet formalized in EasyCrypt (to the best of our knowledge). We describe our approach to overcoming this major challenge, and develop a general formal verification technique aimed at this type of reasoning. Enhancing the set of reusable EasyCrypt artifacts previously produced in the formal verification of stateful hash-based cryptographic constructions, we (1) improve and extend the existing libraries for hash functions and (2) develop new libraries for fundamental concepts related to hash-based cryptographic constructions, including Merkle trees. These enhancements, along with the formal verification technique we develop, further ease future formal verification endeavors in EasyCrypt, especially those concerning hash-based cryptographic constructions.

Abstract
Capricious data streams make no assumptions on feature space dynamics and are mainly handled based on feature correlation, linear classifier or ensemble of trees. There exist deficiencies such as limited learning capacity, high time cost and low interpretability. To enhance effectiveness and efficiency, capricious data streams are handled through a single tree in this paper, and the proposed algorithm is named OCFHT (Online learning from Capricious data streams with Flexible Hoeffding Tree). OCFHT does not rely on the correlation pattern among features and can achieve non-linear modeling. Its performance is verified by various experiments on 18 public datasets, showing that it is not only more accurate than state-of-the-art algorithms, but also runs faster. Copyright © 2025 held by the owner/author(s).

Abstract
Underwater environments pose unique challenges to optical systems due to physical phenomena that induce severe data degradation. Current imaging sensors rarely address these effects comprehensively, resulting in the need to integrate complementary information sources. This article presents a multimodal data fusion approach to combine information from diverse sensing modalities into a single dense and accurate tridimensional representation. The proposed fusiNg tExture with apparent motion information for underwater Scene recOnstruction (NESO) encoder-decoder network leverages motion perception principles to extract relative depth cues, fusing them with textured information through an early fusion strategy. Evaluated on the FLSea-Stereo dataset, NESO outperforms state-of-the-art methods by 58.7%. Dense depth maps are achieved using multi-stage skip connections with attention mechanisms that ensure propagation of key features across network levels. This representation is further enhanced by incorporating sparse but millimeter-precise depth measurements from active imaging techniques. A regression-based algorithm maps depth displacements between these heterogeneous point clouds, using the estimated curves to refine the dense NESO prediction. This approach achieves relative errors as low as 0.41% when reconstructing submerged anode structures, accounting for metric improvements of up to 0.1124 m relative to the initial measurements. Validation at the ATLANTIS Coastal Testbed demonstrates the effectiveness of this multimodal fusion approach in obtaining robust tri-dimensional representations in real underwater conditions.

Abstract
This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

Abstract
By connecting maritime and land transport, container terminals play a critical role in global logistics systems, as part of broader intermodal networks. The evolution of containerisation and technological advances, along with increased demand and volumes, led to significant adaptations in these terminals, as a way to improve productivity, reduce costs and increase competitiveness, while coping with spatial and operational constraints. For strategic decision-making, managing these complex systems can be enhanced by simulation models allowing the analysis of different scenarios in dynamic, uncertain environments. This work, presents a simulation-based decision support tool developed in the FlexSim software, to analyse different container terminal configurations, with a particular focus on automation and on sustainable practices to reduce the energy consumption of terminals. A discrete event simulation model was developed to study multiple scenarios impacting productivity, resource utilisation, and waiting times. The proposed approach allows the test and evaluation of management strategies for port operations, with preliminary results showing that sizing and planning of the fleets of automated guided vehicles (AGV) can significantly affect the total operating time, the energy consumed, and the costs associated with battery charging operations. Future research should explore additional factors affecting container terminal operations, such as the reorganisation of the storage area, while incorporating optimisation elements for work planning and resource allocation. Moreover, the simulation model will be tested and validated in a real case study, designed for the Port of Sines in Portugal. © 2024 The Authors.

Abstract