Attack Graphs & Subset Sabotage Games

Abstract

We consider an extended version of sabotage games played over Attack Graphs. Such games are two-player zero-sum reachability games between an Attacker and a Defender. This latter player can erase particular subsets of edges of the Attack Graph. To reason about such games we introduce a variant of Sabotage Modal Logic (that we call Subset Sabotage Modal Logic) in which one modality quantifies over non-empty subset of edges. We show that we can characterize the existence of winning Attacker strategies by formulas of Subset Sabotage Modal Logic.

Keywords

Attack Graphs Sabotage Games Logics in Games

1 Introduction

Modern systems are inherently complex and security plays a crucial role. The main challenge in developing a secure system is to come up with tools able to detect vulnerabilities and unexpected behaviors at a very early stage of its life cycle. These methodologies should be able to measure the grade of resilience to external attacks. Crucially, the cost of repairing a system flaw during maintenance is at least two orders of magnitude higher, compared to fixing at an early design stage [9].

In the past fifty years, several solutions have been proposed to check system reliability and, in particular, system security. In this area a story of success is the use of formal methods techniques [9]. They allow checking whether a system is correct by formally checking whether a mathematical model of it meets a formal representation of its desired behavior. Recently, classic approaches such as model checking and automata-theoretic techniques, originally developed for monolithic systems [8, 20], have been meaningfully extended to handle open and multi-agent systems [1 , 25]. These are systems that encapsulate the behavior of two or more rational agents interacting among them in a cooperative or adversarial way, aiming at a designed goal [18].

In system security checking, a malicious attack can be seen as an attempt of an Attacker to gain an unauthorized resource access or compromise the system’s integrity. In this setting, Attack Graph [22] is one of the most prominent attack models developed and receiving much attention in recent years. This encompasses a graph where each state represents an Attacker at a specified network location and edges represent state transitions, i.e., attack actions by the Attacker. Then, it is the system’s duty to prevent unauthorized access from the Attacker in each state of the graph. Said more precisely, the Attacker’s goal is to reach a certain state of the Attack Graph by traveling through its edges, while the Defender’s goal is to prevent him from doing so. To do this, the Defender can dynamically deploy countermeasures preventing the attack to succeeds. The attacks are represented by the edges of the Attack Graph. If the Defender deploys a countermeasure and such countermeasure is successful, the Attacker will no longer be able to use an attack. We can formalize such a scenario as a two-player turn based game between the Defender and the Attacker, where in turn the latter moves along adjacent states (w.r.t. the Attack Graph under exam) and the former inhibits some attacks by erasing some subset of edges of the Attack Graph itself. The goal of the Defender is to block the Attacker to reach some designated states, while not blocking the entire system functionality. The kind of scenario that we have just sketched is an example of extendedsabotage game [31]. Sabotage games were introduced by van Benthem in 2005 with the aim of studying the computational complexity of a special class of graph-reachability problems. Namely, graph reachability problems in which the set of edges of the graph became thinner and thinner as long as a path of the graph is constructed. To reason about sabotage games, van Benthem introduced Sabotage Modal Logic. Such a logic is obtained by adding to the ◊-modality of classical modal logic another modality ♦. Let G be a directed graph and s one of its vertex (or states); the intended meaning of a formula ♦ φ is “♦ φ is true at a state s of G iff φ is true at s in the graph obtained by G by erasing an edge e”.

Our sabotage games differ from the one introduced by van Benthem because one of the players can erase an entire subset of edges of a given graph. To reason about such games, we introduce a variant of Sabotage Modal Logic that we call, for lack of wit, Subset Sabotage Modal Logic (SSML for short). The logic SSML is obtained by adding a modality ♦^⊂ to the language of classical modal logic. The intended meaning of a formula ♦^⊂ φ is “♦^⊂ φ is true at a state s of a directed graph G iff φ is true at s in the graph G′ that is obtained from G by erasing a non-empty set of its edges”. We prove that the model-checking problem for SSML is decidable and that the existence of an Attacker winning strategy over an Attack Graph can be expressed by using an SSML formula.

Structure of the work. The rest of the paper is structured as follows. In Sec 2 we discuss the related works. In Sec 3 we briefly present Sabotage Modal Logic. In Sec. 4 we present Attack Graphs, propose a formal definition of such objects in terms of Kripke structures and introduce, informally, subset sabotage games on Attack Graphs. Then, in Sec 5, we formally define the class of subset sabotage games on Attack Graphs that we are interested on. We define plays on such games and Attacker winning strategies. In the penultimate section (Sec 6), we introduce Subset Sabotage Modal Logic and show that the model checking problem for such logic is decidable. To prove such a result, we reduce the model checking problem of SSML to the one of SML by giving a translation of SSML-formulas into SML formulas. We then show that the existence of an Attacker winning strategies for a subset sabotage game over an Attack Graph, is equivalent to the satisfiability of a certain SSML formula at the root of the considered Attack Graph. The last section concludes by discussing possible future works.

2 Related Work

Several existing works have proposed different game-theoretic solutions for finding an optimal defense policy based on Attack Graphs. Most of these approaches do not use formal verification to analyze the game, but rather try to solve them using analytic and optimization techniques. The work in [11, 12] studies the problem of hardening the security of a network by deploying honeypots to the network to deceive the Attacker. They model the problem as a Stackelberg security game, in which the attack scenario is represented using Attack Graphs. The authors in [26] tackle the problem of allocating limited security countermeasures to harden security based on attack scenarios modeled by Bayesian Attack Graphs using partially observable stochastic games. They provide heuristic strategies for players and employ a simulation-based methodology to evaluate them. The work in [32] proposes an approach to select an optimal corrective security portfolio given a probabilistic Attack Graph. They define a Bayesian Stackelberg game that they solve by converting it into Mixed-Integer Conic Programming (MICP) optimization problem.

Since the games we introduce are a variant of sabotage games, our work is indebted to those dedicated to this type of games and to Sabotage Modal Logic [3 , 31]. In particular, the authors of [23] shows the decidability of the model-checking problem for Sabotage Modal Logic. Such a result is important to our work because we use it to show the decidability of the model-checking problem for Subset Sabotage Modal Logic. In [3] the authors develop a complete proof system for Sabotage Modal Logic, they define and study the notion of bisimulation, and they present an extensive discussion of sabotage games and their characterization via the logic.

The present work is an extended version of the material already published in [7]

3 Sabotage Modal Logic

In this section, we briefly present Sabotage Modal Logic (SML, for short). Such logic was proposed in 2005 by Van Benthem [31] as a format for analyzing games that modify the graphs they are played on. SML was later investigated in a series of papers. Before entering into the matter of SML, let us fix some notation and terminology that will be used in the following.

Notation & Terminology. Given a sequence ρ, we denote its length as |ρ|, and its (j + 1)-th element as ρ_j. For j ≤ |ρ|, let ρ_≥j be the suffix of ρ starting at ρ_j and ρ_≤j the prefix ρ₀ ⋯ ρ_j of ρ. The empty sequence will be denoted by ɛ. A tree is a (finite or infinite) connected directed graph, with one node designated as the root, and in which every non-root node as a unique parent (s is the parent of t, and t is the child of s is there is an edge from s to t) and the root has no parent. The arity of a node x in a tree $T$ is the number of children of x. A path $P = x_{0}, x_{1}, \dots$ is a (finite or infinite) sequence of nodes such x_i is the parent of x_i+1 for all i > 0. A branch is a path that is maximal and whose first node is the root. A node x is an ancestor of a node y if there is a path containing x whose last element is y (remark that every node is the ancestor of itself).

Given a non-empty set $P$ of atomic formulas, and a finite non-empty set Σ of labels, we define SML formulas by the following grammar: $φ : : = p ∣ ⊥ ∣ \neg φ ∣ φ \lor φ ∣ ◊ a φ ∣ ♦ a φ$

where $p \in P$ and a ∈ Σ. We define ⊤≐ ¬ ⊥. If φ and ψ are formulas, we define φ → ψ ≐ ¬ φ ∨ ψ, φ ∧ ψ ≐ ¬ (¬ φ ∨ ¬ ψ), □aψ ≐ ¬ ◊a ¬ φ and ■a ≐ ¬ ♦a ¬ φ. The size |φ| of a formula φ is inductively defined. It is 1 if φ is an atomic formula or ⊥, it is sizeofψ + 1 if φ = ∘ ψ with ∘ ∈ set ¬ , ◊a, ♦a and maxset|φ₁|, |φ₂| + 1 if φ = φ₁ ∨ φ₂.

We now define the structures that will serve as interpretation of SML-formulas

Definition 1. A rooted Kripke structure is a 〈 M = 〈S, s₀, Σ, R, V where S is a non-empty set of states, s₀ ∈ S is the initial state, Σ is a finite set of labels, R ⊆ S × Σ × S is the transition relation, and $V : S \to 2^{P}$ is the evaluation function, assigning a set of atomic formulas to any state s ∈ S.

If M = 〈S, s₀, Σ, R, V is a Kripke structure and E ⊆ R, we write M \ E to denote the Kripke structure obtained by erasing the subset E from the relation R. If e = (s, a, s′) ∈ R we say that e is a labeled edge or simply an edge, and that a is the label of e. For any a ∈ Σ, we denote by R_a the subset of labeled edges of R whose label is a, that is R_a = sete ∈ R ∣ e ∈ S × seta × S.

The notion of satisfaction of a formula φ at a given state s of a Kripke structure M (written M, s ⊨ φ) is inductively defined as follows:

M, s⊨ ⊥ never;

M, s ⊨ p iff p ∈ V (s);

M, s ⊨ ¬ φ iff not M, s ⊨ φ (notation M, snotmodelsφ);

M, s ⊨ φ ∨ ψ iff M, s ⊨ φ or M, s ⊨ ψ;

M, s ⊨ ◊aφ iff there is a s′ ∈ S such that (s, a, s′) ∈ R and M, s′ ⊨ φ;

M, s ⊨ ♦aφ iff there is (s₁, a, s₂) ∈ R such that M \ set (s₁, a, s₂) , s ⊨ φ.

We say that a formula φ is true in a rooted Kripke structure M (written M ⊨ φ) iff φ is true at the initial state of M. As we can see from the above definition, the meaning of the boolean connectives of SML logic is the standard one. Equally, the meaning of the ◊a-connective is the standard meaning in modal logic: a formula ◊aφ is true at a given state s of a Kripke structure whenever s is adjacent (with respect to an edge labeled by a) to a vertex s′ for which the property expressed by φ is true. The meaning of the♦a-connective can be spelled out as follows: a formula ♦aφ is true at a given state s of a Kripke structure M whenever φ is true at s in the Kripke structure M′ that is obtained by erasing an edge (s′, a, s″) from R in M.

Definition 2. The model checking problem for Sabotage Modal Logic consists of the following data and question:

Data 1: an SML formula φ,

Data 2: a rooted finite Kripke structure M,

Question: Is it the case that M ⊨ φ?

The proof of the following theorem can be found in [23].

Theorem 1. The model checking problem for Sabotage Modal Logic is PSPACE-complete.

4 Attack Graphs

The term Attack Graph has been first introduced by Phillips and Swiler [29]. Attack Graphs represent the possible sequence of attacks in a system as a graph. An Attack Graph may be generated by using the following pieces of information:

a description of the system architecture (topology, configurations of components, etc.);

the list of the known vulnerabilities of the system;

the Attacker’s profile (his capabilities, password knowledge, privileges, etc.) and attack templates (Attacker’s atomic action, including preconditions and postconditions).

An attack path in the graph corresponds to a sequence of atomic attacks. Several works have developed this approach, see e.g., [16 , 30], and [19] for a survey. Each of the previously cited works introduced its own Attack Graph model with its specificity, and thus there is no standard definition of an Attack Graph. However, all introduced models can be mapped into a canonical Attack Graph as introduced in [15]. It is a labeled, oriented graph where:

each node represents both the state of the system (including existing vulnerabilities) and the state of the Attacker including constants (Attacker skills, financial resources, etc.) and variables (knowledge of the network topology, privilege level, obtained credentials, etc.);

each edge represents an action of the Attacker (a scan of the network, the execution of an exploit based on a given vulnerability, access to a device, etc.) that changes the state of the network or the states of the Attacker; an edge is labelled with the name of the action (several edges of the Attack Graph may have the same label).

An Attack Graph is said complete whenever the following condition holds: for every state q and for every atomic attack att, if the preconditions of the atomic attack hold in q, then there is an out coming edge from q labeled with att.

By abstracting all the data of the above discussion, one can see an Attack Graph as a directed graph together with a labeling of its vertices and edges. The labeling of vertices is used to specify which properties (the kind of properties mentioned in 1) are true at a certain vertex, while the edge labeling specifies the name of the action of the Attacker. As we have seen in the example above, it is also useful to specify the set of Attacker’s target states. We thus define an Attack Graph as follows:

Definition 3. Suppose that the set $P$ contains an atomic proposition win. An Attack Graph is a 〈 AG = 〈S, s₀, Σ, R, V, T where:

〈S, s₀, Σ, R, V is a rooted Kripke structure where the set S of states is finite and for all a ∈ Σ if (s, a, s′) ∈ R then there is no b ∈ Σ such that (s, b, s′) ∈ R.

T is a non-empty subset of S such that win ∈ V (s) for all s ∈ T.

The set T represent the set of target states of the Attacker.

Example 1. Consider the following scenario: an enterprise has a local area network (LAN) that features a Server, a Workstation and two databases A and B. The LAN also provided a Web Server. Internet access to the LAN is controlled by a firewall. Such a scenario is depicted in Figure 1. Suppose that we know some vulnerabilities and that we have established that a malevolent user can make the attack listed in Table 1, e.g., by making att₂ an Attacker can exploit a vulnerability related to the Server: as a precondition, the Attacker needs to have root access to the Web Server and, as a postcondition, he will obtain root access to the Server.

Fig. 1

An illustrating LAN architecture example.

Table 1

Atomic attacks and countermeasures over the LAN of Figure 1.

Attack	Location	Precondition	Postcondition	Counter measure
att ₁	Web Server		web _ server : root	_
att ₂	Server	web _ server : root	server : root	c ₂
att ₃	Workstation	web _ server : root	password : 1234	_
att ₄	Database A	server : root	databaseA : root	c ₄
att ₅	Database B	server : root∧	databaseB : root	c ₅
		password : 1234

Then we can construct an Attack Graph built from this set of atomic attacks and collecting possible attack paths as depicted in Figure 2 1 . The Attacker’s initial state is a node in the Attack Graph. Let us suppose that the Attacker is in state s₁ and wants to reach state s₄. To get to this target, she can perform the sequences of atomic attacks att₂, att₄ or att₃, att₂, att₄.

Fig. 2

Example of Attack Graph, the atomic proposition satisfied at a given state are listed below the state itself.

5 Attack Graphs & Games

In the previous section, we saw that given a specific description of a system together with its vulnerabilities, we can generate a graph representing the dynamics of attacks that are possible over the system. Given a set of target states over such a graph, one can ask whether there is a path from an initial state to one of these target states, i.e., by reasoning over Attack Graphs, we can encode a security problem as a graph-reachability problem. Let us make one step more by adding a dynamic to such reachability problems. An Attack Graph represents a sequence of possible actions made by an Attacker to reach a specific goal. Let us add another character to this story, the Defender, whose objective is to counter the attack. Suppose that she has the power to dynamically deploy a predefined set of countermeasures: for instance by reconfiguring the firewall filtering rules, or patching some vulnerabilities, that is by removing one or several preconditions of an atomic attack. A given countermeasure c will prevent the Attacker from launching a given attack att: deploying c is equivalent to removing all the edges in the Attack Graph labeled with att. In real situations, due to budget limitations or technical constraints, the set of available countermeasures may not cover all atomic attacks. Now that we have specified what is the Defender’s power, we can consider a turn-based game between an Attacker and a Defender. Both players play on an Attack Graph 〈S, s₀, Σ, R, V, T. The Attacker’s goal is to reach one of the states in T, while the Defender’s goal is to prevent him from doing so. The Defender starts the game by selecting a certain countermeasure. By choosing such a countermeasure, she deletes a subset of the edges of the Attack Graph. The Attacker takes his turn and moves from s₀ to one of its successors along the edges that have not been erased (if any). The game evolves following this pattern. The Attacker won if he can reach one of the states in T in a finite number of moves, the Defender wins otherwise.

Example 2. Consider again the Attack Graph of Fig. 2. Suppose that the initial state is s₁. Suppose that the Defender has at her disposal a countermeasure c₂ for attack att₂, c₄ for attack att₄, and c₅ for attack att₅, but no one for the attacks att₁ and att₃ as reported in the last column of Table 1. The Defender starts the game by deploying countermeasure c₃. The only edge of the Attack Graph labeled by att₃ is the one going from s₁ to s₃; consequently, such edge is erased from the Attack Graph and the Attacker can only move to s₂. The Defender takes again the turn and deploys countermeasure c₂. There are two edges that are labeled by att₂ and both are erased from the Attack Graph. The Attacker moves from s₂ to s₄ and, since s₄ is a target state, she wins the game.

There is a natural way to look at the games described above: at each round, the Attacker can follow an edge from his current position in the given graph, but the Defender can choose a new graph (which is a subgraph of the current graph) missing a subset of edges. To precisely define such plays, we first need an auxiliary notion. We know that it is reasonable to assume that the Defender is unable to counter each of the Attacker’s possible attacks. At each step of the game, she can only deactivate a relation contained in a certain subset of the Attack Graph relation set. As mentioned above, we can consider that the Defender selects a sub-graph of the current Attack Graph whenever it is her turn to move. According to the limitation set out above, this sub-graph must be obtained by deleting some specific subset of the set of labeled edges. We define this notion as follows.

Definition 4. Let AG = 〈S, s₀, Σ, R, V, T be an Attack-graph and Δ ⊆ Σ. The Attack Graph AG′ is Δ-reachable from AG iff AG′ = 〈S, s₀, Σ, R \ R_b, V, T for some b ∈ Δ or AG′ = AG.

We have now all the ingredients to define a play in our game.

Definition 5. Let AG = 〈S, s₀, Σ, R, V, T be an Attack-graph and Δ a non-empty subset of Σ. A Δ-play ρ is a non-empty sequence ρ of length at least 2 where ρ₀ = AG, ρ₁ = s₀ and for all 2 < j ≤ |ρ|:

ρ_j is an Attack Graph if j is even.

ρ_j is a state of S if j is odd.

ρ_j is Δ-reachable from ρ_j-2, if j is even.

(ρ_j-2, a, ρ_j) ∈ R is an edge in the Attack Graph AG′ = ρ_j-1 for some a ∈ Σ, if j is odd.

Let ρ be a finite Δ-play whose last element is state s. We say that the Attack Graph AG′ is legal for ρ iff win ∉ V (s) and the sequence obtained by concatenating ρ to AG′ is a Δ-play.

Remark that given any Δ-play ρ and any even natural number j < |ρ|, the sequence ρ_≥j is a Δ-play over the Attack Graph obtained by setting the state ρ_j+1 as initial state of the Attack Graph ρ_j. If ρ is Δ-play we denote by ρ^A (resp. ρ^S) the subsequence of ρ in which only Attack Graphs (resp. states) appears.

Definition 6. Let ρ be a Δ-play over an Attack Graph AG. We say that ρ is won by the Attacker iff |ρ|=2n for some $n \in ℕ$ and there is no Attack Graph AG′ legal for ρ.

Said plainly: the Attacker wins the game whenever he reaches one of his target states.

Fig. 3

Another example of Attack Graph. The red state is the only state in T.

According to the above definition of play, the same state can appear many times in the same play. For instance, consider the Attack Graph AG shown in Figure 1. Let AG′ be the Attack Graph obtained by deleting from AG the edge labeled by c. Consider the following setc-play ρ over AG: $\begin{matrix} AG & s_{0} & {AG}^{'} & s_{0} & {AG}^{'} & s_{0} & {AG}^{'} & s_{1} & {AG}^{'} & s_{2} & {AG}^{'} & s_{3} \\ ρ_{0} & ρ_{1} & ρ_{2} & ρ_{3} & ρ_{4} & ρ_{5} & ρ_{6} & ρ_{7} & ρ_{8} & ρ_{9} & ρ_{10} & ρ_{11} \end{matrix}$

We can see that the vertex s₀ appears three times in such a play. We define another class of plays in which this phenomenon cannot happen.

Definition 7. Let ρ be a Δ-play over an Attack Graph AG. We say that ρ is stubborn whenever for any 0 ≤ j ≤ |ρ| if j is odd then there is no i < j such that ρ_i = ρ_j.

The definition above precludes the Attacker from choosing the same vertex of an Attack Graph in two different turns of the play. As an example, the setc-play presented above is not a setc stubborn play over AG because ρ₁ = ρ₃ = ρ₅.

Every stubborn Δ-play is a Δ-play. If ρ is a stubborn Δ-play over an Attack Graph AG, then |ρ|≤2 (|S|-1), where S is the set of states of AG. This is because if s and s′ are two distinct states of AG and there is a path p₀ ⋯ p_k where all the states p_i are distinct, then k ≤ |S|-1.

A strategy is usually defined as a function. A function that specifies, at each moment of the game, which move a player must play according to the moves previously played (the history of the game). A strategy is winning when the player who is following the strategy wins, whatever the history of the game is. We choose another equivalent definition of strategy. We informally describe how a strategy should operate and then formalize this notion. Imagine being engaged in a game $G$ , that the last move of $G$ was played according to the strategy, and that it is now the Opponent’s turn to play. The Opponent could extend the game in different ways: for example, if you are playing chess, you are white, and you just made your first move by moving a pawn to a certain position of the chessboard, black can in turn move a pawn or move a horse. If you are playing according to the strategy, the strategy should tell you how to react against either type of move. Therefore, a strategy can be viewed as a tree in which each node is move of the game, your Opponent’s move have at most one child and your moves have as many children as there are available moves (with respect to the considered play) for the Opponent. We therefore define strategies as follows:

Definition 8. An Attacker Δ winning strategy strat for an Attack Graph AG is a finite tree in which each branch is a Δ-play won by the Attacker and moreover:

for all node v of strat: if v is an Attack Graph then v has a unique child;

for all node v of strat: if v is a state of AG then v has as many children as there are Δ-reacheable Attack Graphs from the parent of v.

A strategy is stubborn iff every branch of the strategy is a stubborn play.

Remark that any winning Stubborn strategy is a winning strategy by definition.

Let α = AG₀ ⋯ AG_n be a finite non empty sequence of Attack Graphs. Suppose that AG₀ = 〈S, s₀, Σ, R, T and for all 1 ≤ i ≤ n, AG_i = 〈S, s_e, Σ, (R \ E₁ ∪ ⋯ ∪ E_i) , T where for each i, E_i is an eventually empty subset of R. If E is a set of edges such that for all e ∈ Ee is of the form (s, a, s′) for some s, s′ ∈ S and a ∈ Σ, then we denote by α_+E the sequence ${AG}_{1}^{'} \dots {AG}_{n}^{'}$ where ${AG}_{0}^{'} = 〈 S, s_{0}, Σ, R \cup E, T$ and for all 1 ≤ i ≤ n, AG_i = 〈S, s₀, Σ, ((R ∪ E) \ E₁ ∪ ⋯ ∪ E_i) , T.

Let strat be a winning Attacker Δ-strategy for some Attack graph AG. A critical section of strat is a sequence of nodes s′ ⋯ s′ that starts and ends with a node s′ ∈ S and that lies along one of the branches of strat. Clearly strat is stubborn iff strat does not contain any critical section.

Proposition 1. For any Attack Graph AG if there is a winning Attacker Δ-strategy strat for AG then there is a winning Attacker stubborn Δ-strategy ^strat′ for AG.

Proof. The proof is by induction on the number n of critical sections of strat. If n = 0, then strat is already a stubborn strategy, and we are done. Suppose that the hypothesis of the proposition holds for any winning strategy having at most n critical sections, and let strat be a strategy with n + 1 critical sections. Choose a critical section s′ ⋯ s′ of strat. In strat there is a finite number of branches ρ¹, …, ρⁿ for n ≥ 1 in which such a critical section is included, that is: each of the ρ^j has the form ρ′ s′ ⋯ s′ τ for some alternated sequence of Attack Graphs and states τ, and some path ρ′ of strat. The idea of the proof is to cut the critical section s′ ⋯ s′ from any of these branches and modify the Attack Graphs of the obtained sequence to obtain a play. Such a modification is obtained by using the construction define below Definition 5. Let us denote by c the critical section s′ ⋯ s′ and let R_c be the set of edges deleted by the Defender along c. For any ρ¹ … ρⁿ we define $ρ_{★}^{j} = ρ^{'} s^{'} τ_{★}$ where $τ_{★}^{A} = τ_{+ R_{c}}^{A}$ and $τ_{★}^{S} = τ^{S}$ . Any $ρ_{★}^{j}$ is a Δ-play won by the Attacker. Let _strat ★ be the tree of plays induced by the transformation above. Clearly, _strat ★ is a winning Attacker strategy for AG that contains less critical sections than strat. We apply the induction hypothesis and we obtain that there is a winning stubborn strategy ^strat′ for AG. □

6 Games & Subset Sabotage Modal Logic

In this section, we explain why we cannot directly use SML to reason about the above introduced games. We then introduce the Subset Sabotage Modal Logic (SSML) precisely to rectify this problem and we study its properties. In particular, we prove that the model checking problem for SSML is decidable and that the existence of an Attacker Winning strategy is equivalent to the satisfiability of a certain SSML formula.

6.1 What is the problem with SML?

Plays, that we defined in the previous sections, are nothing more than runs in an insidious sabotage game. In a sabotage game, one of the two players can delete an edge of the graph when it is her turn to move. In our games, one of the two players can delete a subset of edges of the graph when it is her turn to move. In [3] the authors claims that, by using our terminology, the existence of an Attacker winning strategy for a Sabotage Game over a finite rooted Kripke structure M = 〈S, s₀, Σ, R, V can be expressed by using a particular SML-formula. Such formula is defined by induction on n, $λ_{n} = {\begin{matrix} win & if n = 0 \\ ◊ ⊤ \land ■ ◊ (λ_{n - 1} \lor win) & otherwise \end{matrix}$ (1)

where ■φ ≐ ⋀ _a∈Σ■aφ and ◊φ ≐ ⋁ _a∈Σ◊aφ for a given SML formula φ, and ◊⊤ is used to check that the ■ is not satisfied because some relation is empty.

More precisely, if M = 〈S, s₀, Σ, R, V is a Kripke structure such that win ∈ V (s) for some s ∈ S and sizeofS = n ≥ 1 then M, s₀ ⊨ win ∨ λ_n-1 if and only if there is an Attacker winning strategy for the sabotage game played over M. Such a result is false in the case of the particular class of sabotage games that we have defined in the previous section, precisely because the Defender erases a subset of R at each step of the game.

Fig. 4

An additional example of Attack Graph. The red states are the only ones in T.

For instance, consider the Attack Graph depicted in Fig. 4. We can see that there is no seta-winning strategy over M. If the Defender erases any edge labeled with a, the Attacker would not be able to move from s₀ to one of the winning states s₁ or s₂. On the contrary, the formula win ∨ λ₂ = win ∨ (◊ ⊤ ∧ ■ ◊ (λ₁ ∨ win)) is true at s₀ in M. This is because if the top-most a-edge is removed, the Attacker can pass from the lowermost edge to reach a winning state, and he can pass from the top-most one if the lower one is removed.

6.2 Subset Sabotage Modal Logic

To speak about our particular games, we introduce a variant of Sabotage Modal Logic. We call such variant of Sabotage Modal Logic, Subset Sabotage Modal Logic.

Definition 9. Given a non-empty set $P$ of atomic propositions and a finite non-empty set Σ of labels, formulas of Subset Sabotage Modal Logic (SSML, for short) are defined by the following grammar: $φ : : = p ∣ ⊥ ∣ \neg φ ∣ φ \lor φ ∣ ◊ a φ ∣ a φ$

where $p \in P$ and a ∈ Σ. Given a rooted Kripke structure M = 〈S, s₀, Σ, R, V, recall that for a ∈ Σ, R_a denote the subset of R defined by sete ∈ R ∣ e ∈ S × seta × S. The definition of satisfaction of an SSML formula at a state s of a Kripke structure M is defined inductively. Such definition is the same as SML for atomic proposition, negation, disjunction and the diamond modality. It is defined as follows for the removea-modality:

M, s ⊨ removeaφ iff there is a non-empty subset E of R_a such that M \ E, s ⊨ φ

where M \ E denotes the structure M from which we have erased the subset E of edges. If φ is an SSML formula we define ■ ⊂aφ ≐ ¬ removea ¬ φ.

Remark 1.M, s ⊨ ■ ⊂aφ if and only if for any non-empty subset E of R_a we have that M \ E, s ⊨ φ, R_a included. This implies that if M, s ⊨ ■ ⊂aφ then M \ R_a, s ⊨ φ.

We now define the model checking problem for SSML.

Definition 10. The model checking problem for SSML consists of the following data and question:

Data 1: a finite rooted Kripke structure M,

Data 2: a SSML formula φ,

Question: is it the case that M ⊨ φ?

In what follows, we show that the model checking problem for SSML is EXPTIME decidable. To do so, we reduce the model-checking problem for SSML to the model-checking problem for SML.

The idea of the proof is the following: we are considering a finite Kripke structure. As a consequence, any of its non-empty subset of edges is finite. We give a name n_e to each edge e of M obtaining a Kripke structure M′. We remark that M ⊨ removeaφ iff there is a finite, non-empty subset of edges sete₁, … e_n of R_a such that M \ sete₁, …, e_n ⊨ φ. If φ is a SML formula then M′ ⊨ ♦n_{e
₁} ⋯ ♦n_{e
_n} φ, that is M′ \ setn_{e
₁}, … n_{e
_n} ⊨ φ, where each n_{e
_i} is the name of edge e_i. Thus, we need to give a translation from SSML-formulas to SML formulas. Such translation will be parametrized by Kripke structures because we need to consider their subsets of edges.

Definition 11. Let M = 〈S, s₀, Σ, R, V be a finite rooted Kripke structure. For all a ∈ Σ, let $f : R \to ℕ$ be an injective function associating to each member e of R a natural number n_e. We define the structure $M^{\subset} = 〈 S^{\subset}, s_{0}^{\subset}, Σ^{\subset}, R^{\subset}, V^{\subset}$ as follows:

the set of states of M^⊂ and its initial state are the same of M;

the set of labels Σ^⊂ is setn_e ∣ e ∈ R;

(s, n_e, s′) ∈ R^⊂ iff for some a ∈ Σ f (s, a, s′) = n_e;

the evaluation function V^⊂ is V.

By the definition above, if n_e ∈ Σ^⊂, there is exactly one edge e ∈ R_{n
_e} = sete ∈ R^Σ ∣ e ∈ S × setn_e × S. Remark that the transformation is linear in the number of states of the structure.

Remark 2. Let M be a finite rooted Kripke Structure, E any non-empty subset of R and M^⊂ the corresponding Kripke structure introduced above. For any non-empty subset E = sete₁, …, e_n of R: (M \ sete₁, …, e_n) ^⊂ = M^⊂ \ setn_{e
₁}, …, n_{e
_n}.

If E = sete₁, …, e_n is a subset of edges of M and φ is a formula, we write ♦_{n
_E} φ as a short-cut for the formula ♦_{n
_{e
₁}} ⋯ ♦ _{n
_{e
_n}} φ where each n_{e
_i} is the label corresponding to e_i in M^⊂.

We define a function that maps an SSML formula φ to an SML formula $(φ)_{M}^{★}$ . Such a function takes as arguments a Kripke Structure M and an SSML formula φ, and gives as result an SML formula $(φ)_{M}^{★}$ . The function is defined on the structure of φ, as follows: $\begin{matrix} (p)_{M}^{★} & = p \\ (⊥)_{M}^{★} & = ⊥ \\ (\neg φ)_{M}^{★} & = \neg (φ)_{M}^{★} \\ (φ \lor ψ)_{M}^{★} & = (φ)_{M}^{★} \lor (ψ)_{M}^{★} \\ (◊ a φ)_{M}^{★} & = ⋁_{e \in R_{a}} ◊ n_{e} (φ)_{M}^{★} \\ (a φ)_{M}^{★} & = ⋁_{E \in 2^{R_{a}} \ \emptyset} (♦ n_{E} (φ)_{M}^{★}) \end{matrix}$

Remark that the above formula translation is exponential in the number of edges of the structure M taken as parameter.

Lemma 1. For any M = 〈S, s₀, Σ, R, V, for any SSML formula φ, for any state s ∈ S: M, s ⊨ φ iff $M^{\subset}, s ⊨ (φ)_{M}^{★}$

Proof. The proof is by induction on the size of φ. We omit the subscript M since it is clear from the context. If φ = p or φ =⊥ the result is immediate since V (s) = V^⊂ (s) for any state s. Suppose that the statement of the lemma holds for any formula of size k ≤ n, and let φ be a formula of size n + 1. If the main connective of φ is a boolean connective, the result follows by the induction hypothesis. If φ = ◊aψ:

M, s ⊨ ◊aψ iff there is s′ such that e = (s, a, s′) ∈ R and M, s′ ⊨ ψ. By induction hypothesis M^⊂, s′ ⊨ (ψ) ^★. By the definition of M^⊂ we have that (s, n_e, s′) ∈ R_{n
_e} thus s and s′ are adjacent, with respect to R_{n
_e}, in M^⊂. It follows that M^⊂, s ⊨ ◊n_e (ψ) ^★. But this means that M^⊂, s ⊨ ⋁ _{e∈R_a}◊n_e (ψ) ^★ as we wanted.

M^⊂, s ⊨ (◊aψ) ^★ iff M^⊂, s ⊨ ⋁ _{e∈R_a}◊n_e (ψ) ^★. If this is the case, then there is at least an edge e = (s, a, s′) ∈ R_a such that M^⊂, s ⊨ ◊n_e (ψ) ^★ which implies that M^⊂, s′ ⊨ (ψ) ^★. By induction hypothesis M, s′ ⊨ ψ. Since, by definition of M^⊂, (s, a, s′) ∈ R in M, we get the result.

If φ = removeaψ:

M, s ⊨ removeaψ iff there is a non-empty subset E = sete₁, … e_n of R_a such that M \ E, s ⊨ ψ. By induction hypothesis (M \ E) ^⊂, s ⊨ (ψ) ^★. As stated in Remark 6.2, (M \ E) ^⊂ = M^⊂ \ setn_{e
₁}, …, n_{e
_n}. Since M^⊂ \ setn_{e
₁}, …, n_{e
_n}, s ⊨ (ψ) ^★ we deduce that (⋯ (M^⊂, \ setn_{e
₁}) \ ⋯) \ setn_{e
_n}, s ⊨ ψ^★, thus M^⊂, s ⊨ ♦n_E ψ^★.

M^⊂, s ⊨ (removeaψ) ^★ iff M^⊂, s ⊨ ⋁ _{E∈2^R_a\∅} (♦n_E (ψ) ^★). This means that there is a subset E of R_a such that E = sete₁, …, e_n and M^⊂, s ⊨ ♦n_E (ψ) ^★. By definition of satisfaction, this means that (⋯ (M^⊂ \ setn_{e
₁}) \ ⋯) \ setn_{e
_n} ⊨ (ψ) ^★, thus M^⊂ \ setn_{e
₁}, …, n_{e
_n}, s ⊨ (φ) ^★. As stated in Remark 6.2, this implies that (M \ E) ^⊂, s ⊨ (ψ) ^★. By induction hypothesis, M \ E, s ⊨ ψ. By the fact that each e_i ∈ R_a, we obtain that M, s ⊨ removeaψ as we wanted.

□

From the above lemma, the fact the our formula translation from SSML to SML is exponential in the number of edges of the Kripke structure taken as parameter, and the fact the model checking problem for SML is decidable, we immediately deduce the following theorem.

Theorem 2. The model checking problem for SSML is in EXPTIME: if M = 〈S, s₀, Σ, R, V is a finite rooted Kripke Structure and φ an SSML formula, we can decide in exponential time whether M ⊨ φ or not.

It should not be surprising that we can express the existence of Attacker winning strategies for our games by using SSML: we have designed such logic with precisely this goal in mind.

Let AG = 〈S, s₀, Σ, R, V, T be an Attack Graph and Δ a non-empty subset of Σ. If φ is an SSML formula, we define the two SSML-formulas: $■ \subset Δ φ ≐ ⋀_{a \in Δ} ■ \subset a φ ◊ φ ≐ ⋁_{a \in Σ} ◊ a φ$

A strategy is a plan of action. As it is logical, the plan is winning when it leads me to victory, whatever my opponent’s plan of action. Thus, a winning strategy can be expressed as an alternance of universally quantified sentences and existentially quantified sentences “for all actions of my Opponent, there is an action that I can make that leads me to victory". Let us put ourselves in the villain’s shoes: suppose that we are the Attacker, and that, by playing, we have reached a certain state s of an Attack Graph AG. It is now Defender’s turn. If I have a winning strategy, I must be able to reach a successor state s′ of s in whatever subgraph AG′ of AG that is Δ-reachable from AG. Said differently, we must have that AG, s ⊨ ■ ⊂Δ ◊ φ = (■ ⊂a ◊ φ) ∧ ⋯ ∧ (■ ⊂b ◊ φ) for some formula φ that expresses the winning condition. Such formula is nothing but the SSML version of the one we have defined in 1.

Definition 12. [Winning Formulas] The family ${ψ_{Δ}^{n}}_{n \in ℕ}$ of Winning formulas is defined by induction on n as follows: $ψ_{Δ}^{n} = {\begin{matrix} win & if n = 0 \\ ◊ ⊤ \land ■ \subset Δ ◊ (ψ_{Δ}^{n - 1} \lor win) & otherwise \end{matrix}$ (2)

We are now ready to prove the main result of our paper. Namely, that the existence of a winning Attacker Δ-strategy over an Attack Graph AG is equivalent to the truth of a winning formula over AG.

Theorem 3. For any Attack Graph AG = 〈S, s₀, Σ, R, V, allowbreakT for any non-empty subset Δ of Σ, if |S| = n, then $AG, s_{0} ⊨ win \lor ψ_{Δ}^{n - 1}$ iff there is a winning Δ-strategy over AG for the Attacker.

Proof. Both directions of the theorem are proved by induction on n.

An Attack Graph has a non-empty set of states by definition. Thus, the base case is n = 1. AG, s₀ ⊨ win ∨ win ⇔ T = sets₀. The strategy we are looking for is the path AGs₀. Suppose that the statement of the theorem holds for any Attack Graph AG′ of size k ≤ n, and let AG be an Attack Graph of size n + 1. Suppose that $AG, s_{0} ⊨ win \lor ψ_{Δ}^{n}$ . Without loss of generality, we can suppose that AG, s₀notmodelswin because otherwise the result is trivial. Thus $AG, s_{0} ⊨ ψ_{Δ}^{n}$ . This means that $AG, s_{0} ⊨ ◊ ⊤ \land (■ \subset Δ ◊ (ψ_{Δ}^{n - 1} \lor win))$ . By the definition of satisfaction, $AG, s_{0} ⊨ (◊ ⊤ \land ■ \subset a ◊ (ψ_{Δ}^{n - 1} \lor win))$ for any a ∈ Δ. Let a one of the element of Δ. We have that, $AG, s_{0} ⊨ ◊ ⊤ \land ■ \subset a ◊ (ψ_{Δ}^{n - 1} \lor win)) \Leftrightarrow AG, s_{0} ⊨ ◊ ⊤ and AG, s_{o} ⊨ ■ \subset a ◊ (ψ_{Δ}^{n - 1} \lor win))$ . We can thus conclude that there is non-empty set of states S′ such that s′ ∈ S implies s′ ≠ s and (s, c, s′) ∈ R for some c ≠ a and $s^{'} ⊨ ψ_{Δ}^{n - 1} \lor win$ . Consider the subgraph AG′ of AG obtained by: erasing the vertex s₀, erasing any edge that has s₀ as source or target and erasing any edge whose label is a. The size of a such graph is n and (since s₀notmodelswin) $AG, s^{'} ⊨ ψ_{Δ}^{n - 1} \lor win$ for some s′ ∈ S. Let AG_a be the Attack Graph obtained by setting the state s′ as initial state of AG′. By induction hypothesis, there is a winning Δ-strategy _strata over AG_a. We obtain a winning strategy strat for AG by taking the sequence AG s₀ and putting an edge from s₀ to the root of _strata for any a ∈ Δ.

If n = 1 and there is a winning Attacker strategy strat over AG, then strat = setAG s₀. Thus s₀ ∈ T and this means that AG, s₀ ⊨ win and we can conclude. Suppose that the statement of the theorem holds for any Attack Graph AG′ of size k ≤ n, and let AG be an Attack Graph of size n + 1. Let strat be any winning strategy over AG. Suppose that strat contains more than one play (otherwise the result is trivial). By Proposition 5, we can suppose that strat is stubborn. Let Next = sets_i ∈ S ∣ ∃ ρ ρ isabranchof strat ∧ ρ₃ = s_i i.e., any s_i ∈ Next is a state that is adjacent to s₀ in the subgraph of AG obtained by erasing all edges labeled by b for some b ∈ Δ. Remark that Next is finite and non-empty and that, since strat is stubborn, each s_i is different from s₀. For any s_i, let AG_{s
_i} be the subgraph of AG obtained by erasing s₀, any edge having s₀ as source and whose initial state is s_i. Define _{strats_i} to be the tree whose branches are of the form AG_{s
_i} s_i ρ′ for s_i ρ′ subsequence of a play of strat. Clearly, _{strats_i} is a winning Attacker Strategy over the Attack Graph AG_{s
_i} for any s_i. Since AG_{s
_i} has n-states, we can use the induction hypothesis and conclude that ${AG}_{s_{i}}, s_{i} ⊨ win \lor ψ_{Δ}^{n - 1}$ . Any _{strats_i} is stubborn, thus s₀ does not appear in any of its play. We deduce that for any s_i ∈ Next, $AG, s_{i} ⊨ win \lor ψ_{Δ}^{n - 1}$ . From this latter fact, and by the definition of Next we conclude that $AG, s_{0} ⊨ ◊ ⊤ \land ■ \subset Δ ◊ (ψ_{Δ}^{n - 1} \lor win)$ .

□

Example 3. Consider the two following Attack Graphs:

There is not seta-winning strategy over the Attack Graph on the left. In fact, it does not satisfy the formula win ∨ (◊ ⊤ ∧ ■ ⊂a ◊ ((◊ ⊤ ∧ ■ ⊂a ◊ win) ∨ win)): we have that s₀notmodelswin and s₀notmodels■ ⊂a ◊ ((◊ ⊤ ∧ ■ ⊂a ◊ win) ∨ win)). If we erase all edges labeled by the letter a, no edges are left. Thus s₀notmodels ◊ φ for any φ.

Consider the Attack Graph on the right, call it AG_r and let ${AG}_{r}^{a}$ be AG_r without edges labeled by a and ${AG}_{r}^{b}$ be the AG_r without the edge labeled by b. The formula $win \lor ψ_{3}^{a, b}$ is satisfied by AG_r, and there is a winning strategy strat whose branches are: $ρ = {AG}_{r} s_{o} {AG}_{r}^{a} s_{3}$ and $τ = {AG}_{r} s_{0} {AG}_{r}^{b} s_{1}$

7 Conclusion and Future Work

We have presented a natural class of two-player games over Attack Graphs. Such games are played by an Attacker and a Defender. The Attacker tries to reach some vertex of the Attack Graph, while the Defender tries to prevent him from doing so. To do this, the Defender can eliminate subsets of arcs in the graph. We have seen how these games can be viewed as a generalized version of sabotage games, we have formally defined plays of such games and winning strategies. Finally, we have introduced a variant of Sabotage Modal Logic, showed that the model checking problem for such logic is decidable and that we can express the existence of a winning strategy for our subset sabotage games by formulas of the new logic.

The games we have defined are perfect information games; both players know, at every point in the game, the location of the other player. This assumption is unrealistic: during a cyberattack, a possible Defender may not know what state an Attacker is in, and conversely, an Attacker may not be aware of changes made by the Defender to counter his attack. We would therefore like to extend our play model in order to include this type of imperfect information. From the Defender’s point of view, this could be implemented as an equivalence class between Attack Graph states. From the Attacker’s point of view, on the other hand, we could think of a notion of weak bisimulation between Attack Graphs: the Attacker considers as equal two models that are bisimilar up to the identification of some subset of arcs. While the first notion of imperfect information would be fairly easy to develop, the second one is higly nontrivial. Indeed, we should consider equivalence classes between graphs that are generated with respect to both their topological structure and their labeling. For this reason, we prefer to leave this interesting development for future work.

We suspect that a bisimulation notion for SSML logic can be obtained by slightly modifying the one for SML and that, at the same, a complete proof system for SSML can be obtained in terms of tableaux. In conclusion, we suspect that the satisfiability problem for SSML logic is undecidable. Indeed, the same problem is undecidable for SML and since our logic is SML in which we quantify over subset of arcs of a graph, our intuition tells us that the satisfiability problem for SSML can only be more difficult than the one of SML.

Finally, we can consider to extend logics for the strategic reasoning such as ATL [1] and Strategy Logic [25] by capturing the features of the sabotage modalities ♦ and ♦^⊂. In this way, we can gain expressive power and check whether the attacker has a strategy to win the game via strategic operators. Furthermore, in this context, we can see ♦^⊂ as a graded modality of ♦ as done in logics for strategies [2, 13]. However, as we mentioned earlier the more realistic setting for games is with imperfect information, but unfortunately, the model checking problem with imperfect information for strategic logics is undecidable in general [10]. Given the relevance of this setting, even partial solutions to the problem can be useful, such as abstractions either on the information [4, 6] or on the strategies [5] or on the formulas [14]. In conclusion, we can embed the mentioned techniques to provide a more powerful framework.

Footnotes

This Attack Graph is not complete w.r.t. our previous description, since some possible sequences of atomic attacks are not listed: for instance att₁, att₂, att₃, att₅ are not taken into account.

References

Alur

, Henzinger

and Kupferman

, Alternating-time temporal logic, Journal of the ACM49(5) (2002), 672–713.

Aminof

, Malvone

, Murano

and Rubin.

, Graded modalities in strategy logic, Inf Comput261 (2018), 634–649.

Aucher

, Benthem

J.V.

and Grossi

, Modal logics of sabotage revisited, Journal of Logic and Computation28(2) (2018), 269–303.

Belardinelli

, Lomuscio

and Malvone

, An abstraction-based method for verifying strategic properties in multi-agent systems with imperfect information, In EAAI 2019, 2019, pp. 6030–6037.

Belardinelli

, Lomuscio

, Malvone

and Yu

, Approximating perfect recall when model checking strategic abilities: Theory and applications, J Artif Intell Res73 (2022), 897–932.

Belardinelli

and Malvone

, A three-valued approach to strategic abilities under imperfect information. In KR 2020, 2020, pp. 89–98.

Catta

, Leneutre

and Malvone

, Subset sabotage games & attack graphs, Workshop WOA23, 2022, pp. 209–218.

Clarke

E.M.

and Emerson

E.A.

, Design and synthesis of synchronization skeletons using branching time temporal logic. In O. Grumberg and H. Veith, editors, 25 Years of Model Checking - History, Achievements, Perspectives, volume 5000 of Lecture Notes in Computer Science, Springer, 2008, pp. 196–215.

Clarke

E.M.

, Grumberg

and Peled

D.A.

, Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.

10.

Dima

and Tiplea

, Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011.

11.

Durkota

, Lisý

, Bosanský

and Kiekintveld

, Approximate solutions for attack graph games with imperfect information, In GameSec 2015, 2015, pp. 228–249.

12.

Durkota

, Lisy

, Bosansky

and Kiekintveld

, Optimal network security hardening using attack graph games, IJCAI’15, AAAI Press, 2015, pp. 526–532.

13.

Faella

, Napoli

and Parente

, Graded alternating-time temporal logic, Fundam Informaticae105(1-2) (2010), 189–210.

14.

Ferrando

and Malvone

, Towards the combination of model checking and runtime verification on multi-agent systems, In PAAMS 2022, 2022, pp. 140–152.

15.

Heberlein

, Bishop

, Ceesay

, Danforth

, Senthilkumar

and Stallard

, A taxonomy for comparing attack-graph approaches. [Online] http://netsq.com/Documents/AttackGraphPaper.pdf, 2012.

16.

Ingols

, Lippmann

and Piwowarski

, Practical attack graph generation for network defense, ACSAC’06, 2006, pp. 121–130.

17.

Jamroga

and Murano

, Module checking of strategic ability, AAMAS 2015, 2015, pp. 227–235.

18.

Jennings

N.R.

and Wooldridge

, Application of intelligent agents, In Agent Technology:Foundations, Applications, and Markets, Springer-Verlag, 1998.

19.

Kaynar

, A taxonomy for attack graph generation and usage in network security, J Inf Secur Appl29(C) (2016), 27–56.

20.

Kupferman

, Vardi

and Wolper

, An automata theoretic approach to branching-time model Checking, Journal of the ACM47(2) (2000), 312–360.

21.

Kupferman

, Vardi

and Wolper

, Module checking, Information and Computation164(2) (2001), 322–344.

22.

Lippmann

R.P.

and Ingols

K.W.

, An annotated review of past papers on attack graphs, 2005.

23.

Löding

and Rohde

, Model checking and satisfiability for sabotage modal logic, In FST TCS 2003, 2003, pp. 302–313.

24.

Lomuscio

, Qu

and Raimondi

, MCMAS: A model checker for the verification of multi-agent systems, In CAV09, 2009, pp. 682–688.

25.

Mogavero

, Murano

, Perelli

and Vardi

M.Y.

, Reasoning about strategies: On the model-checking problem, ACM Transactions in Computational Logic15(4) (2014), 34:1–34:47.

26.

Nguyen

T.H.

, Wright

, Wellman

M.P.

and Baveja

, Multistage attack graph security games: Heuristic strategies, with empirical game-theoretic analysis, In MTD ’17, 2017, pp. 87–97.

27.

Noel

, Jajodia

, O’Berry

and Jacobs

, Efficient minimum-cost network hardening via exploit dependency graphs, In ACSAC 03, 2003, p. 86.

28.

, Boyer

W.F.

and McQueen

M.A.

, Ascalable approach to attack graph generation, In ACMCCS, 2006, pp. 336–345.

29.

Phillips

and Swiler

L.P.

, A graph-based system for network-vulnerability analysis, In NSPW98, 1998, pp. 71–79.

30.

Sheyner

, Haines

, Jha

, Lippmann

and Wing

, Automated generation and analysis of attack graphs, 2002, pp. 273–284.

31.

van Benthem

, An Essay on Sabotage and Obstruction, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 268–276.

32.

Zhang

and Malacaria

, Bayesian stackelberg games for cyber-security decision support, Decis Support Syst148 (2021), 113599.