arXiv subjects

Mikael Asplund

Publications and source records attributed to Mikael Asplund.

8 recordsLinked to original sources

arXiv2026

AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation

Formal verification is a challenging but important task for ensuring the security of cryptographic protocols. While modern protocol verification tools significantly reduce verification effort, modelling remains challenging to practitioners without a background in formal verification. In addition, transferring verification results to a concrete protocol implementation requires expert knowledge. In this paper, we present a novel language-first method for verification of trace properties using a domain-specific language for protocol implementations. We target the Tamarin prover for verification, and we prove that verified universal trace properties translate back to the implementation. We additionally integrate symbolic execution in order to analyse the memory safety of protocol implementations. We use our tool to implement and generate accurate models for a signed Diffie-Hellman protocol, and for the WireGuard VPN protocol. Our WireGuard implementation is interoperable with existing implementations when using our interpreter, and achieves acceptable performance. We formally prove our implementations secure using a combination of symbolic execution and verification of the generated Tamarin models.

cs.CR↗

arXiv2026

Automated Generation of Cybersecurity Exercise Scenarios

There is a growing need for cybersecurity professionals with practical knowledge and experience to meet societal needs and comply with new standards and regulations. At the same time, the advances in software technology and artificial intelligence point towards a future where software agents will play an important role in protecting the computer systems that are critical for society to function. The training and development of both humans and software agents requires the design and execution of cybersecurity exercises that differ in properties such as size, scope, objectives, difficultly, etc. Cybersecurity scenarios are critical for the operation of cybersecurity exercises as they describe the scope, context, operational environment and storyline of each exercise. In this work, we present an approach to automatically generate cybersecurity scenarios that model enterprise IT systems. Our approach is able to generate a large number of scenarios that differ in multiple criteria including size, scope, difficulty, complexity and diversity. We further release as open source: a simulation and a virtualization environment that can run cybersecurity exercises based on the generated scenarios and a dataset containing 100000 sample scenarios.

cs.CR↗

arXiv2025

The Dark Side of Flexibility: How Aggregated Cyberattacks Threaten the Power Grid

Flexible energy resources are increasingly becoming common in smart grids. These resources are typically managed and controlled by aggregators that coordinate many resources to provide flexibility services. However, these aggregators and flexible energy resources are vulnerable, which could allow attackers to remotely control flexible energy resources to launch large-scale attacks on the grid. This paper investigates and evaluates the potential attack strategies that can be used to manipulate flexible energy resources to challenge the effectiveness of traditional grid stability measures and disrupt the first-swing stability of the power grid. Our work shows that although a large amount of power is required, the current flexibility capacities could potentially be sufficient to disrupt the grid on a national level.

cs.CR↗

arXiv2025

Towards Privacy-Preserving Anomaly-Based Intrusion Detection in Energy Communities

Energy communities consist of decentralized energy production, storage, consumption, and distribution and are gaining traction in modern power systems. However, these communities may increase the vulnerability of the grid to cyber threats. We propose an anomaly-based intrusion detection system to enhance the security of energy communities. The system leverages deep autoencoders to detect deviations from normal operational patterns in order to identify anomalies induced by malicious activities and attacks. Operational data for training and evaluation are derived from a Simulink model of an energy community. The results show that the autoencoder-based intrusion detection system achieves good detection performance across multiple attack scenarios. We also demonstrate potential for real-world application of the system by training a federated model that enables distributed intrusion detection while preserving data privacy.

cs.CR↗

arXiv2025

From Balance to Breach: Cyber Threats to Battery Energy Storage Systems

Battery energy storage systems are an important part of modern power systems as a solution to maintain grid balance. However, such systems are often remotely managed using cloud-based control systems. This exposes them to cyberattacks that could result in catastrophic consequences for the electrical grid and the connected infrastructure. This paper takes a step towards advancing understanding of these systems and investigates the effects of cyberattacks targeting them. We propose a reference model for an electrical grid cloud-controlled load-balancing system connected to remote battery energy storage systems. The reference model is evaluated from a cybersecurity perspective by implementing and simulating various cyberattacks. The results reveal the system's attack surface and demonstrate the impact of cyberattacks that can criticaly threaten the security and stability of the electrical grid.

cs.CR↗

arXiv2024

Automated Penetration Testing: Formalization and Realization

Recent changes in standards and regulations, driven by the increasing importance of software systems in meeting societal needs, mandate increased security testing of software systems. Penetration testing has been shown to be a reliable method to asses software system security. However, manual penetration testing is labor-intensive and requires highly skilled practitioners. Given the shortage of cybersecurity experts and current societal needs, increasing the degree of automation involved in penetration testing can aid in fulfilling the demands for increased security testing. In this work, we formally express the penetration testing problem at the architectural level and suggest a general self-organizing architecture that can be instantiated to automate penetration testing of real systems. We further describe and implement a specialization of the architecture in the ADAPT tool, targeting systems composed of hosts and services. We evaluate and demonstrate the feasibility of ADAPT by automatically performing penetration tests with success against: Metasploitable2, Metasploitable3, and a realistic virtual network used as a lab environment for penetration tester training.

cs.CR↗

arXiv2021

Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol

Vehicular networks will enable a range of novel applications to enhance road traffic efficiency, safety, and reduce fuel consumption. As for other cyber-physical systems, security is essential to the deployment of these applications and standardisation efforts are ongoing. In this paper, we perform a systematic security evaluation of a vehicular platooning protocol through a thorough analysis of the protocol and security standards. We tackle the complexity of the resulting model with a proof strategy based on a relation on keys. The key relation forms a partial order, which encapsulates both secrecy and authenticity dependencies. We show that our order-aware approach makes the verification feasible and proves strong authenticity properties along with secrecy of all keys used throughout the protocol.

cs.CR↗

arXiv2014

Modelling Correlated Mobility

When nodes in a mobile network cluster together or move according to common external factors (e.g., cars that follow the road network), the resulting contact patterns become correlated. In this work we address the question of modelling such correlated mobility movements for the analysis of intermittently connected networks. We propose to use the concept of node colouring time to characterise dynamic node contact patterns. We analyse how this model compares to existing work, and demonstrate how to extract the relevant data from actual trace files. Moreover, we show how this information can be used to derive the latency distribution of DTN routing protocols. Our model achieves a very good fit to simulated results based on real vehicular mobility traces, whereas models which assumes independent contacts do not.

cs.NI↗