# Security-Aware Synthesis Using Delayed-Action Games

## TL;DR

This paper introduces delayed-action games (DAGs), a new formalism that models hidden-information games as stochastic multiplayer games, enabling efficient security-aware strategy synthesis for multi-agent systems under stealthy attacks.

## Contribution

The paper proposes DAGs to simulate hidden-information games within SMGs, allowing the use of existing model checkers and enabling parallel exploration for security strategy synthesis.

## Key findings

- DAGs effectively model hidden information in multi-agent systems.
- Parallel decomposition reduces model checking time.
- Framework successfully applied to UAV security under stealthy attacks.

## Abstract

Stochastic multiplayer games (SMGs) have gained attention in the field of strategy synthesis for multi-agent reactive systems. However, standard SMGs are limited to modeling systems where all agents have full knowledge of the state of the game. In this paper, we introduce delayed-action games (DAGs) formalism that simulates hidden-information games (HIGs) as SMGs, where hidden information is captured by delaying a player's actions. The elimination of private variables enables the usage of SMG off-the-shelf model checkers to implement HIGs. Furthermore, we demonstrate how a DAG can be decomposed into subgames that can be independently explored, utilizing parallel computation to reduce the model checking time, while alleviating the state space explosion problem that SMGs are notorious for. In addition, we propose a DAG-based framework for strategy synthesis and analysis. Finally, we demonstrate applicability of the DAG-based synthesis framework on a case study of a human-on-the-loop unmanned-aerial vehicle system under stealthy attacks, where the proposed framework is used to formally model, analyze and synthesize security-aware strategies for the system.