A Framework for Current-State Opacity under Dynamic Information Release Mechanism

TL;DR

This paper introduces a new framework for verifying current-state opacity in discrete-event systems under a dynamic, state-dependent information release mechanism, enhancing analysis of systems with non-prefix-closed observations.

Contribution

It proposes a novel Orwellian-type observation model called DIRM and a new opacity definition based on history-equivalence, enabling effective verification under dynamic information release.

Findings

The DIRM model generalizes existing Orwellian observation models.

A new DIRM-observer structure allows effective opacity verification.

The approach handles non-prefix-closed observations more suitably.

Abstract

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.