  This paper is concerned with the synthesis of strategies in network systems
with active cyber deception. Active deception in a network employs decoy
systems and other defenses to conduct defensive planning against the intrusion
of malicious attackers who have been confirmed by sensing systems. In this
setting, the defender's objective is to ensure the satisfaction of security
properties specified in temporal logic formulas. We formulate the problem of
deceptive planning with decoy systems and other defenses as a two-player games
with asymmetrical information and Boolean payoffs in temporal logic. We use
level-2 hypergame with temporal logic objectives to capture the
incomplete/incorrect knowledge of the attacker about the network system as a
payoff misperception. The true payoff function is private information of the
defender. Then, we extend the solution concepts of $omega$-regular games to
analyze the attacker's rational strategy given her incomplete information. By
generalizing the solution of level-2 hypergame in the normal form to extensive
form, we extend the solutions of games with safe temporal logic objectives to
decide whether the defender can ensure security properties to be satisfied with
probability one, given any possible strategy that is perceived to be rational
by the attacker. Further, we use the solution of games with co-safe
(reachability) temporal logic objectives to determine whether the defender can
engage the attacker, by directing the attacker to a high-fidelity honeypot. The
effectiveness of the proposed synthesis methods is illustrated with synthetic
network systems with honeypots.
