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.
AlurR., HenzingerT. and KupfermanO., Alternating-time temporal logic, Journal of the ACM49(5) (2002), 672–713.
2.
AminofB., MalvoneV., MuranoA. and Rubin.S., Graded modalities in strategy logic, Inf Comput261 (2018), 634–649.
3.
AucherG., BenthemJ.V. and GrossiD., Modal logics of sabotage revisited, Journal of Logic and Computation28(2) (2018), 269–303.
4.
BelardinelliF., LomuscioA. and MalvoneV., An abstraction-based method for verifying strategic properties in multi-agent systems with imperfect information, In EAAI 2019, 2019, pp. 6030–6037.
5.
BelardinelliF., LomuscioA., MalvoneV. and YuE., Approximating perfect recall when model checking strategic abilities: Theory and applications, J Artif Intell Res73 (2022), 897–932.
6.
BelardinelliF. and MalvoneV., A three-valued approach to strategic abilities under imperfect information. In KR 2020, 2020, pp. 89–98.
7.
CattaD., LeneutreJ. and MalvoneV., Subset sabotage games & attack graphs, Workshop WOA23, 2022, pp. 209–218.
8.
ClarkeE.M. and EmersonE.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.
9.
ClarkeE.M., GrumbergO. and PeledD.A., Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
10.
DimaC. and TipleaF., Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011.
11.
DurkotaK., LisýV., BosanskýB. and KiekintveldC., Approximate solutions for attack graph games with imperfect information, In GameSec 2015, 2015, pp. 228–249.
12.
DurkotaK., LisyV., BosanskyB. and KiekintveldC., Optimal network security hardening using attack graph games, IJCAI’15, AAAI Press, 2015, pp. 526–532.
FerrandoA. and MalvoneV., Towards the combination of model checking and runtime verification on multi-agent systems, In PAAMS 2022, 2022, pp. 140–152.
15.
HeberleinT., BishopM., CeesayE., DanforthM., SenthilkumarC. and StallardT., A taxonomy for comparing attack-graph approaches. [Online] http://netsq.com/Documents/AttackGraphPaper.pdf, 2012.
16.
IngolsK., LippmannR. and PiwowarskiK., Practical attack graph generation for network defense, ACSAC’06, 2006, pp. 121–130.
17.
JamrogaW. and MuranoA., Module checking of strategic ability, AAMAS 2015, 2015, pp. 227–235.
18.
JenningsN.R. and WooldridgeM., Application of intelligent agents, In Agent Technology:Foundations, Applications, and Markets, Springer-Verlag, 1998.
19.
KaynarK., A taxonomy for attack graph generation and usage in network security, J Inf Secur Appl29(C) (2016), 27–56.
20.
KupfermanO., VardiM. and WolperP., An automata theoretic approach to branching-time model Checking, Journal of the ACM47(2) (2000), 312–360.
21.
KupfermanO., VardiM. and WolperP., Module checking, Information and Computation164(2) (2001), 322–344.
22.
LippmannR.P. and IngolsK.W., An annotated review of past papers on attack graphs, 2005.
23.
LödingC. and RohdeP., Model checking and satisfiability for sabotage modal logic, In FST TCS 2003, 2003, pp. 302–313.
24.
LomuscioA., QuH. and RaimondiF., MCMAS: A model checker for the verification of multi-agent systems, In CAV09, 2009, pp. 682–688.
25.
MogaveroF., MuranoA., PerelliG. and VardiM.Y., Reasoning about strategies: On the model-checking problem, ACM Transactions in Computational Logic15(4) (2014), 34:1–34:47.
26.
NguyenT.H., WrightM., WellmanM.P. and BavejaS., Multistage attack graph security games: Heuristic strategies, with empirical game-theoretic analysis, In MTD ’17, 2017, pp. 87–97.
27.
NoelS., JajodiaS., O’BerryB. and JacobsM., Efficient minimum-cost network hardening via exploit dependency graphs, In ACSAC 03, 2003, p. 86.
28.
OuX., BoyerW.F. and McQueenM.A., Ascalable approach to attack graph generation, In ACMCCS, 2006, pp. 336–345.
29.
PhillipsC. and SwilerL.P., A graph-based system for network-vulnerability analysis, In NSPW98, 1998, pp. 71–79.
30.
SheynerO., HainesJ., JhaS., LippmannR. and WingJ., Automated generation and analysis of attack graphs, 2002, pp. 273–284.
31.
van BenthemJ., An Essay on Sabotage and Obstruction, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 268–276.
32.
ZhangY. and MalacariaP., Bayesian stackelberg games for cyber-security decision support, Decis Support Syst148 (2021), 113599.
