The increasing integration of digital technologies in connected vehicles introduces cybersecurity risks that extend beyond individual vehicles, with the potential to disrupt entire transportation systems. Current practice (e.g., ISO/SAE 21434 TARA) focuses on threat identification and qualitative impact ratings at the vehicle boundary, with limited systemic quantification. This study presents a systematic, simulation-based methodology for quantifying the systemic operational and safety impacts of cyber threats on connected vehicles, evaluating cascading effects across the transport network. Three representative scenarios are examined: (I) telematics-induced sudden braking causing a cascading collision, (II) remote disabling on a motorway (M25) segment, and (III) a compromised Roadside Unit (RSU) spoofing Variable Speed Limit (VSL) and phantom lane closure messages to connected and automated vehicles (CAVs). The results highlight the potential for cascading safety incidents and systemic operational degradation, as evidenced by the defined systemic operational and safety vectors, factors that are insufficiently addressed in the current scope of the ISO/SAE 21434 standard, which primarily focuses on individual vehicle-level threats. The findings underscore the need to incorporate systemic evaluation into existing frameworks to enhance cyber resilience across connected vehicle ecosystems. The framework complements ISO/SAE 21434 by supplying quantitative, reproducible evidence for the impact rating step at a systemic scale, reducing assessor subjectivity and supporting policy and operations, enabling more data-driven evaluations of systemic cyber risks.

The Road Vehicles Cybersecurity Engineering Standard, ISO/SAE 21434, provides a framework for road vehicle Threat Analysis and Risk Assessment (TARA). The TARA framework must include Connected Vehicles (CVs) and their connectivity with external interfaces. However, assessing cyber-attack feasibility on CVs is a significant challenge, as traditionally, qualitative and subjective expert opinions are the norm. Additionally, there is a need for historical data on security-related incidents and dynamically evolving interconnected vehicle-to-everything (V2X) entities for feasibility assessment, which is not readily available. To address this problem, this paper presents, to the best of our knowledge, the first simulation-based TARA framework designed to characterise, quantify, and assess the Window of Opportunity (WO) for attackers—a metric that indicates the likelihood of an attack. A case study involving Bluetooth, with one attacker and one target, is modelled to demonstrate the proposed framework WOLVES’s applicability. Two scenarios have been investigated using different motorway roads in the UK. The primary outcome is the WOLVES framework, which employs a data-driven approach using both prior and likelihood information to estimate the probability of a successful cyber attack on a given technology in CVs. The findings from this research could assist threat analysts, decision-makers, and planners involved in CV risk assessment by enhancing the modelling of attack feasibility for cybersecurity threats in dynamic scenarios and developing appropriate mitigation strategies.

Modern vehicles are comparable to desktop computers due to the increase in connectivity. This fact also extends to potential cyber-attacks. A solution for preventing and mitigating cyber attacks is Over-The-Air (OTA) updates. This solution has also been used for both desktops and mobile phones. The current de facto OTA security system for vehicles is Uptane, which is developed to solve the unique issues vehicles face. The Uptane system needs to have a secure method of updating; otherwise, attackers will exploit it. To this end, we have developed a comprehensive and model-based security testing approach by translating Uptane and our attack model into formal models in Communicating Sequential Processes (CSP). These are combined and verified to generate an exhaustive list of test cases to see to which attacks Uptane may be susceptible. Security testing is then conducted based on these generated test cases, on a test-bed running an implementation of Uptane. The security testing result enables us to validate the security design of Uptane and some vulnerabilities to which it is subject.

Vehicular platooning is a promising technology for improving road safety, increasing vehicle efficiency, and reducing traffic congestion by enabling high-speed vehicles to travel in close formation with minimum inter-vehicular distance. However, a False Data Injection (FDI) attack can destabilise and break up vehicular platoons in several different ways. First, an attacker can inject false leave or split messages leading to a breakup of the vehicular platoon. Another way is by sending fake beacons or tampering information (such as speed, acceleration, distance, location etc) in a beacon. Upon receiving this false data, the platoon will destabilise as the members receives tampered information from the attacker. In this paper, we studied the impact of FDI attacks on the vehicular platoon by modifying significant information in a beacon. We carried out a simulation-based study, where a FDI attacker is modelled in Plexe simulator to attack a platoon. We considered two scenarios for an FDI attack, i.e., the attacker can be present both inside and outside of the platoon. Further, two flavours of FDI attacks are implemented, i.e., (1) Constant FDI: where, the attacker is launching FDI attack constantly throughout it’s journey, and (2) Intelligent On-Off FDI: where the attacker is performing FDI for short period of time and then hides his identity by performing legitimate communication with platoon members. We studied the impact of FDI attacks on vehicular platoons from three significant aspects: environmental (CO2emissions), safety (distance), and stability (speed). Our study showed that FDI attacks can have drastic impact on the vehicular platoons.

Resource-bounded alternating-time temporal logic (RB-ATL), an extension of Coalition Logic (CL) and Alternating-time Temporal Logic (ATL), allows reasoning about resource requirements of coalitions in concurrent systems. However, many real-world systems are inherently probabilistic as well as resource-bounded, and there is no straightforward way of reasoning about their unpredictable behaviours. In this paper, we propose a logic for reasoning about coalitional power under resource constraints in the probabilistic setting. We extend RB-ATL with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic Resource-Bounded ATL (pRB-ATL).

Many problems in AI and multi-agent systems research are most naturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by the availability of resources, and there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL). In this article, we describe a logic for reasoning about coalitional ability under resource constraints. We extend ATL with costs of actions and hence of strategies. We give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL) and a model-checking algorithm for it.

In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion is when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the K-Android tool, which provides an encoding of the Android/Smali code semantics within the K framework. K-Android allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.

Alternating Time Temporal Logic (ATL) is widely used for the verification of multi-agent systems. We consider Resource Agent Logic ( RAL ), which extends ATL to allow the verification of properties of systems where agents act under resource constraints. The model checking problem for RAL with unbounded production and consumption of resources is known to be undecidable. We review existing (un)decidability results for fragments of RAL , tighten some existing undecidability results, and identify several aspects which affect decidability of model checking. One of these aspects is the availability of a ‘do nothing’, or idle action, which does not produce or consume resources. Analysis of undecidability results allows us to identify a significant new fragment of RAL for which model checking is decidable.

Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable but EXPSPACE-hard. We also investigate some tractable cases and provide a detailed comparison to a variant of the resource logic RAL, together with new complexity results.

Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable.

Recent work on Alternating-Time Temporal Logic and Coalition Logic has allowed the expression of many interesting properties of coalitions and strategies. However, there is no natural way of expressing resource requirements in these logics. In this article, we present a Resource-Bounded Coalition Logic (RBCL) that has explicit representation of resource bounds in the language. We give a complete and sound axiomatization of RBCL, a procedure for deciding satisfiability of RBCL formulas, and a model-checking algorithm.