=Paper= {{Paper |id=Vol-2951/paper5 |storemode=property |title=Attack Trees with Time Constraints |pdfUrl=https://ceur-ws.org/Vol-2951/paper5.pdf |volume=Vol-2951 |authors=Aliyu Tanko Ali,Damas Gruska |dblpUrl=https://dblp.org/rec/conf/csp/AliG21 }} ==Attack Trees with Time Constraints== https://ceur-ws.org/Vol-2951/paper5.pdf 
Attack Trees with Time Constraints
Aliyu Tanko Ali, Damas Gruska
Comenius University, Mlynska Dolina 842 48, Bratislava, Slovak Republic


                                      Abstract
                                      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.

                                      Keywords
                                      Attack trees, timed attack trees, cyber-physical systems, security, threat modelling, timed automata,
                                      reachability




1. Introduction
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 [1, 2, 3] etc. In recent days, attack trees are used for security and
risk assessment of assets such as SCADA systems [4], IoT systems [5], CPS [6], and medical
equipment [7] etc. It is important to note that while attack trees remain a powerful graphical
security tool that can be used to identify how an asset may be compromised, the shift in the
dynamics of the assets i.e. from modelling and analysing single static systems to dealing with
complex and dynamic (sometimes run concurrently) raised some questions in the effectiveness
of using attack trees to analyse certain assets.
   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 [8], attack protection trees [9], sequential and parallel attack

29th International Workshop on Concurrency, Specification and Programming (CS&P’21)
" aliyu.ali@fmph.uniba.sk (A. T. Ali); gruska@fmph.uniba.sk (D. Gruska)
                                    Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
 CEUR
 Workshop
 Proceedings
               http://ceur-ws.org
               ISSN 1613-0073
                                    CEUR Workshop Proceedings (CEUR-WS.org)
trees [10], and attack countermeasure trees [11] etc. These proposed extensions introduced
how potential threats can be refuted. For example, if an attack tree models potential ways an
asset may be attacked (i.e. access to a secure sever room), the security engineer having good
knowledge of the assets surroundings, will design a security defence (hidden or open) to defend
the asset. These concepts are proven effective to assets that can be modelled with finite number
of nodes (states). The asset is modelled with an attack tree, and all possible attack paths are
blocked with defence or attack countermeasures. However, for a large and complex asset that
has infinitely many states, this concept is ineffective. Another important point is that; most
assets nowadays are safety-critical. They do require a timely response to threats. This means
apart from identifying possible ways an asset may be compromised, the model has to also
provide a means to slow down or prevent the attack. In previous papers [9, 12], we investigated
the concept of attack trees for stand-alone assets. In [9] we proposed the use of protection nodes
as an alternative to defence nodes. However, we realised that such a method is less effective to
CPS assets even with a small number of states. The challenge here is, CPS assets interact with a
wide range of objects (i.e. routing signs, cameras, buildings) and respond accordingly. Each of
these objects has its characteristics, and an attacker can manipulate these objects in different
ways (e.g. blur, blocked, add) to compromise the asset (e.g. DoS, message falsification attacks).
As such, a single pre-defined countermeasures or defence nodes is not enough to stop potential
attacks. In [12] we explored informally an idea to introduce time constraints in the set of parent
nodes in addition to the associated gates refinement. In this idea, we assume that even if the
threat environment of an asset changed, new vulnerabilities that emerged are connected to an
existing parent nodes. Although these vulnerabilities might not be refuted with the already
existing defence or protection nodes for other vulnerabilities, the time constraints defined on
the parent node will still be apply to the new vulnerabilities that connect to the parent node.
   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 [1], and attack graph [13]. Among them, attack
tree is a systematic attack scenario modelling method proposed by Schneier [1] and formally
defined by Mauw and Oostdijk [2]. Since attack tree is a static model (and considered a
semiformal model), several analysis frameworks have been proposed to establish its analysis
method based on formal methods. These analysis frameworks have been developed based on
timed automata [14], petri nets [15], and stochastic games [16] etc. The authors of [17] developed
a stochastic framework for quantitative analysis of ADTrees. The framework adopts ADTree
methodology to represent attack scenarios in a simple graphical representation and performs
quantitative assessment using CTMC analytical approach. The authors of [18] introduced a
multi-objective optimization framework for attack trees whereby the leaves of the attack trees
were enriched with various parameters such as cost, time, skills and resources. The framework
supports the computation of a wide range of security metrics such as attack values, attack paths,
and ranking. They translated each attack tree gate and leaf into a priced timed automata and
analyse the framework via UPPAAL CORE. In another effort, the work in [19] developed a
modelling framework for expressing the temporal behaviour of an attacker as a boolean formula,
and use a model checking tools to perform fully automated analyses of the modelled system
by performing both qualitative (boolean) and quantitative (probabilistic) analysis. The authors
demonstrated an example using UPPAAL tool, a network of timed automata that shows the
model of a thief who wants to enter a house while the resident is not at home. The work in
[20] defined the semantics for arbitrary attackers in an attack-defence tree using schematic
timed automata (STA), and implemented the model by translating it into UPPAAL SMC. The
authors modelled the encoding of an AD-Tree with one automaton modelling the defender, one
automaton modelling the attacker and a separate one modelling the environment of an outcome,
and coordinated their behaviour through synchronising channels. Other related works are
[21, 22, 11, 8].
   Unlike the works mentioned here, our work focus on traditional attack trees without consid-
ering defence nodes/actions. In our view, as mentioned earlier, defence actions are effective
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.
2. Attack trees formalism
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 [1]
but here we introduce a set of attacker’s actions 𝐴𝑐𝑑 (explain later) over the tree. (𝒬, β„°) is a
tree, where 𝒬 = {π‘ž0 } βˆͺ 𝒬𝑆 βˆͺ 𝒬𝐿 . {π‘ž0 } is the root node of the tree, it represents attackers
ultimate goal, 𝒬𝑆 is a set of internal nodes which we will refer to as sub-goal (also called parent
nodes), they represent the decomposition of the root node into smaller units that are easier to
solve, and 𝒬𝐿 is a set of leaf nodes (also called child nodes). The leaf nodes represent atomic
nodes or end nodes (vulnerability), indicating an attack step. These sets of nodes are connected
by a set of edges β„° βŠ† 𝒬 Γ— 𝒬. Each node in the attack tree (except for leaf nodes) has a gate
refinement. A gate indicates (the fashion) how a node can be achieved (compromised). The
interpretation of this fashion is on a node at a level above the current node. For this work, we
make use of the 𝐴𝑁 𝐷 and 𝑂𝑅 gates refinement. Informally, for a (parent) node with 𝐴𝑁 𝐷
gate, it is said to have a set of (child) nodes, that are linked to the parent node by a set of
edges and all these (child) nodes must be achieved first before the parent node is reached. For a
(parent) node with 𝑂𝑅 gate, a single node from the set of child nodes when achieved is enough
for the parent node to be reached. Formally we associate nodes with gates by the mapping
𝒒 : {π‘ž0 } βˆͺ 𝒬𝑆 β†’ {𝐴𝑁 𝐷, 𝑂𝑅}.
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)
Figure 1: Simple attack trees of how to steal a car that could be extended with time restriction


   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: 𝑑 = π‘Ÿ(𝑑) iff 𝑑′ 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
  π’œ π’œ          π’œ π’œ
  1 2 β€²
𝑠 β†’            𝑠 , i.e. attacks are asymmetry.
            2 1 β€²
     𝑠 ΜΈ= 𝑠 β†’

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 𝑠 β†’ 𝑠′ iff π’œ(access interior) = plier.
3. Motivation for enhanced restrictions
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 [10],
where the attacker is required to achieve the (child) nodes in sequential order. Failing to achieve
β€œall” the child nodes or β€œ accordingly”, will result in the attack process failing. Mechanisms like
this can be added (hidden) to components that will help prevent an attack. However, assets
such as CPS (i.e. interaction with objects from the physical environment which can be observed
by the attacker), this can be uncovered easily. The following scenario motivates the need for
extending attack trees (gates refinement) with time constraints.

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 manu-
      facturer for intelligent and autonomous vehicle studies,
    β€’ threat analysis: whereby, safety or/and varying ways a vehicle can be in danger is identi-
      fied 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 affected (sub-goals)
and the resultant effect/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 dam-
      ages.

  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.


4. Time constraints and security
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.

4.1. Enhanced restrictions and security
There are some relations between time constraint on the gates refinement and improved security
for different 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 different kinds of
attack scenarios for different kinds of assets.


5. Timed automata
As in [12], we now consider the use of a weighted timed automata to analyse our model.
A weighted timed automata (WTA) is an extension of timed automata [14] with cost/price
information on both locations and edges that can be used to solve several interesting problems.
There exists a formal verification tool UPPAAL [25] that accepts WTA as its modelling language.
Before we explain further, we first recall the definition of a timed automata. (henceforth, we
refer to a location of timed automata by 𝑙).

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 ℐ(𝑙).

5.1. Weighted time automata and attack trees translation
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
final/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 different 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 synchro-
nization 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
                            π‘Ž0 𝛼0     π‘Ž1 𝛼1
the states given as πœ‹ = 𝑙0 βˆ’β†’     𝑙1 βˆ’β†’     𝑙2 ... such that
                              𝑐0        𝑐1

    β€’ 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 Jπ’―π‘Ÿ K βŠ† WTA if
    β€’ Jπ‘ž0 K = WTA, a final location 𝑓 ∈ WTA is always satisfied,
    β€’ J𝒬K𝑂𝑅 = {WTA1 . . . WTA𝑛 }such that at least WTA𝑖 reached the
      final location 𝑓𝑖 ,
    β€’ J𝒬K𝐴𝑁 𝐷 = {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) trans-
lation 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 at-
tacker 𝐴 can only reach the root node of the tree {π‘ž0 } iff 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.

5.2. UPPAAL model
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 π‘₯




Figure 2: A simple UPPAAL model of nodes and time constraints


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) π‘šπ‘Žπ‘₯.


6. Discussion and future work
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.


Acknowledgement
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).


References
 [1] B. Schneier, Attack trees, Dr. Dobb’s journal 24 (1999) 21–29.
 [2] S. Mauw, M. Oostdijk, Foundations of attack trees, in: International Conference on
     Information Security and Cryptology, Springer, 2005, pp. 186–198.
 [3] B. Kordy, L. Piètre-Cambacédès, P. Schweitzer, Dag-based attack and defense modeling:
     Don’t miss the forest for the attack trees, Computer science review 13 (2014) 1–38.
 [4] C.-W. Ten, C.-C. Liu, G. Manimaran, Vulnerability assessment of cybersecurity for scada
     systems, IEEE Transactions on Power Systems 23 (2008) 1836–1846.
 [5] D. Beaulaton, N. B. Said, I. Cristescu, S. Sadou, Security analysis of iot systems using attack
     trees, in: International Workshop on Graphical Models for Security, Springer, 2019, pp.
     68–94.
 [6] F. Xie, T. Lu, X. Guo, J. Liu, Y. Peng, Y. Gao, Security analysis on cyber-physical system
     using attack tree, in: 2013 Ninth International Conference on Intelligent Information
     Hiding and Multimedia Signal Processing, IEEE, 2013, pp. 429–432.
 [7] M. A. Siddiqi, R. M. Seepers, M. Hamad, V. Prevelakis, C. Strydis, Attack-tree-based threat
     modeling of medical implants., in: PROOFS@ CHES, 2018, pp. 32–49.
 [8] A. Roy, D. S. Kim, K. S. Trivedi, Attack countermeasure trees (act): towards unifying the
     constructs of attack and defense trees, Security and Communication Networks 5 (2012)
     929–943.
 [9] A. T. Ali, D. P. Gruska, Attack protection tree., in: CS&P, 2019.
[10] F. Arnold, D. Guck, R. Kumar, M. Stoelinga, Sequential and parallel attack tree modelling,
     in: International Conference on Computer Safety, Reliability, and Security, Springer, 2014,
     pp. 291–299.
[11] X. Ji, H. Yu, G. Fan, W. Fu, Attack-defense trees based cyber security analysis for cpss,
     in: 2016 17th IEEE/ACIS International Conference on Software Engineering, Artificial
     Intelligence, Networking and Parallel/Distributed Computing (SNPD), IEEE, 2016, pp.
     693–698.
[12] A. T. Ali, Simplified timed attack trees, in: International Conference on Research Challenges
     in Information Science, Springer, 2021, pp. 653–660.
[13] X. Ou, A. Singhal, Attack graph techniques, in: Quantitative Security Risk Assessment of
     Enterprise Networks, Springer, 2012, pp. 5–8.
[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).