Deploying secure communication protocols remains a challenging task. To ensure that intended security properties hold, formal verification has become increasingly important. In this work, we present a translation from the design-oriented Alice Bob language to the implementation-level language F*, leveraging the DY* library’s verification capabilities. Our approach addresses the expressiveness gap between abstract specifications and concrete implementations by generating verifiable F* code that benefits from its dependent-type system. This integration of model-driven development with dependent types enables the specification and proof of security properties directly at the implementation level. As a result, users, even those without expertise in formal methods, can start from an intuitive Alice Bob notation and obtain a formally backed implementation that can be enriched with features not expressible in Alice Bob, while preserving correctness through re-verification. We demonstrate the effectiveness of this workflow through the generation and verification of several real-world security protocols, showcasing an end-to-end approach to verified protocol implementation.
The expansion of Internet of Things (IoT) applications in sixth-generation (6G) networks creates new security risks that centralized intrusion detection systems cannot adequately address due to scalability limits, communication overhead, and privacy exposure. We propose a federated learning (FL)-based intrusion detection framework augmented with differential privacy (DP) to protect sensitive data while supporting large-scale IoT deployments. The framework trains models collaboratively across distributed nodes with privacy-preserving updates. Evaluation on benchmark IoT traffic datasets under varied attack scenarios shows that FL with DP maintains high detection accuracy, mitigates information leakage, and scales effectively. These results demonstrate the feasibility of combining FL and DP to deliver robust, privacy-preserving intrusion detection for next-generation IoT networks.
Malicious actors can introduce poisoned data by exploiting security vulnerabilities that may be present anywhere in networked systems. Depending on how the data is processed and used, this can have severe and potentially catastrophic effects. Using the data produced in such systems for the generation and evaluation of Artificial Intelligence (AI)/Machine Learning (ML) models, one may identify if malicious data is being introduced, though not necessarily where the intrusions occur. In this work we exploit the availability of metadata that is associated with the security context in which data is collected, transported and processed, as would be available, for example, in a data confidence fabric. We use this metadata in combination with iterative data weighting informed by that context. This facilitates the isolation of potential attack vectors or vulnerabilities by systematically training and evaluating low-impact AI/ML models while adjusting individual context weighting to discover the outlier features. With this approach, we can identify specific security or safety contexts of high significance based on anomalous impacts on model accuracy and loss evaluation computations.
This paper introduces a grammar-driven approach to model and detect sequences of Advanced Persistent Threat (APT) attacks. APTs are characterized by their complexity and multi-step nature, making them challenging to detect with traditional systems. The proposed method employs interpretable rules to capture malicious behaviors and aligns semantically with the MITRE ATT CK framework. This approach enables the detection of plausible attack scenarios even in the presence of incomplete or noisy data. We evaluate it using a public large CTF dataset which provides realistic and diverse attack scenarios. Experiments illustrate the effectiveness of the method in reconstructing plausible attack progressions, even with incomplete data. The main contribution of this study is an open-source implementation in Rust, ensuring reproducibility and extensibility. We also propose future enhancements to better model contextual dependencies between tactics in APT attack sequences. In a nutshell, this grammatical approach offers a robust method for detecting sophisticated threats, bridging the gap between low-level observations and high-level strategic reasoning.
Cyber resilience requirements may be implemented either to comply with regulatory obligations or to align with industry best practices. They enable organizations to demonstrate that they are capable of anticipating, withstanding, recovering from, and adapting to difficult situations and stresses. In this context, metrics can be used in a structured way to demonstrate these capabilities. These are conceptual data repositories that define and standardize information. They must be clearly defined, effectively implemented, and continuously monitored. According to [30] metrics are measures and assessment results intended to track progress, support decision-making, and enhance performance against defined targets. In this paper, we propose an approach for eliciting and selecting cyber resilience metrics that considers the enterprise architecture layers defined by TOGAF. Once selected, we propose a quantitative approach to evaluate the cyber-resilience level of a capability and a Petri net model to represent the interdependencies between cyber-resilience across the enterprise architecture layers.
