  Opacity is an important information-flow security property that characterizes
the plausible deniability of a dynamic system for its "secret" against
eavesdropping attacks. As an information-flow property, the underlying
observation model is the key in the modeling and analysis of opacity. In this
paper, we investigate the verification of current-state opacity for
discrete-event systems under Orwellian-type observations, i.e., the system is
allowed to re-interpret the observation of an event based on its future suffix.
First, we propose a new Orwellian-type observation model called the dynamic
information release mechanism (DIRM). In the DIRM, when to release previous
"hold on" events is state-dependent. Then we propose a new definition of
opacity based on the notion of history-equivalence rather than the standard
projection-equivalence. This definition is more suitable for observations that
are not prefix-closed. Finally, we show that by constructing a new structure
called the DIRM-observer, current-state opacity can be effectively verified
under the DIRM. Computational complexity analysis as well as illustrative
examples for the proposed approach are also provided. Compared with the
existing Orwellian-type observation model, the proposed framework is more
general in the sense that the information-release-mechanism is state-dependent
and the corresponding definition of opacity is more suitable for
non-prefix-closed observations.
