Lyes Bayou
email: lyes.bayou@telecom-bretagne.eu

Nora Cuppens-Boulahia

David Espes
email: david.espes@univ-brest.fr

Frédéric Cuppens
email: nora.cuppens@telecom-bretagne.eu

Towards a CDS-Based Intrusion

I. INTRODUCTION

For several years, an important trend in industrial process management, has been the increasing use of wireless communication in the so called Supervisory Control and Data Acquisition systems (SCADA). SCADA systems are computerbased technology used for monitoring and managing industrial installations such as power plants, refineries, railways, etc. This is mainly due to the low-cost and the great flexibility provided by WSN that enhance significantly the sensing capability of SCADA systems. Therefore, Wireless Industrial Sensor Networks (WISN) are proposed to provide reliable, robust and secured communication in order to meet industrial requirements such as availability and real-time.

As a specific application of WSN, Wireless Industrial Sensor Networks (WISN) present the followings key characteristics [START_REF] Moyne | The emergence of industrial control networks for manufacturing control, diagnostics, and safety data[END_REF] :

• They are expected to work reliably in industrial harsh environment: wide temperature range, vibrations, reflections due to metallic structures, etc. • There is an online trusted party (the base station).

• There is no data aggregation. All sensing data are sent to the base station.

• Used protocols must be energy efficient. The battery life of sensors is expected to last several years.

In terms of security, WISN are subject to the same attacks as WSN and other wireless networks. Indeed, attackers mainly use wireless communication as a medium to launch their attacks. Moreover, as WISN manage sensitive installations and facilities, attacks against them can lead to harmful economical consequences or even can threaten human lives [START_REF] Huang | Understanding the physical and economic consequences of attacks on control systems[END_REF]. Therefore, several mechanisms were developed to enhance the security of these networks (Cryptography, Authentication, etc). But as these security solutions cannot prevent all attacks, especially in the case of node compromise attacks [START_REF] Bayou | Security issue of wirelesshart based SCADA systems[END_REF], Intrusion Detection Systems (IDS) are used as a second line of defense [START_REF] Onat | An intrusion detection system for wireless sensor networks[END_REF].

Nevertheless, we cannot directly apply intrusion detection techniques used in other wireless networks such as ad hoc networks, to supervise Wireless sensor networks without their adaptation. Indeed, there are three features that distinguish WSN and more specifically WISN from other wireless networks [START_REF] Mitchell | A survey of intrusion detection in wireless network applications[END_REF]:

1) processor, memory, energy and channel are limited resources; 2) WISN are usually not mobile; 3) the behavior of a WISN is highly predictable since it is composed of devices with few human interventions. So, communication and exchanged data respond to specific profiles in terms of quantity and frequency.

Depending on where the intrusion detection logic is implemented, these systems can be divided in two categories [START_REF] Coppolino | An intrusion detection system for critical information infrastructures using wireless sensor network technologies[END_REF]: centralized and distributed systems. In centralized systems, an IDS agent connected to the WSN, mainly through the base station, analyzes information sent from wireless sensors in order to detect potential attacks. In decentralized systems, the detection logic is implemented directly into sensors called IDSagents. These IDS-agents monitor the behavior of adjacent sensors. Hybrid systems consist of a central agent connected to the main station and IDS-agents deployed among sensors. By this way, both local and end-to-end communications are analyzed.

An important issue in such architectures is the deployment of IDS-agents. Indeed, the detection efficiency depends greatly on the collected data quality. Therefore, the localization of devices used to collect data must be well studied otherwise a part of communication will not be monitored.

We must note that as in classical WSN, clustering techniques are widely used for providing routing features and data aggregation, IDS-agents are generally implemented in the cluster head [START_REF] Mitchell | A survey of intrusion detection in wireless network applications[END_REF]. Nevertheless, this placement method is not efficient especially in WISN. Indeed, with this method we do not have the guaranty that all communications are monitored as only communications between sensors and cluster heads are checked by IDS-agents.

In this paper, we present a deployment scheme for the placement of the IDS-agent of a decentralized IDS in a Wireless Industrial Sensor Network. It presents the best tradeoff between the number of used IDS-agents and the detection efficiency. We use the graph theory concept of Dominating Set to select nodes that will be substituted by super-nodes. Super-nodes have enhanced storage and processing capacities that allow them to act in the same way as normal sensors and also as detection agents. By this way, a virtual wireless backbone network providing intrusion detection capabilities will be created upon the WSN.

To validate the deployment scheme, communication in the context of WSN were modeled and then it was proven that this scheme fulfills the defined security requirements.

The rest of the paper is organized as follows. Section II presents some common attacks on WSN. In Section III, we discuss several intrusion detection techniques used in WSN. We show in Section IV how the deployment scheme have been ignored in almost all previous studies. Section V describes security requirements and the attacker model. Our deployment scheme is detailed in Section VI. A formal validation of this deployment is given in Section VII. The performances of the proposed scheme are presented in Section VIII. Finally, Section IX, presents the conclusion and future works.

II. WSN ATTACKS:

WSN can be subject to several kinds of attacks. These attacks can target important mechanisms such as [START_REF] Karlof | Secure routing in wireless sensor networks: attacks and countermeasures[END_REF]: routing protocol, data aggregation, voting, fair resource allocation, and misbehavior detection algorithms. We give below the description of some well-known attacks on WSN:

• Jamming attack: in this kind of attacks, a malicious node emits periodically or continuously on one or more channels. This will create interferences which will disturb transmissions of nearby nodes. • Denial of Service (DoS) attack: it can be executed by flooding a node. A malicious node sends a great amount of packets to a node. The targeted node will be overwhelmed and will not be able to receive legitimate packets. • Sinkhole and blackhole attacks: in this kind of attack a malicious node misleads routing algorithm by transmitting false information to the base station. As a result a part of the traffic will be redirected to the malicious node which can drop partially (wormhole) or totally (blackhole) packets. • Selective forwarding attacks: a malicious node chooses selectively to drop some packets and to not forward them to their final destination. • Wormhole attacks: in this kind of attacks a malicious node creates a virtual tunnel by capturing packets in one location and retransmits them in another location of the network. To do that, the malicious node must have a transmission range longer than other nodes or can require the help of another malicious node. As results, the malicious node can circumvent the routing protocol and lies on its location (number of hops from the base station). • Hello Flood attacks: These attacks target some routing protocols, specially those using a certain kind of packet hello packets, to discover their immediate neighborhood.

A malicious node with a large transmission range can flood a large part of the network with this kind of packets. Nodes receiving these packets, will assume that the malicious node is in their transmission range. As results, normal nodes can exhaust their battery life by trying to communicate with the malicious node. • Sybil attacks: Sybil attacks were first described by Douceur in [START_REF] Douceur | The sybil attack[END_REF]. He shows that in the absence of a central identification authority that checks correspondence between entity and identity, a malicious entity can present multiple identities. This kind of attack can be used to target several types of protocols in WSN such as distributed storage, routing, data aggregation, voting, fair resources allocation and misbehavior detection algorithms [START_REF] Newsome | The sybil attack in sensor networks: analysis & defenses[END_REF]. • Forced delay attacks: a sensor node deliberately delays packets forwarding which can disturb significantly the installation functioning. This kind of attacks can have harmful consequences in WISN where processes are time sensitive.

III. INTRUSION DETECTION TECHNIQUES FOR INDUSTRIAL WIRELESS SENSOR NETWORKS

Several techniques are used in IDS to detect attacks such as watchdogs or local monitoring [START_REF] Khalil | Liteworp: Detection and isolation of the wormhole attack in static multihop wireless networks[END_REF], spontaneous watchdogs [START_REF] Roman | Applying intrusion detection systems to wireless sensor networks[END_REF], edge self-monitoring [START_REF] Dong | Edge self-monitoring for wireless sensor networks[END_REF][13], etc. These techniques rely on the broadcast nature of wireless communication. Indeed, each node is able to overhear all packets sent by nodes in its neighborhood. Nevertheless, these techniques suffer from several drawbacks [START_REF] Abduvaliyev | On the vital areas of intrusion detection systems in wireless sensor networks[END_REF]. In local monitoring or watchdog, selected nodes are used for monitoring specific part of the wireless network. This technique requires that watchdog nodes overhear and store all exchanged packets in their neighborhood. Consequently, it is a very energy and computational resources consuming technique as watchdog nodes must be active continuously. In industrial process management, such technique is in practice not applicable since sensors have limited resources.

To reduce some of these drawbacks, spontaneous watchdog technique was proposed [START_REF] Roman | Applying intrusion detection systems to wireless sensor networks[END_REF]. In this technique, all nodes implement a local agent that monitors information relative to the sensor node itself. Also, a global agent is activated randomly and acts as a watchdog. Thus, as global agent is not active continuously in each node, the added overload is lower in comparison to the previous technique. However, this technique does not ensure that all packets are overheard by a global agent which reduce significantly the IDS efficiency.

In edge self-monitoring technique [START_REF] Dong | Edge self-monitoring for wireless sensor networks[END_REF], nodes are put in sleep or active mode in such a way that each transmission link is always monitored by k nodes (k-self monitoring). This technique ensures that all the traffic is monitored and node resources are not overused. The drawback is that monitoring nodes have partial information about monitored nodes. Indeed, the same node is not monitored each time by the same monitoring nodes. Consequently this technique is not efficient for intrusion detection.

IV. RELATED WORK

After studying many intrusion detection systems specially designed for wireless sensor networks [START_REF] Mitchell | A survey of intrusion detection in wireless network applications[END_REF], we can conclude that the detection logic deployment issue is rarely mentioned. Indeed, although these studies use selected sensors for implementing totally or partially an intrusion detection logic, there is no indication how these sensors are selected. In [START_REF] Da Silva | Decentralized intrusion detection in wireless sensor networks[END_REF], Da Sila et al. proposed one of the first intrusion detection systems for WSN. They designed a decentralized system in which a set of nodes is designated as monitor and is responsible of monitoring their neighbors looking for intruders. Nevertheless, it is not specified how these monitoring nodes are selected except that all nodes must be monitored.

In a more recent study, Roosta et al. proposed in [START_REF] Roosta | An intrusion detection system for wireless process control systems[END_REF] an intrusion detection system for wireless process control systems. The system consists of two components: a central IDS and multiple field IDS distributed among sensor nodes. These field IDS are deployed in super-nodes that passively monitor communications in their neighborhood. They periodically send collected data to the central IDS that will check their conformity with the security policy. Even if it is mentioned that the central IDS is implemented in the Network Manager (The base station in this kind of networks) there is no indication about the deployment of field IDS.

We also must note that in Wireless Sensor Networks, there are two others methods that are more or less similar to the IDS deployment which are Base Station deployment and Network Clustering.

In Base Station deployment studies, the aim is to find the optimal location of one or several base stations in order to ensure the radio coverage, reduce communication latency or increase the network lifetime [START_REF] Akkaya | Positioning of base stations in wireless sensor networks[END_REF]. The most important criteria here is the determination of the most suitable location for the base station that ensures reliable communications with nodes.

In the Network clustering studies, the aim is to organize the wireless network into a collection of small-size networks [START_REF] Abbasi | A survey on clustering algorithms for wireless sensor networks[END_REF]. This is mainly used in routing protocol or in transmission bandwidth optimization. In both cases only nodes designated as cluster heads implement the routing table or have the ability to aggregate received data which reduces the redundancy and the network load. Clusters are built in such a way all nodes are located at k-hops on maximum from the cluster head or by sitting equal-size clusters to perform load balancing [START_REF] Abbasi | A survey on clustering algorithms for wireless sensor networks[END_REF].

In IDS deployment issue, nodes selection criteria are different from those used in base station deployment or cluster heads selection. Indeed, IDS system must be deployed in such a way all exchanged packets are monitored and their conformity with the security policy is checked.

V. SECURITY REQUIREMENTS AND ATTACKER MODEL

Industrial systems rely on processing the sensing data gathered from several kinds of sensors deployed throughout the facility. Therefore, to ensure the industrial process continuity in safe condition, it is important that data sent by these sensors are effectively received by the main station and in the appropriate time. In other words, we must be able to check that the right information arrives to the right destination at the right time without any modification, alteration or delay.

Consequently, we must be able to check the following security requirements:

• the packet source (non repudiation).

• the packet integrity (non modification).

• the packet delivery.

• the packet delivery time.

In this study, we assume that the aim of the attacker is to disturb the industrial process. This can be done either by dropping packets, injecting false packets or modifying packets. The attacker can also delay transmission of some important packets (alarms, sensing data, etc) to hide its malicious activity. Therefore, we consider in our study a Dolev-Yao like attacker [START_REF] Dolev | On the security of public key protocols[END_REF] that can intercept, modify, forge or delay packets. For that it can only use its own credential (cryptographic keys) without any attack against used cryptographic mechanisms.

VI. THE PROPOSED CDS-BASED DEPLOYMENT SCHEME

In this Section, we present our CDS-Based deployment scheme for securing Wireless Industrial Sensors Networks. We use for that the Connected Dominating Set (CDS), a well known concept in the Graph Theory.

The aim of this study is to propose an efficient scheme to select sensor nodes in which intrusion detection logic will be implemented. Thus, on the basis of an existing sensor network topology, selected nodes are substituted by enhanced nodes called Super-Nodes. These super-nodes will act as classical sensor nodes by fulfilling sensing tasks and will also implement intrusion detection capabilities. As a result, a virtual wireless backbone that provides security purposes will be created upon the network.

To achieve this goal, our approach relies on WISN communication characteristics:

1) Local communication: used by adjacent nodes, that acts as relay nodes, to forward packets from the sender to their final destination. It is also used to exchange messages between adjacent nodes to maintain the network connectivity. 2) End-to-end communication: used to transmit sensing data or commands between nodes and the base station. Usually this kind of communication is encrypted. In order to be efficient, an IDS must collect all exchanged packets in both local and end-to-end communication. Consequently, a two-level architecture is the appropriate choice. It consists in a central agent and several IDS-agents. The central agent is responsible for monitoring end-to-end communications and global coordination. It is implemented in the base station. IDS-agents are responsible for monitoring local communications of sensor nodes inside their neighborhood. They are implemented in selected sensor nodes.

Also, to be more efficient, the deployment scheme must fulfill two requirements:

1) each IDS-agent must be able to monitor its neighborhood without any cooperation with other IDS-agents. This requirement aims to decrease the overload added by the IDS and thus avoid to disturb the industrial process by adding a great amount of packets. Also, it allows a better detection effectiveness since an IDS-agent can by itself detect the attack. 2) each IDS-agent must be adjacent to at least another IDSagent. This requirement aims to ensure that we have a secure communication channel between each IDS-agent and the central-IDS. Indeed, as IDS-agents are resilient nodes, we can always trust them for forwarding alarm packets especially in the case of nodes compromission. A final but not less important point, is that the deployment scheme must be able to fulfill above requirements with an acceptable IDS-agents number. Indeed, the implementation of the detection logic in enhanced sensors capabilities must be cost efficient by reducing the number of these sensors.

According to the above requirements, our deployment scheme, that we call CDS-based deployment scheme, includes the three following steps: (i) Connectivity Graph Construction: A preparatory step in which the wireless sensor network is modeled by a graph called Connectivity Graph. (ii) Connected Dominating Set Construction: In this step, the connected dominating set is computed for selecting nodes that will be substituted by IDS-agents. (iii) Uncovered Links Removal: A final step that selects additional nodes for enforcing the monitoring coverage of some links.

A. Connectivity Graph Construction

In this step we model the wireless sensor network as a graph G = (V, E), where V represents the set of all nodes in the network and E represents the set of all links in the network. Building the set V is straightforward as each node in the wireless networks is represented by a vertex. Modeling E is more sophisticated. Indeed, two nodes are linked if they can communicate which means that each node is in the transmission range of the other node.

Several models have been proposed to specify the transmission range. The most used model is the Unit disk graph (UDG). As illustrated in Fig. 1, two nodes are adjacent if and only if their Euclidean distance is at most 1 (or in general case less than a radius r). This model is idealistic as it assumes that the transmission range is uniform and omnidirectional and do not consider obstacles.

Other models try to be more realistic by considering waves propagation and path loss. Due to its simplicity and efficiency, the COST231 multi-wall model [START_REF]Digital mobile radio towards future generations systems[END_REF] is widely used in indoor environment [START_REF] Andrade | IEEE 802.11 WLANs: A comparison on indoor coverage models[END_REF]. In this model, the path loss in dB for environments with just one floor is given by L dB , where the integer k w represents the number of wall types, k wi and L wi represent respectively the number and the loss of the i th wall type and L 0,dB is the free space propagation to 1 meter.

L dB = L 0,dB + 20 log 10 d + kwi i=1 k wi L wi (1)
The reader can refer to [START_REF] Andrade | IEEE 802.11 WLANs: A comparison on indoor coverage models[END_REF] and [START_REF] Yu | Connected dominating sets in wireless ad hoc and sensor networks -A comprehensive survey[END_REF] to have more details about other models.

B. Connected Dominating Set (CDS)

In Graph Theory, a Dominating Set (DS) D of a graph G is a subset of nodes such that each node in G is adjacent to at least one node in D. A node in D is called a dominator node.

A Connected Dominating Set (CDS) is a dominating set in where each dominator node is adjacent to at least one other dominator.

In WSN, CDS have been used for creating a virtual backbone of the network (VBN). The VBN is mainly used as a spin for routing purposes [START_REF] Yu | Connected dominating sets in wireless ad hoc and sensor networks -A comprehensive survey[END_REF]. Only nodes in the dominating set have routing features. Other nodes must send their messages to their closest dominator. Then, messages will be routed to the final destination throughout the VBN. The CDS can also be used for [START_REF] Yu | Connected dominating sets in wireless ad hoc and sensor networks -A comprehensive survey[END_REF]:

• improving multicast/broadcast routing by restricting the forwarding of such messages to dominator nodes only, • managing power consumption by making more nodes in a sleep mode, • providing reliable and stable links. Finding the minimum (connected) dominated set (M(C)DS) i.e., a CDS with the smallest size, is a NP-hard problem [START_REF] Yu | Connected dominating sets in wireless ad hoc and sensor networks -A comprehensive survey[END_REF], [START_REF] Guha | Approximation algorithms for connected dominating sets[END_REF]. Therefore many algorithms for constructing an approximate M(C)DS have been proposed. These algorithms can be divided into two categories: centralized algorithms and decentralized algorithms. Centralized algorithms are used under the assumption that the complete network topology is known. In decentralized algorithms, the dominator nodes are selected after a message exchange process between nodes.

The proposed deployment scheme relies on a centralized algorithm. Firstly, because this deployment scheme will be performed off-line on a topology-known WISN and also because centralized algorithms in general yield to a smaller CDS with a better performance ratio than decentralized algorithms [START_REF] Yu | Connected dominating sets in wireless ad hoc and sensor networks -A comprehensive survey[END_REF]. Guha and Khuller propose in [START_REF] Guha | Approximation algorithms for connected dominating sets[END_REF], a greedy centralized algorithm to construct a Minimal CDS and prove that it performs in a polynomial time. This algorithm builds a spanning tree rooted at the node that has a maximum degree. Each time a node is selected as a dominator, its neighbors are marked. The marked node with the maximum degree is selected as a dominator for the next step. The tree grows until all nodes are added to it. The non-leaf nodes in the tree form a CDS.

We propose a modified algorithm based on the Guha and Khuller algorithm. Indeed, instead of starting by the node with the maximum degree, we use the node representing the base station as a tree root. The pseudo-code of the proposed algorithm is given in Alg. 1. Initially all nodes are white 5: Mark the node root as black;

Algorithm 1 CDS construction algorithm

Start from the base station 6: Mark root neighbors as gray nodes; 7: while Exist a white node do repeat until all nodes are marked 8:

Select n the gray node with the maximum degree;

C. Uncovered Links Removal

To detect efficiently some attacks such as selective forwarding, message injecting or dropping, the IDS-agent should overhear packets received by a node and also those transmitted by that node. By construction, the IDS-agent CDS-based deployment scheme ensures that each packet transmitted by any node in the wireless network is overheard by at least one IDS-agent.

But as illustrated in Fig. 2, this does not guarantee that all packets received by that node are always overheard by at least one of IDS-agents monitoring the node receiving the packet. Indeed, IDS-agent in A cannot check that K actually

A B C D K F Fig. 2.
Example of an uncovered link retransmits packets received from F and the same holds for IDS-agent B for packets received by F from K. Thus, after applying the CDS algorithm, we can have some uncovered links as the link K -F in Fig. 2 .

Uncovered links are links that fulfill the two following conditions:

1) no one of their vertices is an IDS-agent (a dominator).

2) and also their vertices are monitored by different IDSagents. For monitoring these links, we implement an algorithm for their detection as illustrated in Alg. 2. This algorithm starts by building the list of uncovered links. Then, it marks as dominator the node that is part of the maximum number of uncovered links. After updating the uncovered links list, it repeats previous actions until all uncovered links are monitored. Update L; 6: end while

VII. DEPLOYMENT SCHEME FORMAL VALIDATION :

To validate the proposed deployment scheme, we first define communication properties of wireless communication. Then, we specify both attacker capabilities and security requirements. Finally, we prove that the defined security requirements are completely fulfilled by the deployment scheme properties.

A. Notation :

Let us assume the following:

• V and D represent respectively, the set of nodes and the set of IDS-agents with D ⊂ V . • represents the propagation delay of a packet. • δ represents the maximal time a packet must be forwarded within.

• δ (with δ << δ ) represents the maximal time a packet is considered as deleted if it has not been forwarded. We must note that in the predicates sendP acket and receiveP acket the final destination of the packet m is the node n 4 and that the node n 2 is used as relay to forward this packet to its final destination.

B. Properties definitions:

• WISN properties:

1) Medium broadcast property: as regards to the broadcast nature of wireless medium, a packet m sent by a node n 1 is received by all its neighbors.

∀n, n 1 , n 2 , n 3 , n 4 ∈ V, sendP acket(n 1 , n 2 , n 3 , n 4 , m, t) ∧ neighbors(n 1 , n) ⇒ receiveP acket(n, n 1 , n 3 , n 4 , m, t + )
2) Channel symmetry property: If node n 1 is a neighbor of node n 2 , node n 2 is also a neighbor of node n 1 .

∀n 1 , n 2 ∈ V, neighbors(n 1 , n 2 ) ⇔ neighbors(n 2 , n 1 )
3) Multi-hop property: If node n 1 receives a unicast packet m originated from the node n, so either n 1 and n are neighbors, or there is a node n 2 neighbor of node n 1 that has forwarded this packet.

∀n 1 , n 2 , n, n ∈ V, m ∈ M, t ∈ T, receiveP acket(n 1 , n 2 , n, n , m, t) ⇒ (sendP acket(n 2 , n 1 , n, n , m, t -) ∧ neighbors(n 2 , n 1 ))
• Attacker properties: 1) Forging a fake packet: in this attack, a malicious node n 1 pretends retransmitting to n 3 a packet m received from the node n 2 .

∀n 1 , n 3 , n, n ∈ V, n 1 = n, m ∈ M, t ∈ T, f orgeP acket(n 1 , n 3 , n, n , m, t) ⇒ sendP acket(n 1 , n 3 , n, n , m, t) ∧¬(∃m ∈ M, ∃n 2 ∈ N, ∃t ∈ T, t < t, receiveP acket(n 1 , n 2 , n, n , m , t ) ∧equivalent(m, m ) ∧neighbors(n 1 , n 2 ) ∧ neighbors(n 1 , n 3 ))
2) Deleting a packet: in this attack, a malicious node n 1 does not forward to the next node n 2 a received packet m destined to the node n within the defined time δ .

∀n 1 , n 2 , n 3 , n, n ∈ V, n 1 = n , m ∈ M, t ∈ T, deleteP acket(n 1 , n 2 , n, n , m, t + δ) ⇒ receiveP acket(n 1 , n 3 , n, n , m, t) ∧¬(∃m ∈ M, ∃t ∈ T, t + < t < t + δ , sendP acket(n 1 , n 2 , n, n , m , t ) ∧equivalent(m
, m ) ∧ neighbors(n 1 , n 2 ))
3) Modifying a packet: in this attack, a malicious node n 1 forwards to the next node n 2 a packet m which is a modified version of a received packet m.

∀n 1 , n 2 , n 3 , n, n ∈ V, m ∈ M, t ∈ T, modif yP acket(n 1 , n 2 , n, n , m, t) ⇒ receiveP acket(n 1 , n 3 , n, n , m, t ) ∧(∃m ∈ M, ∃t ∈ T, receiveP acket(n 2 , n 1 , n, n , m , t)) ∧¬equivalent(m, m ) ∧ neighbors(n 1 , n 2 )
4) Delaying a packet: in this attack, a malicious node n 1 forwards to the next node n 2 the received packet m after the defined time δ.

∀n 1 , n 2 , n 3 , n, n ∈ V, m ∈ M, t ∈ T, delayP acket(n 1 , n 2 , n, n , m, t) ⇒ ∃m ∈ M, ∃t ∈ T, t + δ < t < t + δ , receiveP acket(n 1 , n 3 , n, n , m, t ) ∧sendP acket(n 1 , n 2 , n, n , m , t) ∧equivalent(m, m ) ∧ neighbors(n 2 , n 3 )
• WISN Security requirements:

1) Traffic monitoring property: In order to gather all exchanged traffic, the IDS system i.e., all IDS nodes, must receive all sent messages.

∀n 1 , n 2 , n, n ∈ V, ∀m ∈ M, ∀t ∈ T, ∃d ∈ D, sent(n 1 , n 2 , n, n , m, t) ⇒ receiveP acket(d, n 1 , n, n , m, t + ) ∧ neighbors(d, n 1 )
2) Forged packet Detection property: an IDS-agent d receives the packet m sent by n 1 to n 2 without receiving the equivalent packet m sent to n 1 by n 3 . C. Security requirements guarantee proof: Theorem 1: Deployment scheme properties guaranty WISN security requirements validation:

∀n 1 , n 2 , n 3 , n, n ∈ V, n 1 = n, ∀m ∈ M,
∀n 1 , n 2 , n 3 , n, n ∈ V, ∀m ∈ M, ∀t ∈ T neighbors(n 1 , n 2 ) ∧ neighbors(n 1 , n 3 ) ⇒ ∃d ∈ D, detectF orgeP acket(d, n 1 , n 2 , n, n , m, t) ∧detectDeleteP acket(d, n 1 , n 2 , n, n , m, t) ∧detectM odif yP acket(d, n 1 , n 2 , n, n , m, t) ∧detectDelayP acket(d, n 1 , n 2 , n, n , m, t)
Indeed, according to the Uncovered link monitoring property, if n 1 sends a packet m to its neighbor n 2 there is always an IDS-agent d, neighbors of n 1 and n 2 that receives the sent packet. Also, according to the medium broadcast property, the IDS-agent d receives all packets sent by n 2 and particularly the packet m i.e., the forwarded version of the packet m. Consequently, the IDS-agent d can always compare packets m and m and checks if ever a packet have been forged, deleted, modified or delayed.

VIII. PERFORMANCES EVALUATION:

A. Dominating Nodes Ratio:

For evaluating the proposed deployment scheme performances, we conduct series of test on simulated wireless sensor networks. For this purpose, we use NS3 to deploy randomly n nodes in a rectangular field. Then, we vary the radius r, representing the transmission range of nodes. By that way, we get networks with different topology density (TD) that is the average node degree.

The dominating node ratio indicates the number of dominating nodes in a WSN compared to the total number of its nodes. For assessing the impact of the topology density on this ratio, we generate for each graph size, 50 random graphs with different topology density. Then, we measure for each generated graph, the dominating node ratio. In order to get accurate results, we measure the dominating node ratio of several generated random graphs with the same size and topology density. Then, we take the average of these measures that we illustrate in Fig. 3.

As intuitively expected, the dominating node ratio decreases, for all graph sizes, with the increase of the topology density. This ratio is about 30% with a TD equal to 7-8 and reaches 20-25% with a TD above 10-12.

We should note, that according to the best practices in WISN deployment [START_REF]WirelessHART[END_REF], 25% of sensors should have a direct connection to the main station; each node should have at least 3 direct neighbors; and each node should not be 4 hops away from the main station.

Table I illustrates the dominating node ratio result for Alg. 1 and Alg. 2. We can see clearly that Alg. 2 does not add a great number of IDS-agents. Indeed, the maximum ratio of added IDS-agents is about 3.5 %. Thus, detecting and removing uncovered links strengthen the efficiency of the solution without increasing significantly the number of IDSagents.

B. Dominating nodes selection execution Time

As the CDS-Based deployment scheme is executed once and offline, it does not require a fast execution. Nevertheless, the average time taken by the execution of both Alg. 1 and Alg.2, illustrated in Fig. 4, shows that it takes very acceptable values. These performances are mainly due to the Alg. 1 that is executed in a polynomial time.

C. Traffic monitoring efficiency

Table II illustrates the number of nodes monitored by the same dominator node. We can see that the average number of nodes dominated by the same dominator node is always bigger than the Topology density, i.e., the average node degree. This is due to the Alg. 1 and Alg. 2 that choose dominator nodes with higher degrees. We can also see that a dominator node monitors at least 2 nodes which indicates that leaf nodes are never selected as dominating nodes.

In another hand, the maximum number of monitored nodes by the same dominator may seem higher particularly for networks with high density.

We must note in these cases that generally communication protocols for WISN use techniques such as Time Division Multiple Acces (TDMA) to manage transmission and avoid collisions. In these techniques, the bandwidth is divided into several channels (Typically 15 or 16) and only one transmission is allowed in the same channel at the same time. Consequently, the maximum number of communication that a dominator node has to monitor is equal to the number of transmission channels (15 or 16).

In Table III, we report the number of dominator nodes that monitors the same node. As expected, all nodes are at least monitored by one dominator. We can also see that on average, a node can be monitored by 2, 3 or more dominator nodes. Thus, this increases the detection efficiency as a node is monitored by several dominator nodes.

IX. CONCLUSION AND FUTURE WORKS

In this paper, we present an efficient IDS-agent deployment scheme for wireless sensor networks. This deployment scheme can be used either in decentralized, clustered or hierarchical architectures. It creates a virtual backbone that adds security purposes to an existing sensor network. To the best of our knowledge, it is the only complete deployment scheme implemented for security purposes. It presents good results both in terms of selected IDS-agent and execution time.

We must also note that the proposed deployment scheme fulfills totally WISN requirements especially in terms of communication specifications. This work can be improved by different ways. For example, as several nodes are monitored by a great number of dominators, we can try to eliminate redundant dominators. Also, we can adapt the deployment scheme to be used in heterogeneous networks in which devices do not have the same capabilities in terms of transmission range, storage and computational resources. In this case, we can use weighted graphs to select nodes with higher capabilities firstly.

Fig. 1 .

 1 Fig. 1. Connectivity graph construction

9 :

 9 Mark n as black; 10: Mark node n neighbors as gray nodes; 11: end while

Algorithm 2

 2 Uncovered links detection and monitoring algorithm 1: Build L the list of uncovered links; 2: while L is not empty do repeat until all uncovered links are monitored 3:Select n the node part of the maximum number of uncovered links;

Fig. 3 .Fig. 4 .

 34 Fig. 3. Dominating nodes ratio compared to the Topology Density

  • M represents the set of all exchanged packets. • sendP acket(n 1 , n 2 , n 3 , n 4 , m, t) means that node n 1 sends to node n 2 the packet m originated from the node n 3 and destined to n 4 at time t. • receiveP acket(n 1 , n 2 , n 3 , n 4 , m, t) means that the node n 1 receives from the node n 2 the packet m originated from the node n 3 and destined to the node n 4 at the time t. • neighbors(n 1 , n 2 ) means that the node n 1 is the neighbor of the node n 2 . • equivalent(m, m ) means that packet m is the forwarded version of the packet m and only fields in the header have been changed according to the used communication protocol.

  Deleted packet Detection property: an IDS-agent d receives the packet m sent by n 3 to n 1 but does not receive the equivalent packet m forwarded by n 1 to n 2 within the defined time δ . ∀n 1 , n 2 , n 3 , n, n ∈ V, n 1 = n , ∀m ∈ M, Modified packet Detection property: an IDS-agent d detects that the packet m sent by n 3 to the node n 1 and the packet m forwarded by n 1 to n 2 are not equivalent.∀n 1 , n 2 , n 3 , n, n ∈ N, ∀m ∈ M, ∀t, t ∈ T, , n 3 ) ∧ neighbors(n 1 , n 2 )5) Delayed packet Detection property: an IDS-agent dthat receives the packet m sent from the node n 3 to the node n 1 , also receives the packets m that n 1 forwarded to the next node n 2 after the defined time δ.∀n 1 , n 2 , n 3 , n, n ∈ V, ∀m ∈ M,

	∀t ∈ T, ∃d ∈ D, detectF orgedP acket(d, n 1 , n 2 , n, n , m, t) ⇒ ¬(∃m ∈ M, ∃t ∈ T, t < t, receiveP acket(d, n 3 , n, n , m , t ) ∧receiveP acket(d, n 1 , n, n , m, t) ∧equivalent(m, m ) ∧neighbors(d, n 1 ) ∧ neighbors(d, n 3 )) 3) ∀t, t ∈ T, t < t < t + δ , ∃d ∈ D, detectDeleteP acket(d, n 1 , n 2 , n, n , m, t + δ ) ⇒ ∃m ∈ M, receiveP acket(d, n 3 , n, n , m , t) ∧¬receiveP acket(d, n 1 , n, n , m, t ) ∧equivalent(m, m ) ∧ neighbors(n 1 , n 3 ) 4) ∃d ∈ D, detectM odif yP acket(d, n 1 , n 2 , n, n , m, t) ∃m ∈ M, ⇒ receiveP acket(d, n 3 , n, n , m, t) ∧ receiveP acket(d, n 1 , n, n , m , t ) ∧¬equivalent(m, m ) ∧neighbors(n 1 ∀t ∈ T, ∃d ∈ D, detectDelayP acket(d, n 1 , n 2 , n, n , m, t ) ⇒ ∃m ∈ M, ∃t ∈ T, t + δ < t < t + δ , receiveP acket(d, n 3 , n, n , m, t) ∧receiveP acket(d, n 1 , n, n , m , t ) ∧equivalent(m, m ) • IDS Deployment properties: 1) CDS property: a node is either an IDS or has at least one IDS as a neighbor. ∀n ∈ V, ∃d ∈ D, neighbors(n, d) As each node has at least an IDS as a neighbor (CDS property) and each packet sent by a node is received by all its neighbors (the medium broadcast property), each sent packet is received by at least one IDS. ∀n 1 , n 2 , n ∈ V, ∀m ∈ M, ∀t ∈ T, ∃d ∈ D, sendP acket(n 1 , n 2 , n 3 , n, m, t) ⇒ receiveP acket(d, n 1 , n 3 , n, m, t + ) ∧ neighbors(n 1 , d) 2) Uncovered link monitoring property: this property guarantee that there is always and IDS-agent d neighbor of two neighbor nodes n 1 and n 2 . ∀n 1 , n 2 ∈ V, ∃d ∈ D, neighbors(n 1 , n 2 ) ⇒ neighbors(d, n 1 ) ∧ neighbors(d, n 2 )

TABLE I DOMINATING

 I NODE RATIO BY ALGORITHM.

	n	Result	Alg.1 Ratio (%)	Result	Alg.2 Ratio (%)	Total Ratio (%)
	50	24.23	48.46	0.15	0.30	48.76
	100	42.38	42.38	1.15	1.15	43.53
	200	72.15	35.92	4.69	2.23	38.15
	300	102.33	33.75	9.08	3.00	36.75
	400	109.07	27.00	13.43	3.57	30.57
	500	133.69	26.46	16.84	3.30	29.76
	600	149.76	24.46	21.39	3.69	28.15
	800	166.78	20.42	27.29	3.50	23.92

TABLE II NUMBER

 II OF MONITORED NODES BY A DOMINATOR.

	n	T D	Number of dominated nodes Min Max Avg
	50	2.09	2.01	11.63	4.80
	100	3.69	2.20	20.76	6.74
	200	7.07	2.83	38.67	10.80
	300	6.81	2.41	43.94	9.90
	400	7.10	2.32	49.78	9.86
	500	8.50	2.48	60.08	11.79
	600	8.11	2.20	64.13	10.90
	800	8.87	2.17	75.65	11.49

TABLE III NUMBER

 III OF DOMINATORS MONITORING A NODE.

	n	T D	Number of dominated nodes Min Max Avg
	50	2.09	1	4.81	2.12
	100	3.69	1	5.56	2.42
	200	7.07	1	6.30	2.82
	300	6.81	1	6.63	2.80
	400	7.10	1	7.12	2.90
	500	8.50	1	7.20	3.05
	600	8.11	1	7.24	2.99
	800	8.87	1	7.50	3.06


Olga Gadyatskaya

René Rydhof Hansen

Kim Guldstrand Larsen

Axel Legay

Mads Chr Olesen

Danny Bøgsted Poulsen

Modelling Attack-Defense Trees using Timed Automata

. In this work we use the attack-defense tree as a goal an attacker wants to achieve, and separate the behaviour of the attacker and defender from the attack-defense-tree. We give a fully stochastic timed semantics for the behaviour of the attacker by introducing attacker profiles that choose actions probabilistically and execute these according to a probability density. Lastly, the stochastic semantics provides success probabilitites for individual actions. Furthermore, we show how to introduce costs of attacker actions. Finally, we show how to automatically encode it all with a network of timed automata, an encoding that enables us to apply state-of-the-art model checking tools and techniques to perform fully automated quantitative and qualitative analyses of the modelled system.

Introduction

In the past few years, we have witnessed a rapid increase in the number and severity of security breaches, ranging from theft of personal information about millions of US government employees 1 to sophisticated targeted malware attacks on security vendors 2 . This problem is exacerbated by the fact that it has become difficult to perform an adequate risk assessment of an organisation's security stance, with many organisations relying on a complex mix of off-site third party IT-services, e.g., "cloud services" and internally supported IT services. One of the tools available to help structure risk assessments and security analyses is attack trees, recommended, e.g., by NATO Research and Technology Organisation (RTO) [START_REF]Improving Common Security Risk Analysis[END_REF] and OWASP [START_REF] Owasp | CISO AppSec Guide: Criteria for managing application security risks[END_REF]. Attack trees [START_REF] Mauw | Foundations of attack trees[END_REF][START_REF] Salter | Toward a secure system engineering methodology[END_REF][START_REF] Schneier | Attack trees: Modeling security threats[END_REF] is a tree based formalism inspired by fault trees, a well-known formalism used in safety engineering. The formalism was initially introduced by Schneier [START_REF] Schneier | Attack trees: Modeling security threats[END_REF] and given a formal definition by Mauw and Oostdijk [START_REF] Mauw | Foundations of attack trees[END_REF]. Kordy et al. [START_REF] Kordy | DAG-Based Attack and Defense Modeling: Don't Miss the Forest for the Attack Trees[END_REF] provide a survey on attack trees and related formalisms. While basic quantitative analysis, i.e., a bottom-up computation for a single parameter (e.g., cost, probability or time of an attack), can be performed directly on attack trees [START_REF] Bagnato | Attribute decoration of attack-defense trees[END_REF], several proposals exist to extend the basic attack tree formalism in order to support better analysis. For example, Buldas et al. [START_REF] Buldas | Rational choice of security measures via multi-parameter attack trees[END_REF], Jürgenson and Willemson [START_REF] Jürgenson | Computing exact outcomes of multiparameter attack trees[END_REF] introduced multi-parameter attack trees with interdependent variables; Dalton et al. [START_REF] Dalton | Analyzing attack trees using generalized stochastic petri nets[END_REF] have proposed analysing attack trees as Generalized Stochastic Petri Nets; Arnold et al. [START_REF] Arnold | Sequential and parallel attack tree modelling[END_REF] applied interactive Input/Output Markov Chains to enhance temporal and stochastic dependencies analysis in attack trees. Kumar et al. [START_REF] Kumar | Quantitative Attack Tree Analysis via Priced Timed Automata[END_REF] have considered priced timed automata for analysis of attack trees. This work defines a translation for each leaf node and each gate in an attack tree into a priced timed automaton. The approach allows to translate the full attack tree into an automaton that can be analysed using the uppaal Cora model checker. The research community interest in attack trees has been recently reinvigorated by new techniques to automatically generate attack trees and attack-defense trees from socio-technical organizational models [START_REF] Gadyatskaya | How to generate security cameras: Towards defence generation for socio-technical systems[END_REF][START_REF] Ivanova | Transforming graphical system models to graphical attack models[END_REF], paving the way towards automating risk assessment.

Attack-defense trees are a notable extension of attack trees that include, besides attacker's actions, also defender's actions and model their interplay [START_REF] Aslanyan | Pareto Efficient Solutions of Attack-Defence Trees[END_REF][START_REF] Kordy | Attack-Defense Trees[END_REF]. This extended formalism allows capturing more detailed scenarios, and incorporating the defender's perspective into an analysis. For example, burglarresistance classes for physical security mechanisms, such as doors and windows, define how much time an attacker equipped with certain tools needs to spend on the intrusion [START_REF] Sitec | Burglar resistance[END_REF]. Explicit consideration of defenses in the analysis allows the domain experts to get a better picture of the scenario [START_REF] Bagnato | Attribute decoration of attack-defense trees[END_REF][START_REF] Kordy | Attack-Defense Trees[END_REF]. Recently, Hermanns et al. [START_REF] Hermanns | The value of attackdefence diagrams[END_REF] have created the attack-defense-diagrams formalism extending attackedefense trees with trigger and reset gates, which allow expressing temporal behaviours. The work [START_REF] Nielson | Quantitative verification and synthesis of attack-defense scenarios[END_REF] likewise introduces a sequential gate to attack-defense trees and considers a two-player stochastic game interpretation of this.

Our paper introduces a framework for analysing complex temporal scenarios of interactions of attackers and defenders, beyond the expressiveness of classic attackdefense trees. For doing this we develop a modelling framework for expressing the temporal behaviour of the attacker with the formalism networks of timed automata. Unlike the work of [START_REF] Kumar | Quantitative Attack Tree Analysis via Priced Timed Automata[END_REF] the attack-defense-tree is not encoded as a timed automata -instead it is encoded as a boolean formula, which the attacker wishes to become true. This encoding allows us to apply state-of-the-art model checking tools and techniques to perform fully automated analyses of the modelled system, both qualitative (boolean) analysis and quantitative (probabilistic) analysis. The modelling framework is accompanied by an automatic translation script. The script reads an attack-defense-tree and outputs a uppaal [START_REF] Larsen | UPPAAL in a nutshell[END_REF] timed automata model which can subsequently be queried several questions: among these questions are "what is the probability that an attack succeeds within τ " and "what is the expected cost of the attacker within τ time units" for a specific behaviour of the attacker. Using Uppaal-Stratego [START_REF] David | Uppaal stratego[END_REF], a recent extension of uppaal, we are furthermore capable of finding an attacker that minimises the expected cost of an attack.

Attack Defense Trees

We will now define an attack-defense tree (Definition 1), along with the standard boolean semantics for such a tree. Thereafter a temporal semantics with time, cost and stochasticity is introduced. This temporal semantics is the first contribution of this paper.

Definition 1 (AD-tree). An AD-tree over the attacker actions A a and defender actions A d is generated by the syntax

t :== p | t ∧ t | t ∨ t |∼ t where p ∈ A a ∪ A d . We denote by L(A a , A d ) all AD-trees over A a and A d . Let t ∈ L(A a , A d ), let A ⊆ A a
be the set of selected attacker actins and let D ⊆ A d be the set of selected defender actions; then we inductively define t A, D as

-p D, A = tt if p ∈ A ∪ D, ff otherwise -t 1 ∧ t 2 D, A = ( t 1 D, A) ∧ ( t 2 D, A) -t 1 ∨ t 2 D, A = ( t 1 D, A) ∨ ( t 2 D, A) -∼ t D, A = ¬( t D, A)
As an example of an attack-defense-tree consider Fig. 1. This tree explains how an attacker may succefully remove an RFID-tag from a warehouse. Among the possible ways is infiltrating management and order a replacement tag. The example is lifted from [START_REF] Aslanyan | Pareto Efficient Solutions of Attack-Defence Trees[END_REF].

To make attack-defense-trees well-formed, we follow Aslanyan and Nielson [START_REF] Aslanyan | Pareto Efficient Solutions of Attack-Defence Trees[END_REF] and impose a type system on top of the abstract syntax of Definition 1 -in this system there are two types d and a corresponding to defender and attacker. The type system is captured in Fig. 2. The negation operator ∼ acts like the switch operator of Aslanyan and Nielson [START_REF] Aslanyan | Pareto Efficient Solutions of Attack-Defence Trees[END_REF] and changes the type of the subtree. Unlike Aslanyan and Nielson, we do not have a normal negation operator: the reason is we only want an attacker (or defender for that matter) to do positive things i.e. the attacker should only do something beneficial for him. In the remainder we only consider well-formed trees according to this type-system and we restrict our attention to trees t where t a. The major interest of attack-defense trees is whether there exists a set of defense measures such that an attack can never occur.

Fig. 1: An example of an attack-defense-tree. Square items correspond to defender's actions and circles to the attacker. Question 1. For an attack-defense tree t ∈ L(A a , A d ), does there exist D ⊆ A d , such that for all A ⊆ A a , t D, A = ff? This encapsulates our view that defense measures are selected ahead of time and fixed, while the attacker selects a set of attack measures. Our view is in accordance with the classical definition of attack-defense trees by [START_REF] Kordy | Attack-Defense Trees[END_REF]. Let λ be a symbol not in A a , which indicates that an attacker chooses to do no actions. We denote by A λ a the set A a ∪ {λ}.

Definition 2. Let t ∈ L(A a , A d ) be an AD-tree. The Attack-Defense-Graph over t is the tuple G t = (V, v 0 , →, → ¬ , , F ) where

A d , Aa p : a , p ∈ Aa A d , Aa p : d , p ∈ A d A d , Aa t1 : r A d , Aa t2 : r A d , Aa t1 ∧ t2 : r A d , Aa t1 : r A d , Aa t2 : r A d , Aa t1 ∨ t2 : r A d , Aa t1 : r A d , Aa ∼ t1 : r -1 , r -1 = a if r = d d if r = a
Fig. 2: Type system to make attack-defense trees well-formed

-V = 2 A d × 2
Aa is a set of vertices containing currently true attacker and defender actions,

-v 0 = (∅, ∅) is the initial vertex, -→⊆ (V × A λ a × V) is a set of edges where ((D, A), a, (D , A )) ∈→ if and only if D = D , A = A ∪ ({a} ∩ A a ) and a / ∈ A, -→ ¬ ⊆ (V × A a × V) is a set of edges where ((D, A), a, (D, A)) ∈→ ¬ if and only if a / ∈ A - = {(v 0 , D, S) | D ∈ 2 A d ∧ S = (D, ∅)} is the "select defense" edges and -F = {(D, A) ∈ V | t D, A = tt} is a set of final vertices.
An attack-defense graph is essentially laying out all the possible steps an attacker may take to achieve a successful attack. Notice the edges in → ¬ correspond to trying to execute an atomic attack and failing. We allow this loop back as in this way we are able to model an attacker who selects what action to perform and an environment deciding whether that action succeeds.

For an attack-defense graph (ADG)

G t = (V, v 0 , →, → ¬ , , F ) we write v D v whenever (v, D, v ) ∈ and similarly we write v a -→ v (v ¬a --→ v ) if (v, a, v ) ∈→ ((v, a, v ) ∈→ ¬ ). An attack-defense scenario (ADS) for G t is a sequence ω = v 0 Dv 1 α 1 v 2 α 2 . . . α n1 s n . . . , where v 0 = v 0 , for all i, α i ∈ {a, ¬a | a ∈ A a } ∪ {λ}, v 0 D v 1 and for all j > 0, v j αj -→ v j+1 .
We call ω a successful ADS if there exists j such that v j ∈ F , denoted ω t, and we call it a failed ADS if for all j, v j / ∈ F , denoted ω t. We denote by Ω(t) all ADSs over t and

furthermore let Ω D (t) = {π = v 0 D v 0 a1 -→ • • • | π ∈ Ω(t)
} be all the ADSs initiated by the defender selecting defense measure D.

Lemma 1. Let t ∈ L(A a , A d ) be an attack-defense-tree and let D ⊆ A d . If for all ω ∈ Ω D (t), ω t then for all A ⊆ A a t D, A = ff. Lemma 2. Let t ∈ L(A a , A d ) be an attack-defense-tree and let D ⊆ A d . If there exists ω ∈ Ω D (t), ω t then there exists A ⊆ A a such that t D, A = tt.

In reality we wish to analyse the possible attacks after the defender has selected some defense measures. For this we remove the choice of defense measures from the ADG to get an attack graph (AG). Let

G t = (V, v 0 , →, → ¬ , , F ) be the ADG for t ∈ L(A a , A d ); then the AG responding to D ⊆ A d is the graph (V, v A , →, → ¬ , F ) where v 0 D v A . We denote this AG by G t D .
Due to Lemma 1 and Lemma 2 then question 1 is answerable by a pure reachability check on G t D for all D ⊆ 2 A d .

Adding Timed Behaviour

Intuitively speaking, an attacker observes the state of an ADG and choose an action. The attacker is memoryless and does, for instance, not remember how many times a specific attack has been attempted. The execution time of an action p a is given by interval [L pa , U pa ], and thus an abstract timed attacker (Definition 3) is essentially a timed transition system. Definition 3 (Abstract Timed Attacker). Let t ∈ L(A a , A d ). An abstract timed attacker over the ADG G t = (V, v 0 , →, → ¬ , , F ) is a tuple (S, M , Ac) where -S is a set of states, -M : V → S maps vertices to attacker states, and -Ac : S → 2 A λ a ×R ≥0 gives the possible actions and delays for an attacker, with the requirements that

• if s = M (v) and (p a , r) ∈ Ac(s) then v pa -→ v for some v , • if (p a , t) ∈ Ac(s) then L pa ≤ t ≤ U pa and {(p a , t )|L pa ≤ t ≤ U pa } ⊆ Ac(s), • if (λ, t) ∈ Ac(s) then Ac(s) = {(λ, t ) | t ∈ R ≥0 }, • if s = M (v), v = D, A, then (λ, 0) ∈ Ac(s) if and only if v ∈ F or A = A a and • for all s ∈ s, Ac(s) = ∅ Let G t = (V, v 0 , → a , → ¬ ,
, F ) be an ADG and let A = (S, M , Ac) be an abstract timed attacker for G t . For D ⊆ A d , we denote by G t D |A the transition system with state space V × S, initial state (v A , M (v A )) and transition relation defined by the rules

-(v, s) pa,t --→ (v , M (v )) if (p a , t) ∈ Ac(s) and v pa -→ v -(v, s) ¬pa,t ---→ (v , M (v )) if (p a , t) ∈ Ac(s) and v ¬pa --→ v -(v, s) λ,t --→ (v , M (v )) if (λ, t) ∈ Ac(s) and v λ -→ v . A timed attack over G t D |A, t ∈ L(A a , A d ) is a sequence v 0 d 0 α 0 , v 1 d 1 α 1 . . . , where v 0 = v A , for all i, d i ∈ R ≥0 , α i ∈ {p a , ¬p a | p a ∈ A a } ∪ {λ}
and there exists a sequence of states and transitions (v 0 , M (v 0 ))

α0,d0 ---→ (v 1 , s 1 ) . . . . We denote by Ω τ (G t D |A) all timed attacks of G t D |A. Let ω = v 0 d 0 α 0 , v 1 d 1 α 1 .
. . be a timed attack, then we write ω τ t if there exists i, s.t. t v = tt and i-1

i=0 d i ≤ τ .
Having introduced time, a defender may consider to not guarantee that an attack can never occur, but to make it very difficult time-wise i.e. that any succeeding attack will require more than τ time units -captured by question 2. Obviously, an attacker wishes to find an attack in response to D ⊆ A d that succeeds before τ time units i.e. to answer question 3.

Question 2. For an attack-defense tree t ∈ L(A a , A d ), abstract timed attacker A and time limit τ , does there exist a D ⊆ A d , such that for all ω ∈ Ω τ (G t D |A), ω τ t? Question 3. For an attack-defense tree t ∈ L(A a , A d ), abstract timed attacker A, time limit τ and D ⊆ A d does there exist ω ∈ Ω τ (G t D |A), such that ω τ t?

Adding Stochasticity

A stochastic attacker is a tuple A S = (A, γ, {δ pa |p a ∈ A λ a }), where A is an attacker defining allowed behaviour by the stochastic attacker, γ : S → A λ a → R ≥0 assigns a probability mass to attacker's actions and for all p a ∈ A λ a ,δ pa : S → R ≥0 → R ≥0 assigns a density to the execution time of p a . A few requirements are in order here:

1.

a∈A λ a γ(s)(a) = 1, 2. R ≥0 δ a (s)(t) dt = 1 for all a ∈ A λ a , 3. γ(s)(a) • δ a (s)(t) = 0 implies (a, t) ∈ Ac(s).
Requirement 1 states that γ(s) must be a probability mass function, 2 requires that δ a (s) is a probability density, and finally the most interesting rule 3 requires that whenever a probability density is assigned to a pair (a, t) then the attacker must in fact be able to do those according to the timed semantics. Finally, to make a complete stochastic semantics we need to resolve the non-determinism of selecting an outcome of performing an action p a . We assume there is a static probability of an action succeeding, and thus we assume a probability mass function γ Succ : A a → {p a , ¬p a } →]0, 1[ that assigns success and failure probabilities to actions with the requirement that any action must have a non-zero probability of succeeding.

Forming the core of a σ-algebra over timed attacks of G t D |A S , consider the finite sequence π = v 0 I 0 α 0 v 1 I 1 α 1 . . . v n , where for all i; α i ∈ {p a , ¬p a | p a ∈ A a }, I i is an interval with rational end-points and v i ∈ V. The set of runs (cylinder) of this sequence is

C G t D |A S (π) = {v 0 d 0 α 0 , v 1 d 1 α 1 . . . v n d n α n • • • ∈ Ω τ (G t D |A) | ∀i < d i ∈ I i }.
The probability of these timed attacks runs from (v, s) are recursively defined by

F (v,s) (π) = (v 0 = v) • γ(s)(c(α)) • R ≥0 δ c(α) (s)(t) dt • γ Succ (α)F [(v,s)] α,t (π 1 ), where π 1 = v 1 d 1 α 1 . . . v n d n α n , c(p a ) = c(¬p a ) = p a and (v, s) α,t --→ [(v, s)] α,t and base case F (v,s) ( ) = 1.
Remark 1. The stochastic semantics above is given for arbitrary time distributions. For the remainder we will however restrict our attention to stochastic attacker using only uniform distributions.

Let G t D = (V, v A , → a , → ¬ , F ) be an AG and let A S = ((S, M , Ac), γ, {, δ pa |p a ∈ A λ a }) then we let F G t D |A S (π) = F (v A ,M (v A ) (π).
With the above in place, the probability of a succesful attack within a time-bound τ is

P G t D |A S (♦ ≤τ t) = ω∈Ω τ (G t D |A S ) 0 if ω τ t 1 if ω τ t dF G t D |A S .
Question 4. Given an attack-defense tree t ∈ L(A a , A d ), stochastic attacker A S and time limit τ ; find

D * = arg min D∈2 A d P G t D |A S (♦ τ t)
Notice that question 4 has the time bound requirement for how quickly an attacker must succeed in an attack. If this time bound was not present and we thus gave an attacker unlimited time, then if a successful attack exists (no matter how unlikely) it would eventually succeed. This is evidenced by the plot in Fig. 3 with the time limit on the x-axis and the probabilities of an attack on the y-axis.

The dashed line in the figure is the lower bound of the 99% confidence level and the solid line is the upper bound.

Adding Cost

Fig. 3: Plot of probabilities of a successful attack for a uniform attacker.

Considering that an attacker is not only constrained by time, but also by his available resources e.g. money, we want to reflect the concept of a resource in our modelling. For this purpose we consider that an attacker only has one resource and that each action has an associated cost per attempted execution. We capture this cost by a function C : A λ a → R ≥0 that assigns the cost to actions with the requirement that C(λ) = 0.

Let ω = v 0 d 0 α 0 . . . be a timed attack; then we define the cost of ω up till step j as C(ω, j) = j-1 i=0 C(c(α i )), where c(λ) = λ and c(p a ) = c(¬p a ) = p a , i.e., we just sum up the individual costs along the attack before the j th step. Now we can define the expected cost of a stochastic attacker, A S , responding to a set of defense measures D with a time limit τ

E G t D |A S (C : ♦ ≤τ t) = ω∈Ω τ (G t D |A S ) C(π, j) if ω τ t ∧ j = max{i | i k=0 d k ≤ τ } C(π, j) if ω τ t ∧ j = min{i | t v i = tt} dF G t D |A S .
Question 5. Given an attack-defense tree t ∈ L(A a , A d ), stochastic attacker A S , time limit τ and

D ⊂ A d , find E G t D |A S (C : ♦ ≤τ t).
Consider that we fix the distribution over execution times and the success probabilities of execution attacks, but let γ range freely among all possible probability mass functions. Thus, we have a range of possible stochastic attackers, parameterised by γ, i.e. a range of attackers A S 1 , A S 2 . . . , where

A S i = (A, γ i , {δ pa |p a ∈ A λ a }).
Then we are interested in finding the attacker that minimises the cost. Question 6. Given an attack-defense tree t ∈ L(A a , A d ) time limit τ , D ⊂ A d and a collection of attackers A S 1 , A S 2 . . . parameterised by γ; find a stochastic attacker, A S , minimising E G t D |A S (C : ♦ ≤τ t).

In this paper we use the expressive network of timed automata (TA) formalism [START_REF] Alur | Automata for modeling real-time systems[END_REF] extensively. An efficient model checking technique exists for this formalism, and the tool uppaal [START_REF] Behrmann | A tutorial on Uppaal[END_REF][START_REF] Larsen | UPPAAL in a nutshell[END_REF] uses an extended version as its modelling language. As an example consider the three automata in Fig. 4, modelling two persons and a door. One of the persons is a Resident of a house and the other is a Thief who wants to enter the house while the Resident is not home. The Resident is initially at Home with the door locked for 14 hours -indicated by the expression x <= 14 . The expression x <= 14 is an invariant expression and is something that should always be true whenever the automata is in the given location. From Home the resident may unlock! the door and go Outside, from where he can either Lock! the door or just leave the location to go Away. The "U" in Outside means this location is urgent and thus no time may pass while any automata is in such a location. The Door is initially Locked -from here someone may request to enter ?, after which the Door responds with ok!: the "C" in the location means committed and is similar to urgent locations, but in addition to stopping time, it also ensures that only components in committed locations may move next. The door may be lock?ed -from which it responds to an enter ? with a nok!. The Thief chooses some time, between 0 and 24 to attempt enter !ing -if he succeeds and gets an ok? from the Door he is happy and enters Succ. In case he is unlucky he receives an nok? and tries again later. Although simple, the above example contains the key elements of timed automata. To summarise, a timed automaton consists of locations and edges between locations. On locations one can write invariant expressions based on the values of clocks, like x <= 14. A clock is a real-valued counter that increases as time progresses. While moving along an edge, a TA may synchronise with another over a set of channels: in uppaal the convention is that a! means "send on a", and a? means "receive on a". Not shown in the example is that edges can be "guarded" by expressions over clocks.

Let c be a clock then we call an element c ≤ n (c ≥ n) an upper (lower) bound and denote by B ≤ (C) (B ≥ (C)) the set of all finite conjunctions of lower (upper) bounds. For a finite set of channels Σ we denote by Σ o = {a!|a ∈ Σ} and Σ i = {a?|a ∈ Σ} the output and input actions over Σ respectively. Definition 4 (Timed Automaton). A timed automaton (TA) is a 6-tuple A = (L, C, 0 , A , →, I), where 1) L is a finite set of locations, 2) 0 ∈ L is the initial location, 3) C is a finite set of clocks, 4) Σ is a finite set of channels, 5) → ⊆ L × G(C) × 2 C × L is the (non-deterministic) transition relation. We write g,a,R -→ for a transition, where is the source and the target location, g ∈ B ≤ (C) is a guard, a ∈ Σ o ∪ Σ i is a label, and R ⊆ C is the set of clocks to reset, and 6) I : L → B ≥ (C) is an invariant function, mapping locations to a set of invariant constraints.

A clock valuation is a function v : C → R ≥0 . We denote all clock valuations over C with V(C). We need two operations on clock valuations:

v = v + d for a delay of d ∈ R ≥0 time units, s.t. ∀c ∈ C : v (c) = v(c) + d, and reset v = v[R] of a set of clocks R ⊆ C, s.t. v (c) = 0 if c ∈ R, and v (c) = v(c) otherwise.
We write v g to mean that the clock valuation v satisfies the clock constraint g.

The semantics of a TA (L, C, 0 , A , →, I) is a timed transition system with states L × V(C) and initial state ( 0 , v 0 ), where v 0 assigns zero to all clocks. From a state ( , v) the TA may transit via a discrete transition ( , v)

a -→ ( , v ) if there exists an edge g,a,r ---→ , v g and v = v[r]. Time-wise the TA can perform a delay d ∈ R ≥0 via a time transition ( , v) d -→ ( , v + d) if v + d I( ). Several TAs A 1 , A 2 , . . . , A n , A i = (L i , C i , i 0 , Σ, → i , I i
) may be joined into a network of timed automata. The state space of such a composition is the product of the individual TAs state spaces. From a state (s 1 , s 2 , . . . , s n ) the network can do a discrete output transition (s 1 , s 2 , . . . , s n ) a! -→ (s 1 , s 2 , . . . , s n ), if there exists an i, such that s i a! -→ s i and for all j = i s j a?

-→ s j or it can can delay d time units, (s

1 , s 2 , . . . , s n ) d -→ (s 1 , s 2 , . . . , s n ), if for all i s i d -→ s i .
Notice we are using broadcast synchronisation for accommodating the use of uppaal SMC. Furthermore, we will assume that components are input-enabled and action-deterministic thus for any action there is at most one successor and for any input action there is at least one.

Stochastic Semantics

The stochastic semantics of networks of timed automata was laid out by David et al. [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF]. In a state, each timed automaton is given a delay density and a probability mass function for selecting output actions. The semantics is now race based: components select a delay, t, according to their delay distribution, and the one with the smallest delay is selected the winner. After the entire network performs the delay, the winner selects an output according to its probability mass function. The remaining network respond to this output by performing the corresponding input. Afterwards a new race commences. In uppaal SMC bounded delays (i.e. the current location has an invariant) are selected from a uniform distribution ranging from the minimal delay before some guard is satisfied and the maximal delay, where the invariant is still satisfied. For unbounded delays the delay is selected from an exponential distribution.

In the preceding example, the probability that the Thief enters the house without the Resident being home within 12 time units is:

12 0 1 14 • 24 t 1 24 dt • 1 2 • 12-t 0 1 24 -t dτ dt ≈ 0.13
Game Semantics In recent works [START_REF] David | On time with minimal expected cost![END_REF][START_REF] David | Uppaal stratego[END_REF] the simple stochastic timed automata model has been given a game semantics. In this semantics the edges of timed automaton A = (L, C, 0 , A , →, I) are partitioned into a controllable set of edges, → C , and uncontrollable set of edges → U . The uncontrollable edges are controlled by stochastic environment behaving according to the stochastic semantics above, while the controllable set of edges is controlled by an actor that tries to "drive" the system into a given goal state. In Fig. 4 the dashed edges correspond to uncontrollable edges and the controllable edges are the solid edges.

A tool like Uppaal-Stratego can, by using reinforcement learning, find deterministic strategies for minimising the expected time (or cost) of reaching a goal -taking the stochastic environment into account.

Timed Automata Encoding

The timed automata encoding of the attack-defense tree semantics given in the previous sections consists of three automata; one encoding the attacker, one encoding the defender and one encoding the environment selecting an outcome for the execution of attacker actions (γ Succ ). Furthermore, the encoding has one boolean variable b pa per atomic proposition, p, in the attack-defense tree. The state of these boolean variables directly corresponds to the states of the ADG. Let A a be the set of attacker actions in the attackdefense-tree, then for each p a ∈ A a we create a channel c pa that is used by the attacker to indicate that he wishes to execute p a . The environment responds to this by deciding an outcome in accordance with γ Succ . Fig. 5 depicts the modelling of the environment for an attack-defense tree, where there is only one attacker action (p a ); here 1 -p is the probability that p a succeeds. Let A d be the set of defender actions available to the defender. For each D ∈ 2 A d the defender has an edge, where he sets all boolean variables, p d ∈ D, to true. In Fig. 6 an example modelling of this is shown with two defender actions. As the edges of this defender are uncontrollable, the defender would select a set of defense measures by a uniform choice among all the edges. For analysing possible attack scenarios in response to a specific set of defense measures D we would delete edges of the defender until only the edge corresponding to D remains.

Environmental Modelling

Defender Modelling

Attacker Modelling

In the formal development of an attacker we just defined general requirements that any attacker should respect. Firstly, we present a non-deterministic attacker that is as general as possible, which can be used for learning; afterwards we create one specific attacker profile, where the non-determinism is resolved by a probability mass function. Non-deterministic Attacker Assume we have A a = {p a } as our set of attacker actions and let each of the attacker propositions have a lower execution bound (L pa) and an upper execution bound (U pa) -an execution time that is not controllable by the attacker and thus will be selected according to a uniform distribution by the environment. Fig. 7 depicts an attacker with only one action: from the initial state, the attacker can decide to perform p a , if it is not already true and the tree is not already true (!{t}); after which it enters a location, where the environment decides how long the execution takes according to the uniform distribution. After this waiting time the environment is informed of the attempt to execute p a and decides on the outcome. Also, during this transition the cost of executing p a is added to the variable i attC ost. For the case with several propositions, the cycle in Fig. 7 is added for each proposition.

In case the tree is true, the attacker only has one option, namely, to enter the location, where he cannot do anything.

Uniform Attacker

The uniform attacker is essentially the non-deterministic attacker, where the non-determinism of selecting an action is resolved by a uniform choice among all possible actions. The translation into timed automata described in the preceding section has been implemented as a python script. This script takes the attack-defense tree, the description of the cost of atomic attacker actions, the execution time and their probability of succeeding. Having translated into timed automata, we can now take advantage of the uppaal [START_REF] Behrmann | A tutorial on Uppaal[END_REF] model checking engine to answer some of the questions raised in the previous sections. For instance, question 3 is answerable by a simple timed reachability check by uppaal. In the following we focus on answering question 5 and question 6. We consider the attack-defense tree in Fig. 1. The success probability and cost of the various attacker actions are summarised in Fig. 8. The L column is the lower bound of the execution time, U is the upper bound, C is the cost of the actions and F is the success probability.

Expected Cost

We first show how to answer question 5 by finding expected cost of the uniform attacker within 300 time units. The cost of the attacker is estimated by the uppaal SMC with the query E[<= 300; 1000](max : i attCost). Table 1: Expected cost for the uniform attacker and for synthesised strategies.

The estimates for various defense measures are given in Table 1 in the "Uniform" row. From the results we can see that the highest cost (unsurprisingly) is obtained when all possible defender's actions are selected, and the smallest when none of them are selected. Also the results indicate that by performing t2, t1, tf the expected cost is equivalent to performing all of the defense measures. This is because this set jointly blocks large parts of the attack-defense tree, leaving only the expensive "threaten" and " blackmail" for an attacker to succeed.

Finding Good Attacker Profile

Next we answer question 6 i.e. we focus on a stochastic attacker, who minimises his costs in response to various defense measures. For doing this, we apply the non-deterministic attacker of our encoding and use the Uppaal-Stratego to minimise the cost variable. The queries for the Uppaal-Stratego are strategy s = minE(bi attCost)[<= 300] :<> t E[<= 300; 1000](max : bi attCost) under s, where t is the attack-defense tree translated into the uppaal syntax.

The result of executing these queries for different defenders are reported in Table 1 in the Uppaal-Stratego row. As can be seen, the synthesized attacker generally obtains a reduced expected cost. The reason is that he can avoid attempting attacks he knows are blocked due to the defender's measures. Another reason is that this attacker actively attempts to minimise his costs; meaning he will not take the expensive "threaten" or "bribe" if it can be avoided.

Conclusion

In this paper we have shown how to separate the modelling of attacker's and defender's behaviours from the attack-defense tree. In this way we allow modelling complex temporal behaviours without compromising the intuitively simple description of various ways of achieving an attack expressed in the attack-defense tree. This stands in opposition with, for example, the work [START_REF] Hermanns | The value of attackdefence diagrams[END_REF] that adds temporal behaviours by introducing sequential gates, trigger gates and reset gates, which may clutter the description of possible attacks. Experiments reported in the paper have shown the different analyses that can be performed on our encoding using the uppaal SMC and Uppaal-Stratego: among these are finding an attacker who minimises his costs, and estimating the probability of an attack for a specific attacker.

In the future we wish to extend the current framework by describing the actual behaviour of the attacker in a more thorough way. This may include incorporating parts of the work by Hermanns et al. [START_REF] Hermanns | The value of attackdefence diagrams[END_REF], but we will maintain them in a separate modelling language.

Fig. 4 :

 4 Fig. 4: Model of a Thief, a Resident and a Door.

Fig. 5 :

 5 Fig. 5: Environmental modelling. In the figure p = 1γ Succ (p a )(p a ).

Fig. 6 :

 6 Fig. 6: Modelling the environment with two defender actions, p 1 d and p 2 d .

Fig. 7 :

 7 Fig. 7: Non-deterministic attacker modelling

L

  Fig. 8: Experimental setup.

Research leading to these results was partially supported by the European Union Seventh Framework Programme under grant agreement no. 318003 (TREsPASS). 1 https://www.opm.gov/cybersecurity/cybersecurity-incidents/ 2 http://usa.kaspersky.com/about-us/press-center/press-releases/ duqu-back-kaspersky-lab-reveals-cyberattack-its-corporate-netwo