We propose how attack trees formalism can be extended with time constraints. An attack tree is a basic description of how an attacker can compromise an asset, we refine this basic description by adding time constraints which can prevent an attacker from reaching the root node, if the attack actions performed cannot be completed within the defined time constraint. Adding time to attack trees causes an infinite number of possible states, to overcome this problem, we translate the tree into (an extended version of) timed automata and later use UPPAAL verification tool to analyse.
Attack tree’s security. The revolution that brought the introduction of assets such as IoTs, CPS,
and industrial control systems etc., in the last decades also brought many security challenges.
At its inception, attack trees are used to model how an asset (mostly static) may be compromised
and allow a security engineer to plan on how to address the potential security threats. For
example, in its early days, attack trees were used to model how to gain access (open) to secure
documents, how a PGP encrypted file or password can be cracked, potential ways to infect a
system files with a virus, how unauthorized users can obtain admin privileges, and how to gain
remote access to a system [
The settings of (traditional) attack trees are to depict (static) varying ways an asset may be
compromised. However, most assets nowadays have erratic behaviour and can interact with
other (sub)systems. This makes their vulnerabilities change according to the threat environments.
Therefore, to capture such dynamism using attack trees, the estimated annotations (i.e. nodes)
need to be updated regularly. Attempts have been made to extend attack trees through the
introduction of attack-defence trees [
In this paper we push forward our approach, we formally defined attack trees with time constraints, we provided a case study to highlight situations where such model is applicable. Also, we translated the concept into a (weighted) timed automata, and use a formal verification tool UPPAAL to analyse. Let be a parent node that is associated with a gate refinement, assume we want to prevent an attacker from achieving the parent node. We introduce a set of constant time intervals that is represented by a constant pair < , >, with marking the start of an attack and marking the end of the attack on a parent node. , ∈ Q, and ≤ . We associate the set of attack actions with a set of attack time . An attack time defines the attack execution time for each action. To reach to the parent node, the attack time ∈ for each action on a given child node under attack has to be less than or equal to the interval. In other words, if the attack time for child node(s) is more than the interval, the attacker cannot reach to the parent node. We formalized this idea and translated the parent node reachability to state reachability of timed automata.
Related work. Currently, threat modelling methods commonly used in industry mainly
include graphical models, such as attack trees [
Unlike the works mentioned here, our work focus on traditional attack trees without considering defence nodes/actions. In our view, as mentioned earlier, defence actions are efective only to pre-identified vulnerabilities. As such cannot be applied to a (new) set of attack surface that emerged as a result of a change in the vulnerabilities landscape of the asset; modelled in an attack tree. Therefore, we shift our focus on preventing attacks by introducing a set of time constraints at the parent nodes; in addition to the gate refinement of the tree. We introduce a set of time constraints that is represented by a constant pair < , >, with marking the start of an attack and marking the end of the attack on a parent node. , ∈ Q, and ≤ . We associate the set of attack actions with a set of attack time . An attacker can achieve the parent node if and only if the attack action(s) together with the attack time can be executed within the defined constant time intervals. To model the time constraints, we translate the tree into a parallel composition of weighted timed automata (WTA). The sets of nodes of the attack trees are translated to a set of locations in the weighted timed automata. For each leaf node in the attack tree, we have an automaton that represents a linear path from the leaf to the root node. Altogether their areas many WTAs as the leaf nodes in the attack tree. Each location that represents a leaf has a clock that is activated when there is an attack in the corresponding leaf in the tree. A transition is enabled only if a simple attack is successful in the attack tree.
The paper is organized as follows. In Section 2 we describe attack trees formalism. In Section 3 we present the motivation for enhanced restrictions on attack trees model, and why time constraint is a good option. In Section 4 we present time constraint as a form of security in attack trees, and Section 5 timed automata and the translation of attack trees with time constraint into (weighted) timed automata. Section 6 contains discussions and plans for future work.
In this section, we describe and define attack trees. An attack tree is a graphical way of describing
varying ways an asset may be compromised by a malicious user (an attacker). The structure
of attack trees we use in this paper is based on the existing model introduced by Schneier [
Definition 1. An attack tree is a tuple = (, 0, , , ℰ , ) where, is a finite set of nodes, 0 is the root node of the tree, , ⊆ are two subsets such that ∪ = and ∩ = ∅, ℰ ⊆ × is a set of edges, connecting the nodes, and : {0} ∪ → { , } is a mapping that associate some nodes to a gate.
Steal a car attack tree (A)
An attack tree with time constraint (B)
Note, to compromise nodes in the tree, an attacker needs to perform a set of attack actions. These set of (possible) actions are denoted by , and we defined an attack as a mapping : → ∪ { } such that () = means that an attacker can compromises leaf node ∈ by executing an action ∈ , () = Nil when no action is performed. We say that attack is simple if () ̸= Nil only for one leaf i.e. only one leaf is attacked. Practically, these set of attack actions are aided by the use of tools or/and techniques to carry out the attack. Therefore, in this work, we will name a tool that can aid an attacker in executing the attack when referring to attack process in the working examples.
Example 1. Shown in Figure.1 (A) is a simple attack tree that depicts possible ways to steal a car. The car can be stolen by achieving the sub-goal obtain key or short-circuit. To obtain the key, the sub-goal is of refinement and therefore, an attacker must either steal the key or make a copy. While to achieve short-circuit, the sub-goal is of refinement and the attacker must get access interior, find ignition cable, and connect the cable. Since the nodes must be achieved sequentially, in this case the gate is said to be extended to (sequential ). Linked with dotted lines (below the tree) are a set of aided tools or/and techniques, and an attack is performed when a tool is mapped to a node i.e. (make copy) = key cutter.
To model the attack propagation (i.e. from leaf nodes, through sub-goals to root), we define a state of attack tree, denoted by i.e. state after an attacker has performed some actions from . A state of attack tree is defined as a set of nodes, and for each successful execution of attack actions (depending on the gate refinement of the target state), an attacker progresses to another state. An initial state is denoted by 0. Let be a state of an attack tree, and let be an attack. The transition : (, ) → ′ defines a change in state from , when an attack is performed, to state ′ . We define this for simple attacks but it can be extended for arbitrary ones.
Definition 2. Let be a simple attack such that () = and let be an attack state. Then the next state ′ after attack is defined as ′ = ( ∪ ) where operation on the set of nodes is defined as follows: ′ = () if ′ is the smallest set with the following properties • ⊆ ′ • if is a sub-goal that is associated with gate and all its child nodes are in () then ∈ () • if is a sub-goal that is associated with gate and at least one of its child node is contained in () then ∈ (), A state is called final if it contains the root node. The transitive closure of defines reachability and will consider only states reachable from 0 by some attacks. Henceforth, we will use the notation → ′ instead of : (, ) → ′ . In the following lemma, we can see that an attack can be decomposed into simple attacks, however, the order of executing the attacks is important in succeeding.
Lemma 1. Given an attack tree . Let 1, 2 be two simple attacks and is a state. Then →12 ′ ̸= 21 ′, i.e. attacks are asymmetry.
→ Proof 1. By example. State is composed of all the nodes needed to reach ′, while ′ contains all the nodes attacked by 1 and 2. As we can see from example 1, it is impossible to connect the cable before accessing the interior and/or before finding the ignition cable. As such ordering of attacks has influences on multiple simple attacks.
Example 2. Let , ′ be a state and its successor respectively. Suppose from Fig.1 (A) to access the interior, an attacker needs a plier. Then a transition → ′ if (access interior) = plier.
In this section, we will present motivations for a new security concept that will be formally introduced in the next section. We start by presenting why it is important to have enhanced restrictions in attack trees that will serve as a form of security in addition to identifying varying ways an asset (modelled with attack trees) may be compromised. But first, we start by explaining enhanced restriction and why it is needed.
An attack tree is a basic description of how an attacker may compromise an asset, without
the description of how to prevent or repel the attack. This can play well into potential attackers;
by analysing an asset using attack trees to identify the set of vulnerabilities. The gates describe
an order (restriction) that guides how a set of parent nodes can be achieved. For example, the
gate refinement required an attacker to execute attack on all the child nodes (link to a
parent node) before the attack succeeds. A more restrictive version of this was proposed in [
Attack Scenario: Assume that an auto company developed an app tool that connects its customers with the service centre for • technical analysis: whereby, some sensors in the vehicle can send data back to the manufacturer for intelligent and autonomous vehicle studies, • threat analysis: whereby, safety or/and varying ways a vehicle can be in danger is identiifed and cautions message sent to the user.
Combined this, a security threat analysis of the vehicle can be carried out based on the threat environment (i.e. vehicle moving or parked), at each instance; an attack tree identifies potential threats and display either in the vehicles’ onboard TFT LCD screen display or/and the user mobile phone as a notification. For each identified possible threat/fault, the app indicates the originating location (leaf node), other components in the vehicle that can be afected (sub-goals) and the resultant efect/damage (attack goal). Potential adversaries to the vehicle are classified as follows: • an insider: someone with close relation to the auto company i.e. rough employee that directly/indirectly misuses his/her privileges, • generic attacker: someone with the intention to exploit vulnerabilities, that can result in putting the vehicle to harm, • component failure: part of vehicle components with rust/ware-out that can lead to damages.
For this paper, we will model working examples from a single threat environment i.e. the vehicle is at a parked position, and in our future work, we will consider working with a dynamic threat environment. Now, consider the vehicle user who is notified (by the app) of potential danger. Even though the attack tree can (correctly) show the originating point and target, the user cannot prevent or slow down the attack process.
Example 3. Let us revisit example 1. let us assume a case whereby an attacker has already made some progress with the attack (i.e. access interior and locate ignition cable) and (s)he is interrupted. By the settings of traditional attack trees model, the attacker is not restricted from returning later in time to complete the attack, or with the previous knowledge, restart the attack process.
It is important that, apart from identifying possible ways the attacker can achieve the target, a security measure is defined that will constrain the attacker from unlimited attempts.
In this section, we extend the set of gates refinement with a set of time constraints. The time constraints is an addition to the already existing gate refinement that is associated with each parent node. We also associate each attack action with an attack time, indicating the time needed for an attacker to complete executing the action.
Given a set of attack actions , we introduce a set of attack time . is the time needed to complete an action that can result in compromising a node, denoted simply by (, ) ∈ × (see Figure.1 (B)). By doing so, we are extending the attack definition (defined in section 2) by : → ( × ) ∪ { }. The set of gates refinements mapping is also extended with a set of time constraints that is represented by a constant pair ⟨, ⟩, with marking the start of an attack and marking the (expected) end of attack on the parent node such that , ∈ Q, and ≤ . This allows us to redefine the gates refinement mapping as : {0} ∪ → {, } × . For the sake of simplicity, we denote this as ⟨, ⟩. From the graphical representation shown in Figure.1 (B), one can easily derive these time extensions whereby ⟨0, 0⟩, ⟨1, 1⟩, and ⟨2, 2⟩ is added to the parent nodes (root node and sub-goals), meaning they can only be reached if an attacker can execute the attack within the interval respectively. Also, below with the dotted lines, attack time is added to each action, where ∈ {1 . . . 6}. Regardless of the gates refinement i.e. , , an attack can only succeed if the action(s) execution time does not exceed the time intervals at the gates of the (parent) node. Example 4. Let us consider attack tree shown in Figure.1(B), the parent nodes are extended with time intervals represented as pairs ⟨0, 0⟩ for the root node, ⟨1, 1⟩ for the sub-goal, and ⟨2, 2⟩ for the sub-goal. The attack actions (represented by tools) are also extended with attack time. Each time indicates the time needed to complete the attack. From the initial attack attempt, an attacker has until elapsed of to complete the attack, otherwise the whole attack process is consider failed. If is larger than the constant time interval for the connected sub-goal, the attack cannot succeed.
Definition 3. Attack trees with time constraint. Let (, ℰ ) be a tree, an attack tree with time constraint is a tuple = (, 0, , , ℰ , , , , ), where, is a finite set of nodes, 0 is the root node of the tree that represents the attack target, , ⊆ are two subsets such that ∪ = and ∩ = ∅, ℰ ⊆ × is a set of edges that connect the nodes, is a set of time constraints, : {0} ∪ → { , } × is the mapping that associate some nodes to a gate and time constraint, is a set of attack time, and : → ( × ) ∪ { }. Definition 4. Given an attack tree with time constraint , an attack over the tree that can reach to the root node is defined as (assuming ∈ , ∈ and ∈ ) • If the tree has gates, ∀1 . . . : ∀ . . . are less than or equal to the constant time interval on the parent node, • If the tree has gates, ∃ : is less than or equal to the constant time interval on the parent node.
As an example, let us consider a sub-goal short-circuit from Figure. 1 (B), an attacker can succeed in achieving the sub-goal if and only if the summation of attack time 3 + 4 + 5 does not exceed the time interval defined at ⟨, ⟩.
From Figure.1 (B), () = Nil if the attacker cannot complete the attack within the time constraint at the gates. The following lemma guarantees that under some conditions a parent node remains unreachable to a potential attacker regardless of the gate refinement associated with the parent node.
Lemma 2. Given a sub-goal , a set of time constraint defined at the gate refinement ⟨, ⟩, and a set of attack (actions) ⊆ required to compromise . The sub-goal is unreachable to an attacker if the attack execution time ∀ ∈ exceeds the attack time defined at the gate refinement. Proof 2. Since each action has an attack time, we need to show that this attack time for all the child nodes of exceeds the time constraint at the gate. Now if this action cannot be executed within the attack time, the sub-goal cannot be achieved.
There are some relations between time constraint on the gates refinement and improved security for diferent kinds of systems; in general. For example, the use of idle time outs for web session is a common practice in the development of high-risk applications such as online banking platforms. Other instances where time constraint is used to improve the security of asset can be found on e-locks (eg. car central locking system) that can automatically locked itself after a specified passage of time [ 23]. The implementation of time restriction such as action time-out in assets such as ATMs [15], and SMART-doors [24] are further good examples.
In addition to other extensions of attack trees with security mechanism such as defence nodes or attack countermeasures, time constraint can be used to model and analyse diferent kinds of attack scenarios for diferent kinds of assets.
As in [
Definition 5. A timed automaton is a tuple = (ℒ, ℒ0, E, , ℐ, , ), where ℒ is a finite set of locations, ℒ0 ⊆ ℒ is a set of initial locations, E is a finite set of synchronization actions (events), is a finite set of clocks, ℐ : ℒ → Φ( ) is an invariant, assigning to every location ∈ ℒ a clock constraint, ⊆ ℒ × E × Φ( ) × 2 × ℒ is a set of transition relations such that ⟨, , , , ′ ⟩ represents an edge from location to location ′ on symbol . is a clock constraint, ⊆ is a set of clocks to be reset, and is a final location.
The semantics of a timed automaton is defined by associating a (labelled) transition system (defined in section 1) with it. A state in consists of a pair (, ) whereby is a location of and indicates that for a clock , satisfies the label constraint ℐ().
In this subsection, we introduce the basics of a WTA and give the translation of attack trees with time constraint into a WTA.
A Weighted timed automata, otherwise known as price timed automata (PTA), is an extended version of timed automata (TA) with weight/cost information added on both locations and edges. To arrive at a location, the weight value defined at that location has to be satisfied, also, to enabled a transition via an edge, the weight value at that edge has to be satisfied. At the ifnal/desired location, a global weight/cost which is the accumulated weight/cost along the run is calculated. With this accumulative weight/cost value, it is easy to calculate the distance or cost of travelling from point to point in diferent case studies. Formally, a weighted timed automata is defined as follows [25].
Definition 6. The tuple = (ℒ, ℒ0, E, , ℐ, , , ) is a weighted timed automaton, where ℒ is a finite set of locations, ℒ0 ⊆ ℒ is a set of initial locations, E is a finite set of synchronization actions (events), is a finite set of clocks, ℐ : ℒ → Φ( ) is an invariant, assigning to every location ∈ ℒ a clock constraint, : ℒ ∪ E → N≥ 0 is a function that assigns weight value to location and edge, : → Q is a set of weight parameters that updates the weight value : → ( ∪ ), is a set of transitions such that ⟨, , , , , ′ ⟩, where , ′ ∈ ℒ are the source and target locations, is a clock constraint, ∈ E, ⊆ is a set of clocks to be reset, and is a parametric weight update, and finally is a final location.
The trace of a weighted timed automata is a sequence of states with the transitions across the states given as = 0 →−00 0 1 →−11 1 2... such that • there is always an initial location 0 with an initial clock valuation 0 = 0, • for every ∈ {1, .., }, there is some transition (, , , , , +1) ∈ , • a transition is enables only if; for every clock valuation , there exists a constraint such that satisfies , • for every successful transition, a new clock valuation +1 is obtained by increasing every clock variable in by a transition and resetting all previous clocks 0.
Now, in other to analyse attack trees with time constraint using UPPAAL, we translate the tree into a parallel composition of weighted timed automata. The sets of nodes of the attack trees are translated to a set of locations in the weighted timed automata. For each leaf node in the attack tree, we have a WTA that represents a linear path from the leaf to the root node. Altogether there are as many WTAs as the leaf nodes in the attack tree. Each location that represents a leaf which has a clock that is activated when there is an attack in the corresponding leaf in the tree. An attack on a node in the tree represents an enabled transition in the WTA. Initially, clocks become active when events synchronized, and end with either a success or fail synchronization action.
More general, an attack tree is translated into a parallel composition of weighted timed automata 1 . . . that represents linear path from the leaf to the root node. Given an attack tree with time constraint , the semantics of successfully reaching the root node that satisfies the weighted timed automata WTA can be given as JK ⊆ WTA if • J0K = {WTA1 . . . WTA}such that at least WTA reached the
= WTA, a final location ∈ WTA is always satisfied, • JK
ifnal location , • JK = {WTA1 . . . WTA}such that for all A, the final location reached. Lemma 3. Let be an attack tree with time constraint and let be the equivalent product of weighted timed automata. Suppose is a (target) node, and location is the (equivalent) translation in . The number of the active clock(s) in to reach , is the same as the number of (attack) actions carried out by an attacker before reaching .
Proof 3. We know that a clock is reset for each enabled transition in WTA, therefore, since the locations of corresponds to the nodes in the attack trees, each enabled clock indicates an active attack on a node. As such, the number of attack executed will correspond to the number of clock(s) reset for events in the .
Theorem 1. Let be a product of weighted timed automata for the translation of . For a transition (, , , , , +1), the clock is inactive for a corresponding node ∈ in the tree, if there is no active attack process on that node.
Proof 4. Directly from lemma 3.
We can model an attack as a special weighted timed automata, and denote it as , this weighted timed automata shows the attackers’ action and time when they are performed on the attack tree. We use this in the following theorem to check the attack target (root node) reachability for both the attack tree and the WTA.
Theorem 2. Given an attack tree with time constraint and a time automata , an attacker can only reach the root node of the tree {0} if corresponding plus running with the attack path in the tree can reach the final location.
Proof 5. The main idea. We know that a root node can only be reached if an attacker can succeed in completing the attack process. Therefore we have to show that a plus can also reach the final location.
Uppaal accepts the synchronization of events using channels (input and output). As such, we modelled a set of events ?, ?, ?, ? (receive) at the initial location to serve as a set of leave nodes. We use two clocks and , with being a clock associated with each event while associated with a target location. Here, is a clock to track . We also define two invariant and , to check whether both and are satisfied before the transition to the target location is enabled.
The UPPAAL template shown in Figure.2 is a simple model of time constraint in achieving nodes in an attack trees. The leaves locations begin by waiting for the activation of signal by one of the events ?, ?, ?, ? An event become activate only when the clock is less than (predefined) . If the sub_goal location is of gate, the activation of a single event is enough for the transition to be enabled to the target location (sub_goal), otherwise all the events (i.e. gate) needs to be activated, and the sub_goal location can only be reached if the clock is less than (predefined) .
In this paper, we have presented attack trees with a time constraint to serve as a secured version of attack trees. We discussed how the gates refinement can be extended with time parameters and also propose how the attack trees with time constraint can be modelled using a formal verification tool UPPAAL.
As further work, we plan to study how attack trees can be used to analyse a CPS. A CPS is a special kind of asset that can interact with objects from the physical environment as well as other cyber-systems. This allows its operations to run parallel and concurrent, making it easy for a potential attacker to observe (from the physical components), and perform some dangerous attacks such as message falsification attack, DoS, message spoofing etc. by simply adding, blocking or blurring the objects from the physical environment. This kind of threats cannot be captured using attack trees alone. We plan to investigate opacity, a security property formalizing the information leakage of a system to an external observer, namely intruder and study how it can be used with attack trees.
This work was supported by the Slovak Research and Development Agency under the Contract no. APVV-19-0220 (ORBIS) and by the Slovak VEGA agency under Contract no. 1/0778/18 (KATO). [14] R. Alur, Timed automata, in: International Conference on Computer Aided Verification,
Springer, 1999, pp. 8–22. [15] B. Berthomieu, M. Diaz, Modeling and verification of time dependent systems using time petri nets, IEEE transactions on software engineering 17 (1991) 259. [16] L. S. Shapley, Stochastic games, Proceedings of the national academy of sciences 39 (1953) 1095–1100. [17] K. Lounis, S. Ouchani, Modeling attack-defense trees’ countermeasures using continuous time markov chains, in: International Conference on Software Engineering and Formal Methods, Springer, 2020, pp. 30–42. [18] R. Kumar, E. Ruijters, M. Stoelinga, Quantitative attack tree analysis via priced timed automata, in: International Conference on Formal Modeling and Analysis of Timed Systems, Springer, 2015, pp. 156–171. [19] O. Gadyatskaya, R. R. Hansen, K. G. Larsen, A. Legay, M. C. Olesen, D. B. Poulsen, Modelling attack-defense trees using timed automata, in: International Conference on Formal Modeling and Analysis of Timed Systems, Springer, 2016, pp. 35–50. [20] R. R. Hansen, P. G. Jensen, K. G. Larsen, A. Legay, D. B. Poulsen, Quantitative evaluation of attack defense trees using stochastic timed automata, in: International Workshop on Graphical Models for Security, Springer, 2017, pp. 75–90. [21] I. A. Tøndel, M. G. Jaatun, M. B. Line, Threat modeling of ami, in: Critical Information
Infrastructures Security, Springer, 2013, pp. 264–275. [22] A. E. M. AL-Dahasi, B. N. A. Saqib, Attack tree model for potential attacks against the scada system, in: 2019 27th Telecommunications Forum (TELFOR), IEEE, 2019, pp. 1–4. [23] D. Ray, The time structure of self-enforcing agreements, Econometrica 70 (2002) 547–582. [24] J. Padhye, V. Firoiu, D. Towsley, J. Kurose, Modeling tcp throughput: A simple model and its empirical validation, in: Proceedings of the ACM SIGCOMM’98 conference on Applications, technologies, architectures, and protocols for computer communication, 1998, pp. 303–314. [25] P. Bulychev, A. David, K. G. Larsen, M. Mikučionis, D. B. Poulsen, A. Legay, Z. Wang, Uppaal-smc: Statistical model checking for priced timed automata, arXiv preprint arXiv:1207.1272 (2012).