Synthesis of Deceptive Cyberdefense with Temporal Logic Constraints

The design of provably correct systems from temporal logic specifications employs reactive synthesis, which models the interaction between the system and its dynamic environment as a two-player zero-sum game with complete information. However, most situations encountered in cybersecurity applications are characterized by asymmetric incomplete information: the adversary may not know the exact network configuration and the defender does not know the adversary’s capabilities or intention. In this context, we discuss the recent developments in hypergame theory and omega-regular games with incomplete information which show that the solution concepts of this class of games lead to deceptive strategies that are surely or almost-surely (with probability one) guaranteed to satisfy a given security specification in Linear Temporal Logic (LTL).