  We study in depth the class of games with opacity condition, which are
two-player games with imperfect information in which one of the players only
has imperfect information, and where the winning condition relies on the
information he has along the play. Those games are relevant for security
aspects of computing systems: a play is opaque whenever the player who has
imperfect information never "knows" for sure that the current position is one
of the distinguished "secret" positions. We study the problems of deciding the
existence of a winning strategy for each player, and we call them the
opacity-violate problem and the opacity-guarantee problem. Focusing on the
player with perfect information is new in the field of games with
imperfect-information because when considering classical winning conditions it
amounts to solving the underlying perfect-information game. We establish the
EXPTIME-completeness of both above-mentioned problems, showing that our winning
condition brings a gap of complexity for the player with perfect information,
and we exhibit the relevant opacity-verify problem, which noticeably
generalizes approaches considered in the literature for opacity analysis in
discrete-event systems. In the case of blindfold games, this problem relates to
the two initial ones, yielding the determinacy of blindfold games with opacity
condition and the PSPACE-completeness of the three problems.

Computer Science and Game Theory