  This paper investigates an important informationflow security property called
opacity in partially-observed discrete-event systems. We consider the presence
of a passive intruder (eavesdropper) that knows the dynamic model of the system
and can use the generated information-flow to infer some "secret" of the
system. A system is said to be opaque if it always holds the plausible
deniability for its secret. Existing notions of opacity only consider secret
either as currently visiting some secret states or as having visited some
secret states in the past. In this paper, we investigate information-flow
security from a new angle by considering the secret of the system as the
intention to execute some particular behavior of importance in the future. To
this end, we propose a new class of opacity called pre-opacity that
characterizes whether or not the intruder can predict the visit of secret
states a certain number of steps ahead before the system actually does so.
Depending the prediction task of the intruder, we propose two specific kinds of
pre-opacity called K-step instant pre-opacity and K-step trajectory pre-opacity
to specify this concept. For each notion of pre-opacity, we provide a necessary
and sufficient condition as well as an effective verification algorithm. The
complexity for the verification of pre-opacity is exponential in the size of
the system as we show that pre-opacity is inherently PSPACE-hard. Finally, we
generalize our setting to the case where the secret intention of the system is
modeled as executing a particular sequence of events rather than visiting a
secret state.
