← All opacity pages Search by tag →

Opacity of Classical Systems

run with secret cover run (no secret) a secret b c a b c
Two runs differ on whether a secret event occurred, yet produce the same observable event sequence a·b·c. No clocks, no probabilities, one fixed observer: the system is opaque with respect to this secret if a cover run like this always exists.
● Scope of this page

This page covers the setting where the field started: discrete event systems modeled as finite automata, labeled transition systems, or Petri nets, with no notion of real time, no randomness, and a single observer watching a fixed set of observable events.

This is the setting the foundational definitions were built for, and it's where the largest share of the opacity literature still sits: the core notions (language-based, current-state, initial-state, K-step, infinite-step opacity), the algorithms that verify them, and the mechanisms (supervisory control, insertion and edit functions, dynamic masks) that enforce opacity on a system that doesn't already have it.

A

Notions & Verification

The core literature on opacity for finite-state systems: articles that introduce a notion of opacity, study its decidability or complexity, or develop an algorithm to verify it. Most use plain finite automata as the underlying model and are grouped by what they contribute; a separate group uses Petri nets, which raise their own decidability questions distinct from automata.

Core notions & definitions

Articles that define opacity or a closely related notion: state-based and language-based definitions on automata and labeled transition systems, a notion of secrecy together with a weaker version, and opacity for cryptographic protocols.

  • Using Unification for Opacity Properties
    Laurent Mazaré · WITS 2004 (Workshop on Issues in the Theory of Security), pp. 165–176 · technical report PDF
    Opacity defined for cryptographic protocols rather than for discrete-event systems.
    classical · finite-automata · opacity
    Show abstractHide abstract
    The most studied property, secrecy, is not always sufficient to prove the security of a protocol. Other properties such as anonymity, privacy or opacity could be useful. Here, we give a simple definition of opacity by looking at the possible traces of the protocol. Our approach draws on a new property over messages called similarity. Then, using rewriting methods close to those used in unification, we demonstrate the decidability of our opacity property. This is only achieved in the case of atomic keys using a method called Key Quantification.
  • Notions of Security and Opacity in Discrete Event Systems
    Anooshiravan Saboori, Christoforos N. Hadjicostis · 46th IEEE Conference on Decision and Control (CDC 2007), pp. 5056–5061 · IEEE Xplore
    Source of current-state opacity, here with a K-step strengthening.
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we follow a state-based approach to extend the notion of opacity in computer security to discrete event systems. A system is (S, P)-opaque if the evolution of its true state through a set of secret states S remains opaque to an observer who is observing activity in the system through the projection map P. In other words, based on observations through the mapping P, the observer is never certain that the current state of the system is within the set of secret states S. We also introduce the stronger notion of (S,P, K)-opacity which requires opacity to remain true for K observations following the departure of the system's state from the set S. We show that the state-based definition of opacity enables the use of observer constructions for verification purposes. In particular, the verification of (S,P, K)-opacity is accomplished via an observer with K-delay which is constructed to capture state estimates with K-delay. These are the estimates of the state of the system K observations ago and are consistent with all observations (including the last K observations). We also analyze the properties and complexity of the observer with K-delay.
  • Opacity Generalised to Transition Systems
    Jeremy W. Bryans, Maciej Koutny, Laurent Mazaré, Peter Y. A. Ryan · International Journal of Information Security, 7(6), pp. 421–435, 2008 · doi.org/10.1007/s10207-008-0058-x
    classical · finite-automata · opacity
    Show abstractHide abstract
    Recently, opacity has proved a promising technique for describing security properties. Much of the work has been couched in terms of Petri nets. Here, we extend the notion of opacity to the model of labelled transition systems and generalise opacity in order to better represent concepts from the literature on information flow. In particular, we establish links between opacity and the information flow concepts of anonymity and non-inference. We also investigate ways of verifying opacity when working with Petri nets. Our work is illustrated by two examples, one describing anonymity in a commercial context, and the other modelling requirements upon a simple voting system.
  • Verification and Synthesis for Secrecy in Discrete-Event Systems
    Shigemasa Takai, Ratnesh Kumar · 2009 American Control Conference (ACC), pp. 4741–4746 · doi.org/10.1109/ACC.2009.5160162
    classical · finite-automata · opacity
    Show abstractHide abstract
    Keeping a property of system behaviors secret from an observer (who has a partial observation of any executed behavior) requires that the execution of any property-satisfying or property-violating behavior must not become known to the observer. When an observer does not know the exact behaviors of a system it observes, a weaker notion of secrecy can be defined, which we introduce in this paper. We present an algorithm for verifying the properties of secrecy as well as its weaker version. When a given system does not possess a secrecy property, we consider restricting the behaviors of the system by means of supervisory control so as to ensure that the controlled system satisfies the desired secrecy property. We show the existence of a maximally permissive supervisor to ensure secrecy or its weaker version, and present algorithms for their synthesis.
  • Opacity of Discrete Event Systems and Its Applications
    Feng Lin · Automatica, 47(3), pp. 496–503, 2011 · doi.org/10.1016/j.automatica.2011.01.002
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we investigate opacity of discrete event systems. We define two types of opacities: strong opacity and weak opacity. Given a general observation mapping, a language is strongly opaque if all strings in the language are confused with some strings in another language and it is weakly opaque if some strings in the language are confused with some strings in another language. We show that security and privacy of computer systems and communication protocols can be investigated in terms of opacity. In particular, two important properties in security and privacy, namely anonymity and secrecy, can be studied as special cases of opacity. We also show that by properly specifying the languages and the observation mapping, three important properties of discrete event systems, namely observability, diagnosability, and detectability, can all be reformulated as opacity. Thus, opacity has a wide range of applications. Also in this paper we provide algorithms for checking strong opacity and weak opacity for systems described by regular languages and having a generalized projection as the observation mapping.

Verification & complexity

Algorithms and complexity results for verifying the standard notions (current-state, initial-state, K-step, infinite-step and initial-and-final-state opacity): observer-based and compositional constructions, structural restrictions that make verification easier, lower bounds, and benchmarks.

  • Verification of K-Step Opacity and Analysis of Its Complexity
    Anooshiravan Saboori, Christoforos N. Hadjicostis · IEEE Transactions on Automation Science and Engineering, 8(3), pp. 549–559, 2011 · doi.org/10.1109/TASE.2011.2106775
    classical · finite-automata · opacity
    Show abstractHide abstract
    Motivated by security and privacy considerations in a variety of applications of discrete event systems, we describe and analyze the computational complexity required for verifying the notion of K-step opacity for systems that are modeled as nondeterministic finite automata with partial observation on their transitions. Specifically, a system is K-step opaque if, at any specific point within the last K observations, the entrance of the system state to a given set of secret states remains opaque (uncertain) to an intruder who has complete knowledge of the system model and observes system activity through some natural projection map. We provide two methods for verifying K-step opacity using two different state estimator constructions, and analyze the computational complexity of both.
  • Verification of Infinite-Step Opacity and Complexity Considerations
    Anooshiravan Saboori, Christoforos N. Hadjicostis · IEEE Transactions on Automatic Control, 57(5), pp. 1265–1269, 2012 · doi.org/10.1109/TAC.2011.2173774
    classical · finite-automata · opacity
    Show abstractHide abstract
    We describe and analyze the complexity of verifying the notion of infinite-step opacity in systems that are modeled as non-deterministic finite automata with partial observation on their transitions. Specifically, a system is infinite-step opaque if the entrance of the system state, at any particular instant, to a set of secret states remains opaque (uncertain), for the length of the system operation, to an intruder who observes system activity through some projection map. Infinite-step opacity can be used to characterize the security requirements in many applications, including encryption using pseudo-random generators, coverage properties in sensor networks, and anonymity requirements in protocols for web transactions. We show that infinite-step opacity can be verified via the construction of a set of appropriate initial state estimators and provide illustrative examples. We also establish that the verification of infinite-step opacity is a PSPACE-hard problem.
  • Verification of Initial-State Opacity in Security Applications of Discrete Event Systems
    Anooshiravan Saboori, Christoforos N. Hadjicostis · Information Sciences, 246, pp. 115–132, 2013 (journal version; conference version: WODES 2008, pp. 328–333) · doi.org/10.1016/j.ins.2013.05.033
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we formulate and analyze methodologies for verifying the notion of initial-state opacity in discrete event systems that are modeled as non-deterministic finite automata with partial observation on their transitions. A system is initial-state opaque if the membership of its true initial state to a set of secret states remains opaque (i.e., uncertain) to an intruder who observes system activity through some projection map. Initial-state opacity can be used to characterize security requirements in a variety of applications, including tracking problems in sensor networks. In order to model and analyze the intruder capabilities regarding initial-state opacity, we first address the initial-state estimation problem in a non-deterministic finite automaton via the construction of an initial-state estimator. We analyze the properties and complexity of the initial-state estimator, and show how the complexity of the verification method can be greatly reduced in the special case when the set of secret states is invariant. We also establish that the verification of initial-state opacity is a PSPACE-complete problem.
  • A New Approach for the Verification of Infinite-Step and K-Step Opacity Using Two-Way Observers
    Xiang Yin, Stéphane Lafortune · Automatica, 80, pp. 162–171, 2017 · doi.org/10.1016/j.automatica.2017.02.037
    classical · finite-automata · opacity
    Show abstractHide abstract
    In the context of security analysis for information flow properties, where a potentially malicious observer (intruder) tracks the observed behavior of a given system, infinite-step opacity (respectively, K-step opacity) holds if the intruder can never determine for sure that the system was in a secret state for any instant within infinite steps (respectively, K steps) prior to that particular instant. We present new algorithms for the verification of the properties of infinite-step opacity and K-step opacity for partially-observed discrete event systems modeled as finite-state automata. Our new algorithms are based on a novel separation principle for state estimates that characterizes the information dependence in opacity verification problems, and they have lower computational complexity than previously-proposed ones in the literature. Specifically, we propose a new information structure, called the two-way observer, that is used for the verification of infinite-step and K-step opacity. Based on the two-way observer, a new upper bound for the delay in K-step opacity is derived, which also improves previously-known results.
  • Incremental Observer Reduction Applied to Opacity Verification and Synthesis
    Mona Noori-Hosseini, Bengt Lennartson, Christoforos N. Hadjicostis · arXiv:1812.08083, 2018 (preliminary version: WODES 2018) · arXiv:1812.08083
    classical · finite-automata · opacity
    Show abstractHide abstract
    With the proliferation of communication networks and mobile devices, the privacy and security concerns on their information flow are raised. Given a critical system that may leak confidential information, the problem consists of verifying and also enforcing opacity by designing supervisors, to conceal confidential information from unauthorized persons. To find out what the intruder sees, it is required to construct an observer of the system. In this paper, we consider incremental observer generation of modular systems, for verification and enforcement of current state opacity. The synchronization of the subsystems generate a large state space. Moreover, the observer generation with exponential complexity adds even larger state space. To tackle the complexity problem, we prove that observer generation can be done locally before synchronizing the subsystems. The incremental local observer generation along with an abstraction method lead to a significant state space reduction compared to traditional monolithic methods. The existence of shared unobservable events is also considered in the incremental approach. Moreover, we present an illustrative example, where the results of verification and enforcement of current state opacity are shown on a modular multiple floor/elevator building with an intruder. Furthermore, we extend the current state opacity, current state anonymity, and language based opacity formulations for verification of modular systems.
  • Compositional Visible Bisimulation Abstraction Applied to Opacity Verification
    Mona Noori-Hosseini, Bengt Lennartson, Christoforos N. Hadjicostis · IFAC-PapersOnLine, 51(7), pp. 434–441, 2018 (14th IFAC Workshop on Discrete Event Systems, WODES 2018) · doi.org/10.1016/j.ifacol.2018.06.337
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, an alternative equivalence based definition of bisimulation is proposed, called visible bisimulation equivalence. It includes both state and transition labels and therefore unifies stuttering and branching bisimulation. Furthermore, it is equivalent to a temporal logic called ECTL*, where CTL* is extended with events. The presented bisimulation abstraction is applied to a set of synchronized submodels, where local events are identified incrementally and abstracted after each synchronization. Since the bisimulation reduction is applied after each synchronization, a significant part of the state space explosion in ordinary synchronization is avoided. This compositional abstraction is used for opacity verification, where it is shown that local observers can be generated before they are synchronized, a key factor to be able to apply compositional opacity verification. The efficiency of this method is illustrated on a modular opacity problem with mutual exclusion of moving agents.
  • Comments on "A New Approach for the Verification of Infinite-Step and K-Step Opacity Using Two-Way Observers"
    Hao Lan, Yin Tong, Jin Guo, Alessandro Giua · Automatica, 122, article 109290, 2020 · doi.org/10.1016/j.automatica.2020.109290
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this note, we point out that the observer of a given discrete event system and the observer of the reversed system can be used together to verify both infinite-step opacity and K-step opacity without constructing the two-way observer in Yin and Lafortune (2017). In this way, the complexity of checking the two opacity properties can be reduced.
  • On Opacity Verification for Discrete-Event Systems
    Jiří Balun, Tomáš Masopust · IFAC-PapersOnLine, 53(2), pp. 2075–2080, 2020 (21st IFAC World Congress) · doi.org/10.1016/j.ifacol.2020.12.2524 · preprint: arXiv:1912.07314
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is an information flow property characterizing whether a system reveals its secret to an intruder. Verification of opacity for discrete-event systems modeled by automata is in general a hard problem. We discuss the question whether there are structural restrictions on the system models for which the opacity verification is tractable. We consider two kinds of automata models: (i) acyclic automata, and (ii) automata where all cycles are only in the form of self-loops. In some sense, these models are the simplest models of (deadlock-free) systems. Although the expressivity of such systems is weaker than the expressivity of linear temporal logic, we show that the opacity verification for these systems is still hard.
  • K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations
    Jiří Balun, Tomáš Masopust · arXiv:2109.02158, 2021 · arXiv:2109.02158
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has a limited observation of its behavior. Several notions of opacity have been studied, including current-state opacity, K-step opacity, and infinite-step opacity. We study K-step opacity that generalizes both current-state opacity and infinite-step opacity, and asks whether the intruder cannot decide, at any time, whether or when the system was in a secret state during the last K observable steps. We design a new algorithm deciding K-step opacity the complexity of which is lower than that of existing algorithms and that does not depend on K. We then compare K-step opacity with other opacity notions and provide new transformations among the notions that do not use states that are neither secret nor non-secret (neutral states) and that are polynomial with respect to both the size of the system and the binary encoding of K.
  • Reduced-Complexity Verification for K-Step and Infinite-Step Opacity in Discrete Event Systems
    Xiaoyan Li, Christoforos N. Hadjicostis, Zhiwu Li · arXiv:2310.11825, 2023 · arXiv:2310.11825
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a property that captures security concerns in cyber-physical systems and its verification plays a significant role. This paper investigates the verifications of K-step and infinite-step weak and strong opacity for partially observed nondeterministic finite state automata. K-step weak opacity is checked by constructing, for some states in the observer, appropriate state-trees, to propose a necessary and sufficient condition. Based on the relation between K-step weak and infinite-step weak opacity, a condition that determines when a system is not infinite-step weak opaque is presented. Regarding K-step and infinite-step strong opacity, we develop a secret-involved projected automaton, based on which we construct secret-unvisited state trees to derive a necessary and sufficient condition for K-step strong opacity. Furthermore, an algorithm is reported to compute a verifier that can be used to obtain a necessary and sufficient condition for infinite-step strong opacity. It is argued that, in some particular cases, the proposed methods achieve reduced complexity compared with the state of the art.
  • Speed Me Up If You Can: Conditional Lower Bounds on Opacity Verification
    Jiří Balun, Tomáš Masopust, Petr Osička · MFCS 2023 (Mathematical Foundations of Computer Science), LIPIcs vol. 272, pp. 16:1–16:15 · doi.org/10.4230/LIPIcs.MFCS.2023.16 · preprint: arXiv:2304.09920
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system’s behaviour can ascertain some "secret" information of the system. Deciding opacity is a PSpace-complete problem, and hence there are no polynomial-time algorithms to verify opacity under the assumption that PSpace differs from PTime. This assumption, however, gives rise to a question whether the existing exponential-time algorithms are the best possible or whether there are faster, sub-exponential-time algorithms. We show that under the (Strong) Exponential Time Hypothesis, there are no algorithms that would be significantly faster than the existing algorithms. As a by-product, we obtained a new conditional lower bound on the time complexity of deciding universality (and therefore also inclusion and equivalence) for nondeterministic finite automata.
  • Verifying Weak and Strong k-Step Opacity in Discrete-Event Systems
    Jiří Balun, Tomáš Masopust · Automatica, 155, article 111153, 2023 · doi.org/10.1016/j.automatica.2023.111153 · conference precursor: “On Verification of Weak and Strong k-Step Opacity for Discrete-Event Systems”, IFAC-PapersOnLine, 55(28), pp. 108–113, 2022 (WODES 2022) · doi.org/10.1016/j.ifacol.2022.10.331 · preprint: arXiv:2204.01286
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is an important system-theoretic property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has only limited observations of its behavior. Several notions of opacity have been discussed in the literature, including current-state opacity, k-step opacity, and infinite-step opacity. We investigate weak and strong k-step opacity, the notions that generalize both current-state opacity and infinite-step opacity, and ask whether the intruder is not able to decide, at any time instant, when respectively whether the system was in a secret state during the last k observable steps. We design a new algorithm verifying weak k-step opacity, the complexity of which is lower than the complexity of existing algorithms and does not depend on the parameter k, and show how to use it to verify strong k-step opacity by reducing strong k-step opacity to weak k-step opacity. The complexity of the resulting algorithm is again better than the complexity of existing algorithms and does not depend on the parameter k.
  • K-Step Opacity Benchmarks for Discrete Event Systems
    Jiří Balun, Tomáš Masopust, Petr Osička · unpublished manuscript / benchmark resource, 2024, referenced at apollo.inf.upol.cz · apollo.inf.upol.cz
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a generic framework expressing secret in discrete-event systems. Many notions of opacity have been discussed in the literature, including current-state opacity (CSO), k-step opacity (k-SO), and strong k-step opacity (k-SSO). We design new algorithms for the verification of k-SO and k-SSO based on reductions of k-SO to CSO and of k-SSO to k-SO, respectively, and experimentally compare their performance with the existing algorithms. In particular, for CSO, we use the classical algorithm based on the observer construction and an algorithm based on a reduction to the antichain-based language inclusion. For k-SO, we compare our algorithms with the two-way observer of Yin and Lafortune, with the reduction-based algorithm of Wintenberg et al., and with our projected-automata-base algorithm. For k-SSO, we compare our algorithms with the reduction-based algorithm of Wintenberg et al. and with the algorithm of Han et al.. For the comparisons, we use extensive benchmarks with almost twelve thousand instances based on real data.
  • On Algorithms Verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison
    Tomáš Masopust, Petr Osička · Automatica, 174, article 112171, 2025 · doi.org/10.1016/j.automatica.2025.112171 · preprint: arXiv:2402.17000
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a general framework modeling security properties of systems interacting with a passive attacker. Initial-and-final-state opacity (IFO) generalizes the classical notions of opacity, such as current-state opacity and initial-state opacity. In IFO, the secret is whether the system evolved from a given initial state to a given final state or not. There are two algorithms for IFO verification. One arises from a trellis-based state estimator, which builds a semigroup of binary relations generated by the events of the automaton, and the other is based on the reduction to language inclusion. The time complexity of both algorithms is bounded by a super-exponential function, and it is a challenging open problem to find a faster algorithm or to show that no faster algorithm exists. We discuss the lower-bound time complexity for both general and special cases, and use extensive benchmarks to compare the existing algorithms.

Comparisons & frameworks

Relations between the standard notions (transformations from one notion to another, comparisons) and general frameworks that unify them, including a logic for specifying opacity and a uniform treatment of opacity with other observational properties such as diagnosability and detectability.

  • Comparative Analysis of Related Notions of Opacity in Centralized and Coordinated Architectures
    Yi-Chin Wu, Stéphane Lafortune · Discrete Event Dynamic Systems, 23(3), pp. 307–339, 2013 · doi.org/10.1007/s10626-012-0145-z
    Its transformations among the opacity notions are extended by the Balun and Masopust paper on this page.
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a confidentiality property that captures whether an intruder can infer a “secret” of a system based on its observation of the system behavior and its knowledge of the system’s structure. In this paper, we study four notions of opacity: language-based opacity, initial-state opacity, current-state opacity, and initial-and-final-state opacity. Initial-and-final-state opacity is a new opacity property introduced in this paper, motivated by secrecy considerations in anonymous network communications; the other three opacity properties have been studied in prior work. We investigate the relationships between these opacity properties. In this regard, a complete set of transformation algorithms among the four notions is provided. We also propose a new, more efficient test for initial-state opacity based on the use of reversed automata, and present a trellis-based test for the new property of initial-and-final state opacity. We then study the notions of initial-state opacity, current-state opacity, and initial-and-final-state opacity in the context of a new coordinated architecture where two intruders work as a team in order to infer the secret. In this architecture, the intruders have the capability of combining their respective state estimates at a coordinating node. In each case, a characterization of the corresponding notion of “joint opacity” and an algorithmic procedure for its verification are provided.
  • Comparing the Notions of Opacity for Discrete-Event Systems
    Jiří Balun, Tomáš Masopust · Discrete Event Dynamic Systems, 31(4), pp. 553–582, 2021 · preprint: arXiv:2102.02889 · doi.org/10.1007/s10626-021-00344-2
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is an information flow property characterizing whether a system reveals its secret to a passive observer. Several notions of opacity have been introduced in the literature. We study the notions of language-based opacity, current-state opacity, initial-state opacity, initial-and-final-state opacity, K-step opacity, and infinite-step opacity. Comparing the notions is a natural question that has been investigated and summarized by Wu and Lafortune, who provided transformations among current-state opacity, initial-and-final-state opacity, and language-based opacity, and, for prefix-closed languages, also between language-based opacity and initial-state opacity. We extend these results by showing that all the discussed notions of opacity are transformable to each other. Besides a deeper insight into the differences among the notions, the transformations have applications in complexity results. In particular, the transformations are computable in polynomial time and preserve the number of observable events and determinism, and hence the computational complexities of the verification of the notions coincide. We provide a complete and improved complexity picture of the verification of the discussed notions of opacity, and improve the algorithmic complexity of deciding language-based opacity, infinite-step opacity, and K-step opacity.
  • On Transformations among Opacity Notions
    Jiří Balun, Tomáš Masopust · 2022 IEEE International Conference on Systems, Man, and Cybernetics (SMC 2022), Prague, pp. 3012–3017 · doi.org/10.1109/SMC53654.2022.9945608
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a property asking whether a system may reveal its secret to a passive observer who knows the structure of the system but has only limited observations of its behavior. Several notions of opacity have been studied. Similarities among the opacity notions have been investigated via transformations, which have many potential applications. We investigate K-step opacity (K-SO), a notion that generalizes both current-state opacity and infinite-step opacity, and asks whether the intruder cannot decide, at any instant, whether or when the system was in a secret state during the last K observable steps. We provide new polynomial-time transformations among K-SO and other opacity notions. Our results lead, among others, to the general solution of an open problem concerning the computational complexity of the verification of K-SO.
  • A General Language-Based Framework for Specifying and Verifying Notions of Opacity
    Andrew Wintenberg, Matthew Blischke, Stéphane Lafortune, Necmiye Ozay · Discrete Event Dynamic Systems, 32(2), pp. 253–289, 2022 · doi.org/10.1007/s10626-021-00357-x · preprint: arXiv:2103.10501
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is an information flow property that captures the notion of plausible deniability in dynamic systems, that is whether an intruder can deduce that “secret” behavior has occurred. In this paper we provide a general framework of opacity to unify the many existing notions of opacity that exist for discrete event systems. We use this framework to discuss language-based and state-based notions of opacity over automata. We present several methods for language-based opacity verification, and a general approach to transform state-based notions into language-based ones. We demonstrate this approach for current-state and initial-state opacity, unifying existing results. We then investigate the notions of K-step opacity. We provide a language-based view of K-step opacity encompassing two existing notions and two new ones. We then analyze the corresponding language-based verification methods both formally and with numerical examples. In each case, the proposed methods offer significant reductions in runtime and space complexity.
  • Verifying Opacity Properties in Security Systems
    Chunyan Mu, David Clark · IEEE Transactions on Dependable and Secure Computing, 20(2), pp. 1450–1460, 2023 · doi.org/10.1109/TDSC.2022.3155323
    classical · finite-automata · opacity · stochastic
    Show abstractHide abstract
    We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL, for straightforwardly expressing such properties in systems that can be modelled as partially observable labelled transition systems. We develop verification techniques for analysing property opacity with respect to observation notions. Adding a probabilistic operator to the specification language enables quantitative analysis and verification. This analysis is implemented as an extension to the PRISM model checker and illustrated via a number of examples. Finally, an alternative approach to quantifying the opacity property based on entropy is sketched.
  • A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems
    Jianing Zhao, Xiang Yin, Shaoyuan Li · IEEE Transactions on Automatic Control, 69(7), pp. 4710–4717, 2024 · doi.org/10.1109/TAC.2024.3355378
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this article, we investigate property verification problems in partially-observed discrete-event systems (DES). Particularly, we are interested in verifying observational properties that are related to the information-flow of the system. Observational properties considered here include diagnosability, predictability, detectability, and opacity, which have drawn considerable attentions in the literature. However, in contrast to existing results, where different verification procedures are developed for different properties case by case, in this work, we provide a unified framework for verifying all these properties by reducing each of them as an instance of HyperLTL model checking. Our approach is based on the construction of a Kripke structure that effectively captures the issue of unobservability as well as the finite string semantics in partially-observed DES so that HyperLTL model checking techniques can be suitably applied. Then for each observational property considered, we explicitly provide the HyperLTL formula to be checked over the Kripke structure for the purpose of verification. Our approach is uniform in the sense that all different properties can be verified with the same model checking engine and also brings new insights for classifying observational properties in terms of their verification complexity. Numerical experiments are conducted, which show that our framework is computationally more efficient for verifying properties involving quantifier alternations, such as opacity, compared with the standard subset-based approaches.

Strong opacity

Stronger versions of the standard notions (current-state, initial-state, K-step, infinite-step and initial-and-final-state opacity), with their verification algorithms and, for some of them, their enforcement.

  • Verification of Strong K-Step Opacity for Discrete-Event Systems
    Xiaoguang Han, Kuize Zhang, Zhiwu Li · 2022 IEEE 61st Conference on Decision and Control (CDC), pp. 4250–4255 · doi.org/10.1109/CDC51059.2022.9993023 · preprint: arXiv:2204.04698
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we revisit the verification of strong K-step opacity (K-SSO) for partially-observed discrete-event systems modeled as nondeterministic finite-state automata. As a stronger version of the standard K-step opacity, K-SSO requires that an intruder cannot make sure whether or not a secret state has been visited within the last K observable steps. To efficiently verify K-SSO, we propose a new concurrent-composition structure, which is a variant of our previously-proposed one. Based on this new structure, we design an algorithm for deciding K-SSO and prove that the proposed algorithm not only reduces the time complexity of the existing algorithms, but also does not depend on the value of K. Furthermore, a new upper bound on the value of K in K-SSO is derived, which also reduces the existing upper bound on K in the literature. Finally, we illustrate the proposed algorithm by a simple example.
  • Strong Current-State and Initial-State Opacity of Discrete-Event Systems
    Xiaoguang Han, Kuize Zhang, Jiahui Zhang, Zhiwu Li, Zengqiang Chen · Automatica, 148, article 110756, 2023 · arXiv:2109.05475 · doi.org/10.1016/j.automatica.2022.110756
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity, as an important property in information-flow security, characterizes the ability of a system to keep some secret information from an intruder. In discrete-event systems, based on a standard setting in which an intruder has the complete knowledge of the system’s structure, the standard versions of current-state opacity and initial-state opacity cannot perfectly characterize higher-level privacy requirements. To overcome such a limitation, in this paper we propose two stronger versions of opacity called strong current-state opacity and strong initial-state opacity for partially-observed nondeterministic finite-state automata. Strong current-state (resp., initial-state) opacity describes that for each run of a system ending (resp., starting) at a secret state, there exists a non-secret run whose observation is the same as that of the previous run. Then we propose an information structure using a novel concurrent-composition technique to verify strong current-state opacity and strong initial-state opacity, which has time complexity O((|Σ||X|2 + |Σo||X∖XS|2(1 + |Σuo|))2|X∖XS|), where |X| (resp., |Σ|, |Σo|, |Σuo|, |X∖XS|) is the number of states (resp., events, observable events, unobservable events, non-secret states) of an automaton. Finally, the proposed information structure is also used to check strong infinite-step opacity, which has lower time complexity than the previous one in the literature.
  • Always Guarding You: Strong Initial-and-Final-State Opacity of Discrete-Event Systems
    Shaowen Miao, Aiwen Lai, Jan Komenda · Automatica, 173, article 112085, 2025 · doi.org/10.1016/j.automatica.2024.112085
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a security property of discrete-event systems that specifies whether the secret can be concealed from an external intruder. In this paper, we proposed two advanced variants of initial-and-final-state opacity, namely partially strong initial-and-final-state opacity (PSIFO) and strong initial-and-final-state opacity (SIFO), which impose more stringent security requirements, for discrete-event systems modeled by nondeterministic finite-state automata. SIFO (resp. PSIFO) is a property that for each path between a given secret state pair, there exists a strongly non-secret-pair path (resp. non-secret-pair path), with the same observation as that path. In other words, the strong version of initial-and-final-state opacity requires the existence of at least one path always guarding the secret. Furthermore, we conduct an analysis of the reductions from strong current-state opacity and initial-state opacity to PSIFO. Finally, two concurrent composition-based information structures are proposed to verify these two properties, the size of which grows exponentially with the number of states of the original system.
  • Verification and Enforcement of Strong State-Based Opacity for Discrete-Event Systems
    Xiaoguang Han, Kuize Zhang, Zhiwu Li · Automatica, 193, article 113237, 2026 · doi.org/10.1016/j.automatica.2026.113237 · preprint: arXiv:2401.10363
    Builds on two earlier concurrent-composition structures for strong opacity and adds enforcement by disabling controllable transitions.
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we investigate the verification and enforcement of strong state-based opacity (SBO) in discrete-event systems modeled by partially-observed (nondeterministic) finite-state automata, including strong K-step opacity (K-SSO), strong current-state opacity (SCSO), strong initial-state opacity (SISO), and strong infinite-step opacity (Inf-SSO). They are stronger versions of four widely-studied standard opacity notions, respectively. We first propose a new notion of K-SSO and construct a concurrent-composition structure to verify it efficiently. Based on this structure, a verification algorithm is designed and an upper bound on K is derived for the newly proposed K-SSO notion. Second, we introduce a new opacity-enforcement mechanism independent of assumptions. Its basic philosophy is to select a subset of controllable transitions to disable prior to the execution of an original system, so as to eliminate all runs that violate a notion of strong SBO of interest. Accordingly, the algorithms for enforcing the four notions of strong SBO are designed using the two reported concurrent-composition structures. In particular, the designed algorithm for enforcing Inf-SSO has lower time complexity than the existing one in the literature. Finally, we illustrate the designed algorithms using examples.

Observation & system models

Opacity when the observation is not a fixed projection of the events (observations reinterpreted in light of the future, nondeterministic observation mechanisms, state or output observations) and for richer models such as extended finite automata with event parameters or switching output automata.

  • Opacity with Orwellian Observers and Intransitive Non-Interference
    John Mullins, Moez Yeddes · 12th IFAC International Workshop on Discrete Event Systems (WODES 2014), pp. 344–349 · doi.org/10.3182/20140514-3-FR-4046.00016 · preprint: arXiv:1312.6426
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a general behavioural security scheme flexible enough to account for several specific properties. Some secret set of behaviors of a system is opaque if a passive attacker can never tell whether the observed behavior is a secret one or not. Instead of considering the case of static observability where the set of observable events is fixed off-line or dynamic observability where the set of observable events changes over time depending on the history of the trace, we consider Orwellian partial observability where unobservable events are not revealed unless a downgrading event occurs in the future of the trace. We show that verifying opacity of some regular secret for a regular language L w.r.t. an Orwellian projection is PSPACE-complete while it has been proved undecidable even for a regular language L w.r.t. a general Orwellian observation function. We finally illustrate relevancy of our results by proving the equivalence between the opacity property of regular secrets w.r.t. Orwellian projection and the intransitive non-interference property.
  • A Framework for Current-State Opacity Under Dynamic Information Release Mechanism
    Junyao Hou, Xiang Yin, Shaoyuan Li · Automatica, 140, article 110238, 2022 · doi.org/10.1016/j.automatica.2022.110238 · preprint: arXiv:2012.04874
    classical · finite-automata · opacity
    Show abstractHide 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 is 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, information is partially released and the corresponding definition of opacity is more suitable for non-prefix-closed observations.
  • Opacity of Discrete-Event Systems Under Nondeterministic Observation Mechanism
    Jing Zhang, Qianyu Chu, Xiaoguang Han, Zhiwu Li, Zengqiang Chen · Asian Journal of Control, 25(2), pp. 1577–1590, 2023 · doi.org/10.1002/asjc.2956
    classical · finite-automata · opacity
    Show abstractHide abstract
    For some practical systems modeled by discrete-event systems (DESs), the event observation mechanism may be no longer static/fixed due to sensor faults/failures, packet loss, and/or measurement uncertainties. It is required to redefine the observations of events. Therefore, it is interesting to reconsider the opacity in the context of abnormal conditions as mentioned. In this paper, we extend notions of initial-state opacity (ISO), current-state opacity (CSO), and initial-and-final-state opacity (IFSO) in a standard setting to an advanced framework of nondeterministic observations (i.e., the event-observation mechanism is state-dependent and nondeterministic) by taking the output-observation-equivalence instead of the natural projection-equivalence into account. To efficiently verify them, we construct three new matrix-based information structures in this advanced framework called an initial-state estimator, a current-state estimator, and an initial-and-final-state estimator using the Boolean semi-tensor product (BSTP) theory. Accordingly, the matrix-based criteria for verifying these three types of opacity are given, respectively. Computational complexity analysis as well as illustrative examples are also provided for the proposed results.
  • Verification of Current State Opacity using Switching Output Automata
    Tianyu Liu, Carla Seatzu, Alessandro Giua · 2023 9th International Conference on Control, Decision and Information Technologies (CoDIT), pp. 1–6 · doi.org/10.1109/CoDIT58514.2023.10284385
    The timed extension of this model is covered on the timed-systems page.
    classical · opacity
    Show abstractHide abstract
    We present a new discrete event model called switching output automaton where with each state is associated a set of discrete output values. The evolution of such a system, as state and output change, produces as observation a piecewise constant signal. The goal of this paper is that of designing a suitable observer for estimating the current discrete state of this model as a function of the observed output signal. In addition, we show how the observer can be used to verify if the system is current-state opaque.
  • Verification of Opacity Under a K-Delay Orwellian Observation Mechanism
    Jiahui Zhang, Kuize Zhang, Xiaoguang Han, Zhiwu Li · Mathematics, 13(10), article 1568, 2025 · doi.org/10.3390/math13101568
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity, an important property of the information flow in discrete-event systems (DESs), characterizes whether the secret information in a system is ambiguous to a passive observer (called an intruder). Observation models play a critical role in the analysis of opacity. In this paper, instead of adopting a fully static observation model or a fully dynamic observation model, we use a novel Orwellian-type observation model to study the verification of the current-state opacity (CSO), where the observability of an unobservable event can be re-interpreted once certain/several specific conditions are met. First, a K-delay Orwellian observation mechanism (KOOM) is proposed as a novel Orwellian-type observation mechanism for extending the existing Orwellian projection. The main characteristics of the KOOM are delaying the inevitable information release and narrowing the release range for historical information to protect the secrets in a system to a greater extent than with the existing Orwellian projection. Second, we formulate the definitions of standard and strong CSO under the KOOM. Finally, we address the verification problem for these two types of opacity by constructing two novel information structures called a standard K-delay verifier and a strong K-delay verifier, respectively. An analysis of the computational complexity and illustrative examples are also presented for the proposed results. Overall, the proposed notions of standard and strong CSO under the KOOM capture the security privacy requirements regarding a delayed release in applications, such as intelligent transportation systems, etc.
  • Current-State Opacity Based on State Outputs: Definition and Verification
    Patrícia C. Mayer, Felipe G. Cabral, Públio M. M. Lima, Marcos V. Moreira · Discrete Event Dynamic Systems, 36(1), article 23, 2026 · doi.org/10.1007/s10626-026-00444-x · conference precursor: “Current-State Opacity Based on State Outputs”, IFAC-PapersOnLine, 58(1), pp. 19–23, 2024 (WODES 2024) · doi.org/10.1016/j.ifacol.2024.07.004
    classical · finite-automata · opacity
    Show abstractHide abstract
    Cyber-physical systems (CPSs) are formed of physical and computational components that interact to operate a process safely and efficiently according to the desired behavior. To do so, the plant is continuously monitored, and the information obtained from its components is transmitted to computer-based devices. The connection between the plant and the monitoring and control device is carried out using communication networks, which may be susceptible to cyber-attacks. In this paper, we consider that the communication channel used to transmit data from the plant to the monitoring and control device is vulnerable to attacks, and that the attacker eavesdrops on the communication channel to gather sensitive information and discover if the system has reached a secret state. Since we assume that the information transmitted in the network is the status of system components, such as sensors, actuators, and memory variables of local controllers, the system can be modeled, from the attacker’s perspective, as a finite state transducer, where each state of the model is associated with an output vector formed of the signals associated with the system components. Considering that the attacker has full knowledge of the system model and does not know the current state of the system when he/she initiates to eavesdrop on the communication channel, the attacker tries to estimate the current state of the system by observing the state outputs transmitted in the network. Therefore, in this case, it is necessary to verify whether the attacker is never able to detect the secret states of the system. In the Discrete-Event System literature, the system property associated with the intruder’s inability to discover the system secret based on the transmitted information is called opacity. Since, in this paper, the attacker observes state outputs of a finite state transducer instead of events, we introduce a new notion of opacity called Current-State Opacity based on State Outputs (CSO-SO). We also present a method for the verification of CSO-SO. In addition, a comparison between the definition of current-state opacity based on event observations and CSO-SO is provided. A practical system is used to illustrate the definition and verification of CSO-SO.
  • Existential Opacity for Discrete-Event Systems with State Observations
    Zhiyuan Huang, Zhao Tong, Jiakai Li, Bingzhuo Zhong · arXiv preprint, 2026 · arXiv:2609.02132
    classical · diagnosability · opacity · trajectory-planning
    Show abstractHide abstract
    Opacity is a fundamental system property for confidentiality in discrete-event systems (DES). Classical opacity is typically defined under event-based observations, requiring that any secret system behavior remains indistinguishable from some non-secret behavior to an external intruder. However, in many applications such as path planning or opacity-preserving tasks, the intruder observes system states rather than events. Moreover, it often suffices that the system exhibits secret behaviors that can be exploited for opacity-preserving task execution, but such a system property cannot be fully captured by existing notions of state-observation-based opacity. Motivated by this limitation, we propose a relaxed notion of existing state-observation-based opacity, called existential opacity (EO), which only requires the existence of secret behaviors (instead of all secret behaviors) that are indistinguishable from a non-secret behavior under the state observations of the intruder. We show that the notion of EO is more expressive than existing state-observation-based opacity notions. In addition, a class of EO properties together with their corresponding verification approaches are developed, enabling the analysis of existential opacity in discrete-event systems and providing a new criterion for determining the feasibility of opacity-preserving problems.
  • Opacity of Extended Finite Automata with Event Parameters
    Weilin Deng, Daowen Qiu, Jingkai Yang · IEEE Transactions on Automatic Control, 71(4), pp. 2684–2691, 2026 · doi.org/10.1109/TAC.2025.3627016 · originally circulated as "Opacity of Parametric Discrete Event Systems: Models, Decidability, and Algorithms", arXiv:2307.03870, 2023 · arXiv:2307.03870
    classical · finite-automata · opacity
    Show abstractHide abstract
    Finite automata (FAs) are popular tools to characterize discrete event systems due to their succinctness. However, capturing data flow between systems and their environments using FAs can be challenging for some systems. To address this problem, this article introduces an extension of FAs, called extended finite automata with event parameters (EP-EFAs), where each transition carries a predicate over a tuple of event parameters. The issue of opacity analysis for EP-EFAs is investigated, and verification algorithms for current-state opacity, initial-state opacity, and infinite-step opacity are presented, using the symbolic observer. Experimental results demonstrate that these algorithms are significantly more efficient for EP-EFAs compared to classical algorithms for their corresponding FAs, particularly in cases involving large data domains. This article establishes a foundation for the opacity analysis of complex systems with data flow.

Richer secrets & intruders

Notions where the secret or the intruder differs from the standard setting: secrets about future behavior (pre-opacity), mixed opacity requirements, secrets that change over time, secrets about what a user knows (high-order and epistemic properties), and joint opacity against intruders that intersect state estimates.

  • Optimal Information Release for Mixed Opacity in Discrete-Event Systems
    Behnam Behinaein, Feng Lin, Karen Rudie · IEEE Transactions on Automation Science and Engineering, 16(4), pp. 1960–1970, 2019 · doi.org/10.1109/TASE.2019.2917136
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity is a property of a system that captures whether certain event sequences (or certain states) are indistinguishable from other event sequences (or states) in the system. Opacity is used in analyzing privacy, secrecy, and other aspects of systems modeled by discrete-event systems. In this paper, we introduce the concept of minimal information release policies for non-opacity and the concept of mixed opacity. Mixed opacity policies are introduced as a holistic approach for solving problems that involve a combination of releasing information to make some objectives of the system opaque while making some other objectives non-opaque. We present a set of algorithms for information release under a mixed opacity policy. These algorithms compute policies in a system such that two given sublanguages are opaque, and at the same time, two other sublanguages in the same system are non-opaque. The application of mixed opacity is demonstrated on the Dining Cryptographers Problem.
  • Generalized Current-State Opacity With Dynamically Changing Secrets
    Dan You, Shouguang Wang, Carla Seatzu · arXiv:2103.00234, 2021 · arXiv:2103.00234
    classical · finite-automata · opacity
    Show abstractHide abstract
    Opacity, an information-flow property related to the privacy and security of a system, has been extensively studied in the context of discrete event systems. Although various notions of opacity have been proposed, in all cases the considered secret was constant. This work focuses on current-state opacity, considering a scenario where the secret changes dynamically with the system evolution. In other words, we propose the new notion of generalized current-state opacity (GCSO), which is with respect to a dynamic-secret model rather than a constant secret. Moreover, we provide a method to verify GCSO based on the construction of the GCSO-verifier. Finally, a practical example is given to illustrate the proposed notion and the method for its verification.
  • Secure Your Intention: On Notions of Pre-Opacity in Discrete-Event Systems
    Shuo Yang, Xiang Yin · IEEE Transactions on Automatic Control, 68(8), pp. 4754–4766, 2022 · doi.org/10.1109/TAC.2022.3210148 · preprint: arXiv:2010.14120
    classical · finite-automata · opacity
    Show abstractHide abstract
    This article investigates an important information-flow 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 article, 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.
  • You Don't Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems
    Bohan Cui, Xiang Yin, Shaoyuan Li, Alessandro Giua · IFAC-PapersOnLine, 55(28), pp. 135–141, 2022 · doi.org/10.1016/j.ifacol.2022.10.335 · preprint: arXiv:2203.17051
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we investigate a class of information-flow security properties called opacity in partial-observed discrete-event systems. Roughly speaking, a system is said to be opaque if the intruder, which is modeled by a passive observer, can never determine the “secret” of the system for sure. Most of the existing notions of opacity consider secrets related to the actual behaviors of the system. In this paper, we consider a new type of secret related to the knowledge of the system user. Specifically, we assume that the system user also only has partial observation of the system and has to reason the actual behavior of the system. We say a system is high-order opaque if the intruder can never determine that the system user knows some information of importance based on its own incomparable information. We provide the formal definition of high-order opacity. Two algorithms are provided for the verification of this new notion: one with doubly-exponential complexity for the worst case and the other with single-exponential complexity. Illustrative examples are provided for the new notion of high-order opacity.
  • On Epistemic Properties in Discrete-Event Systems: A Uniform Framework and Its Applications
    Bohan Cui, Ziyue Ma, Shaoyuan Li, Xiang Yin · arXiv:2409.06588, 2024 · arXiv:2409.06588
    classical · finite-automata · opacity
    Show abstractHide abstract
    In this paper, we investigate the property verification problem for partially-observed DES from a new perspective. Specifically, we consider the problem setting where the system is observed by two agents independently, each with its own observation. The purpose of the first agent, referred to as the low-level observer, is to infer the actual behavior of the system, while the second, referred to as the high-level observer, aims to infer the knowledge of Agent 1 regarding the system. We present a general notion called the epistemic property capturing the inference from the high-level observer to the low-level observer. A typical instance of this definition is the notion of high-order opacity, which specifies that the intruder does not know that the system knows some critical information. This formalization is very general and supports any user-defined information-state-based knowledge between the two observers. We demonstrate how the general definition of epistemic properties can be applied in different problem settings such as information leakage diagnosis or tactical cooperation without explicit communications. Finally, we provide a systematic approach for the verification of epistemic properties. Particularly, we identify some fragments of epistemic properties that can be verified more efficiently.
  • Joint Opacity and Opacity Against State-Estimate-Intersection-Based Intrusion of Discrete-Event Systems
    K. Ritsuka, Stéphane Lafortune, Feng Lin · Automatica, 176, article 112136, 2025 · doi.org/10.1016/j.automatica.2025.112136
    classical · finite-automata · opacity
    Show abstractHide abstract
    This paper presents a general framework for joint opacity of discrete-event systems under partial observation. It discusses a class of state-estimate-intersection-based (SEI-based) intrusions that existing opacity conditions cannot prevent. The paper provides a procedure to verify the opacity of a system against such SEI-based intrusions. The results are formally verified by Isabelle/HOL.

Petri nets

Verification techniques specifically for (bounded) labeled Petri nets, rather than automata. Unbounded/general Petri nets raise genuine undecidability questions of their own, covered on a separate page about opacity of infinite-state systems.

  • Modelling Opacity Using Petri Nets
    Jeremy W. Bryans, Maciej Koutny, Peter Y. A. Ryan · Electronic Notes in Theoretical Computer Science, vol. 121, pp. 101–115, 2005 · doi.org/10.1016/j.entcs.2004.10.010
    Early treatment of opacity on Petri nets, before its generalization to transition systems.
    classical · opacity · petri-nets
    Show abstractHide abstract
    We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.
  • Verification of State-Based Opacity Using Petri Nets
    Yin Tong, Zhiwu Li, Carla Seatzu, Alessandro Giua · IEEE Transactions on Automatic Control, 62(6), pp. 2823–2837, 2017 · doi.org/10.1109/TAC.2016.2620429
    classical · opacity · petri-nets
    Show abstractHide abstract
    A system is said to be opaque if a given secret behavior remains opaque (uncertain) to an intruder who can partially observe system activities. This work addresses the verification of state-based opacity in systems modeled with Petri nets. The secret behavior of a system is defined as a set of states. More precisely, two state-based opacity properties are considered: current-state opacity and initial-state opacity. We show that both current-state and initial-state opacity problems in bounded Petri nets can be efficiently solved by using a compact representation of the reachability graph, called basis reachability graph (BRG). This approach is practically efficient since the exhaustive enumeration of the reachability space can be avoided.
  • On-Line Verification of Current-State Opacity by Petri Nets and Integer Linear Programming
    Xuya Cong, Maria Pia Fanti, Agostino Marcello Mangini, Zhiwu Li · Automatica, 94, pp. 205–213, 2018 · doi.org/10.1016/j.automatica.2018.04.021
    classical · opacity · petri-nets
    Show abstractHide abstract
    Opacity is a security and privacy property that evaluates whether an external observer (intruder) can infer a secret of a system by observing its behavior. This paper proposes an on-line approach to address the problem of current-state opacity in discrete event systems (DESs) modeled in a labeled Petri Net (PN) framework and by observing its evolution. An observation of the system is said to be current-state opaque if the intruder is unable to determine whether the current state of the system is within a set of secret states, otherwise it is said to be not current-state opaque. The proposed approach to verify the current-state opacity works on-line: the verification algorithm waits for the occurrence of an observable event and uses Integer Linear Programming problem solutions to verify if the behavior of the system is current-state opaque to the intruder under the given observation. Moreover, the proposed method is applied in two different settings: (i) a centralized approach where the intruder has full knowledge of the system model but can partially observe the system behavior; (ii) a decentralized approach where a set of intruders can observe different event sets and collaborate with a coordinator to disclose the same secret. Finally, experimental results are presented to demonstrate the efficiency of the proposed method.
  • The Complexity of Diagnosability and Opacity Verification for Petri Nets
    Béatrice Bérard, Stefan Haar, Sylvain Schmitz, Stefan Schwoon · Fundamenta Informaticae, 161(4), pp. 317–349, 2018 · doi.org/10.3233/FI-2018-1706 (journal version; conference precursor: 38th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2017), LNCS vol. 10258, pp. 200–220, Springer · doi.org/10.1007/978-3-319-57861-3_13)
    classical · diagnosability · infinite-state · opacity · petri-nets
    Show abstractHide abstract
    Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is EXPSPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.
  • On-Line Verification of Initial-State Opacity by Petri Nets and Integer Linear Programming
    Xuya Cong, Maria Pia Fanti, Agostino Marcello Mangini, Zhiwu Li · ISA Transactions, 93, pp. 108–114, 2019 · doi.org/10.1016/j.isatra.2019.01.023
    classical · opacity · petri-nets
    Show abstractHide abstract
    This paper deals with a problem related to the observability of discrete event systems: the initial-state opacity. Given a set of system states (the secret), a system observation is called initial-state opaque if an agent (named intruder), who can partially observe the system, cannot determine whether the set of initial states consistent with an event sequence is included in the secret. Such a character can describe security problems in cyber-infrastructures, such as Internet and mobile communication networks or national defense service systems. This work presents a novel on-line methodology to verify the notion of initial-state opacity of discrete event systems that are modeled by labeled Petri nets. By working on-line, the intruder records an event and exploits integer linear programming problem for checking the initial-state opacity of the system’s evolution under the given observation. A set of examples are shown to shed light on the efficiency of the presented methodology.
  • Current-State Opacity Modelling and Verification in Partially Observed Petri Nets
    Ikram Saadaoui, Zhiwu Li, Naiqi Wu · Automatica, 116, article 108907, 2020 · doi.org/10.1016/j.automatica.2020.108907
    classical · opacity · petri-nets
    Show abstractHide abstract
    System opacity is a widely studied security notion, implying that a secret behaviour of a given system cannot be seen or assessed by an external observer based on the system evolution. This work deals with the problem of current-state opacity formulation and verification in the context of discrete event systems modelled with partially observed Petri nets (POPNs) (i.e., Petri nets containing place sensors that measure the number of tokens in observable places and event sensors that indicate the firing of observable transitions). A Petri net system is recognized as current-state opaque if the current-state estimate is never entirely contained in the set of secret states. In this regard, we introduce the notion of discernible markings to design a reduced state estimator called a discernible reachability graph, and then come up with formal modelling of current-state opacity in POPN systems. The main idea of the proposed approach consists in proving that if a system is current-state opaque, its current-state estimate, possibly established by an intruder, contains at least one non-secret state. We exploit the mathematical feasibility to formulate this concept by defining and solving an integer linear programming problem with respect to a given secret and an observation sequence collected from sensors. In the light of the proposed modelling, necessary and sufficient conditions are proposed for opacity verification, and examples are given to expose the results.
  • Verification of K-Step and Infinite-Step Opacity of Bounded Labeled Petri Nets
    Yin Tong, Haocen Lan, Carla Seatzu · Automatica, 140, article 110221, 2022 · doi.org/10.1016/j.automatica.2022.110221
    classical · opacity · petri-nets
    Show abstractHide abstract
    Opacity is an important information security property. Given a discrete event system, a set of secret states, and an intruder who observes the system evolution through an observation mask, the system is said to be K-step opaque if the intruder is not able to ascertain that the system is or was in a secret state at some time within K steps, namely within the observation of K events. If the intruder is never able to ascertain that the system is or was in a secret state at any time, the system is said to be infinite-step opaque. This work aims at verifying the two opacity properties when the discrete event system is modeled as a bounded labeled Petri net. Using the notion of basis reachability graph, new approaches are proposed to check K-step opacity and infinite-step opacity. The proposed approaches are shown to be more efficient than the standard methods based on the reachability graph.
  • Language-Based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets
    Salwa Habbachi, Zhiwu Li, Naiqi Wu, Mohamed Khalgui · Science Progress, 105(1), article 368504221075466, 2022 · doi.org/10.1177/00368504221075466
    classical · opacity · petri-nets
    Show abstractHide abstract
    This work deals with the language-based opacity verification and enforcement problems in discrete event systems modeled with labeled Petri nets. Opacity is a security property that relates to privacy protection by hiding secret information of a system from an external observer called an “intruder”. A secret can be a subset of a system's language. In this case, opacity is referred to as language-based opacity. A system is said to be language-based opaque if an intruder, with a partial observation on the system's behavior, cannot deduce whether the sequences of events corresponding to the generated observations are included in the secret language or not. We propose a novel and efficient approach for language-based opacity verification and enforcement, using the concepts of basis markings and basis partition. First, a sufficient condition is formulated to check language-based opacity for labeled Petri nets by solving an integer-programming problem. A unique graph, called a modified basis reachability graph (MBRG), is then derived to verify different language-based opacity properties. The proposed method relaxes the acyclicity assumption of the unobservable transition subnet thanks to the basis partition notion. A new embedded insertion function technique is also provided to deal with opacity enforcement. This technique ensures that no new observed behavior is created. A verification algorithm is developed to check the enforceability of a system. Finally, once a system is proved to be enforceable, an algorithm is given to construct a new structure, called an insertion automaton, which synthesizes all possible insertion functions that ensure opacity.
  • Current-State Opacity Verification in Discrete Event Systems Using an Observer Net
    Abdeldjalil Labed, Ikram Saadaoui, Naiqi Wu, Jiaxin Yu, Zhiwu Li · Scientific Reports, 12, article 21479, 2022 · doi.org/10.1038/s41598-022-25697-y
    classical · opacity · petri-nets
    Show abstractHide abstract
    Due to the proliferation of contemporary computer-integrated systems and communication networks, there is more concern than ever regarding privacy, given the potential for sensitive data exploitation. A recent cyber-security research trend is to focus on security principles and develop the foundations for designing safety-critical systems. In this work, we investigated the problem of verifying current-state opacity in discrete event systems using labeled Petri nets. A system is current-state opaque provided that the current-state estimate cannot be revealed as a subset of secret states. We introduced a new sub-model of the system, named an observer net. The observer net have the same structure as the plant, but it is distinguished by the use of colored markers as well as simultaneous and recursive transition enabling and firing, which offer an efficient state estimation. We considered two settings of the proposed approach: an on-line setting, in which a current-state opacity algorithm is proposed. The algorithm waits for the occurrence of an observable event and determines if the current observation of a plant reveals the secret behaviour, as well as, an off-line setting, where the verification problem is solved based on a state estimator called a colored estimator. In this context, necessary and sufficient conditions for verifying opacity are developed with illustrative examples to demonstrate the presented approach.
  • Assessment of Initial-State-Opacity in Live and Bounded Labeled Petri Net Systems via Optimization Techniques
    Francesco Basile, Gianmaria De Tommasi, Carlo Motta · Automatica, 152, article 110911, 2023 · doi.org/10.1016/j.automatica.2023.110911
    classical · opacity · petri-nets
    Show abstractHide abstract
    Opacity is a property of discrete event systems (DES) that is related to the possibility of hiding a secret to external observers, the so called intruders. If the secret is the system initial state, then the related opacity problem is referred to as Initial State Opacity (ISO). This paper gives a necessary and sufficient condition to check ISO in DES modeled as bounded and live labeled Petri nets (PNs). The proposed approach relies on both the algebraic representation of labeled PNs dynamic, and on their structural representation in terms of minimal support T-invariants. The proposed necessary and sufficient condition enables ISO assessment by means of the solution of Integer Linear Programming problems, which can be efficiently solved nowadays by means of off-the-shelf optimization tools.
  • A Symbolic Approach to the Verification and Enforcement of Current-State Opacity Using Labelled Petri Nets
    Kun Peng, Yufeng Chen, Zhiwu Li · IET Control Theory & Applications, 18(2), pp. 171–183, 2024 · doi.org/10.1049/cth2.12546
    classical · opacity · petri-nets
    Show abstractHide abstract
    This work proposes a symbolic method to verify and enforce the current-state opacity of labelled Petri nets (LPNs). The notion of basis markings of partially observed Petri nets currently dominates the development of opacity verification and enforcement for discrete event systems. However, the related computational efficiency, to a great extent, depends on the number of basis markings in a system, which increases exponentially with respect to the size of its corresponding LPN model. Binary decision diagrams (BDDs) are capable of computing a set of basis markings in a compact shared structure. To mitigate the computational overheads, a BDD-based method to efficiently model the structure and behaviour of an LPN is proposed. Then, the current-state opacity of LPNs is verified and enforced in a symbolic manner. Finally, a number of examples are provided to demonstrate the effectiveness and efficiency of the proposed method.
  • State Opacity via Structural Observability in Continuous Petri Nets
    Cristian Mahulea · 2025 IEEE 21st International Conference on Automation Science and Engineering (CASE), pp. 2935–2940 · doi.org/10.1109/CASE58245.2025.11164017
    classical · opacity · petri-nets
    Show abstractHide abstract
    This paper investigates state-opacity in discrete Petri nets through structural observability derived from continuous Petri nets. We provide structural conditions ensuring or violating initial-state and current-state opacity, leveraging partial measurements of markings. We illustrate our methodology through a healthcare application involving the confidentiality of patient decisions in anterior cruciate ligament (ACL) treatments.
  • Current-State Opacity in Safe Partially Observed Quantum Petri Nets: True-Concurrency Semantics and Exact Symbolic Verification
    Sichen Ding, Zhiwu Li · arXiv preprint, 2026 · arXiv:2604.17784
    classical · opacity · petri-nets
    Show abstractHide abstract
    Classical opacity theory for discrete-event systems relies strictly on observable event sequences, fundamentally failing to capture security breaches in hybrid architectures where an attacker exploits both classical traces and localized quantum correlations. To address this gap, we formalize current-state opacity within the framework of safe partially observed quantum Petri nets by introducing a true-concurrency semantics that represents classical observations as partially ordered multisets via unfolding configurations. Building upon this, we define quantitative posterior-state leakage as the trace distance between the attacker's localized quantum states, evaluated conditionally on whether the underlying system has reached a secret or non-secret marking. This formulation strictly preserves classical opacity definitions. To achieve computational tractability, we apply the stabilizer formalism and develop an exact symbolic verification algorithm. By combining targeted unfolding exploration, state aggregation exclusively at maximal unobservable reach, and stabilizer-tableau propagation, this procedure circumvents both concurrent interleaving explosions and exponential density-matrix overhead. Finally, an entanglement-swapping case study validates the exact leakage evaluation, demonstrates substantial computational gains, and establishes a rigorous interface for counterexample-guided leakage enforcement.
B

Control & Enforcement

Making a system opaque, or enforcing opacity when it is initially absent, by restricting or modifying its behavior. Four mechanisms appear across this literature: supervisory control (disabling events), insertion and edit functions (adding or changing events in the observation channel), obfuscation policies (altering what the observer sees at the output), and approaches that account for an active or adversarial intruder.

Supervisory control

Restrict which controllable events are allowed to occur, rather than touching what the observer sees.

  • Opacity Enforcing Control Synthesis
    Jérémy Dubreil, Philippe Darondeau, Hervé Marchand · 9th International Workshop on Discrete Event Systems (WODES 2008), pp. 28–35 · doi.org/10.1109/WODES.2008.4605918
    classical · opacity · supervisory-control
    Show abstractHide abstract
    Given a finite transition system and a regular predicate, we address the problem of computing a controller enforcing the opacity of the predicate against an attacker (that partially observes the system), supposedly trying to push the system to reveal the predicate. Assuming that the controller can only control a subset of the events it observes (possibly different from the ones of the attacker), we show that an optimal control always exists and provide sufficient conditions under which it is regular and effectively computable. These conditions rely on the inclusion relationships between the observable alphabets of the attacker and the controller and the controllable alphabet.
  • A Formula for the Supremal Controllable and Opaque Sublanguage Arising in Supervisory Control
    Shigemasa Takai, Yohei Oka · SICE Journal of Control, Measurement, and System Integration, 1(4), pp. 307–311, 2008 · doi.org/10.9746/jcmsi.1.307
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In this paper, we study a property of opacity in the language-based framework of discrete event systems. The problem of synthesizing a supervisor that enforces opacity in a maximally permissive way is addressed. A maximally permissive opacity-enforcing supervisor is realized by an automaton that generates the supremal closed controllable and opaque sublanguage of the generated language of the system. This motivates the study on computability of the supremal sublanguage. We present a formula for computing the supremal sublanguage under some assumption on uncontrollable events. Whenever the languages under consideration are regular, the supremal sublanguage is effectively computed using the presented formula.
  • Supervisory Control for Opacity
    Jérémy Dubreil, Philippe Darondeau, Hervé Marchand · IEEE Transactions on Automatic Control, 55(5), pp. 1089–1100, 2010 · doi.org/10.1109/TAC.2010.2042008 · inria-00483891
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In the field of computer security, a problem that received little attention so far is the enforcement of confidentiality properties by supervisory control. Given a critical system G that may leak confidential information, the problem consists in designing a controller C, possibly disabling occurrences of a fixed subset of events of G, so that the closed-loop system G/C does not leak confidential information. We consider this problem in the case where G is a finite transition system with set of events Σ and an inquisitive user, called the adversary, observes a subset Σa of Σ. The confidential information is the fact (when it is true) that the trace of the execution of G on Σ* belongs to a regular set S ⊆ Σ*, called the secret. The secret S is said to be opaque w.r.t. G (resp. G/C) and Σa if the adversary cannot safely infer this fact from the trace of the execution of G (resp. G/C) on Σa*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controller C such that S is opaque w.r.t. G/C and Σa. This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet Σa of the adversary and the set of events that the controller can disable are comparable.
  • Supervisory Control for Opacity of Discrete Event Systems
    Mohamed Ben-Kalefa, Feng Lin · 49th Annual Allerton Conference on Communication, Control, and Computing, 2011, pp. 1113–1119 · doi.org/10.1109/Allerton.2011.6120292
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In previous papers, we investigated the properties of opacity and we discussed the modification of the languages to satisfy the strong opacity, weak opacity, and no opacity in the framework of discrete event systems. In this paper, we study how to ensure strong opacity, weak opacity and no opacity by a supervisory control. If strong opacity, weak opacity or no opacity is not satisfied, then we can restrict the system's behavior by a supervisor so that strong opacity, weak opacity or no opacity is satisfied. We consider the strong opacity control problem (SOCP), weak opacity control problem (WOCP) and no opacity control problem (NOCP). We characterize the solutions to SOCP in terms of the largest sublanguage that is controllable, observable (or normal), and strongly opaque. Similar characterization is available for solutions to NOCP. We also show that solutions to WOCP do not exist. We present formulas and algorithms for finding solutions to SOCP and NOCP. Examples are given to illustrate the results.
  • Opacity-Enforcing Supervisory Strategies via State Estimator Constructions
    Anooshiravan Saboori, Christoforos N. Hadjicostis · IEEE Transactions on Automatic Control, 57(5), pp. 1155–1165, 2012 · doi.org/10.1109/TAC.2011.2170453 · conference version: "Opacity-Enforcing Supervisory Strategies for Secure Discrete Event Systems", 47th IEEE Conference on Decision and Control (CDC 2008), pp. 889–894
    classical · opacity · supervisory-control
    Show abstractHide abstract
    State-based notions of opacity, such as initial-state opacity and infinite-step opacity, emerge as key properties in numerous security applications of discrete event systems. We consider systems that are modeled as partially observed nondeterministic finite automata and tackle the problem of constructing a minimally restrictive opacity-enforcing supervisor (MOES), which limits the system's behavior within some prespecified legal behavior while enforcing initial-state opacity or infinite-step opacity requirements. We characterize the solution to MOES, under some mild assumptions, in terms of the supremal element of certain controllable, normal, and opaque languages. We also show that this supremal element always exists and that it can be implemented using state estimators. The result is a supervisor that achieves conformance to the pre-specified legal behavior while enforcing initial-state opacity by disabling, at any given time, a subset of the controllable system events, in a way that minimally restricts the range of allowable system behavior. Although infinite-step opacity cannot be easily translated to language-based opacity, we show that, by using a finite bank of supervisors, the aforementioned approach can be extended to enforce infinite-step opacity in a minimally restrictive way.
  • Synthesis of Opaque Systems with Static and Dynamic Masks
    Franck Cassez, Jérémy Dubreil, Hervé Marchand · Formal Methods in System Design, 40(1), pp. 88–115, 2012 · doi.org/10.1007/s10703-012-0141-9 · hal-00662539
    classical · opacity · supervisory-control
    Show abstractHide abstract
    Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask.
  • Enforcing Opacity of Regular Predicates on Modal Transition Systems
    Philippe Darondeau, Hervé Marchand, Laurie Ricker · Discrete Event Dynamic Systems, 25(1), pp. 251–270, 2015 · doi.org/10.1007/s10626-014-0193-7 · hal-00987988
    classical · opacity · supervisory-control
    Show abstractHide abstract
    Given a labelled transition system G partially observed by an attacker, and a regular predicate Sec over the runs of G, enforcing opacity of the secret Sec in G means computing a supervisory controller K such that an attacker who observes a run of the controlled system K/G cannot ascertain that the trace of this run belongs to Sec based on the knowledge of G and K. We lift the problem from a single labelled transition system G to the class of all labelled transition systems specified by a Modal Transition System M. The lifted problem is to compute the maximally permissive controller K such that Sec is opaque in K/G for every labelled transition system G which is a model of M. The situations of the attacker and of the controller are asymmetric: at run time, the attacker may fully know G and K whereas the controller knows only M and the sequence of actions executed so far by the unknown G. We address the problem in two cases. Let Σa denote the set of actions that can be observed by the attacker, and let Σc and Σo denote the sets of actions that can be controlled and observed by the controller, respectively. We provide optimal and regular controllers that enforce the opacity of regular secrets when Σc ⊆ Σo ⊆ Σa = Σ. We provide optimal and regular controllers that enforce the opacity of regular upper-closed secrets (Sec = Sec·Σ*) under the following assumptions: (i) Σa ⊆ Σc ⊆ Σo = Σ or (ii) Σa, Σc ⊆ Σo = Σ and wσ ∈ Sec ⇒ w ∈ Sec for all σ ∈ Σ∖Σc.
  • A Uniform Approach for Synthesizing Property-Enforcing Supervisors for Partially-Observed Discrete-Event Systems
    Xiang Yin, Stéphane Lafortune · IEEE Transactions on Automatic Control, 61(8), pp. 2140–2154, 2015 · doi.org/10.1109/TAC.2015.2484359
    classical · opacity · supervisory-control
    Show abstractHide abstract
    The problem under consideration in this paper is that of enforcement by supervisory control of a given property on a partially-observed discrete-event system. We present a general methodology that is applicable to a large class of properties previously studied (individually) in the literature. These properties include, but are not restricted to, safety, diagnosability, opacity, detectability, anonymity and attractability. When the given system does not satisfy the considered property, the objective is to synthesize a supervisor that restricts the system's behavior and provably enforces the given property; moreover, it is required that this supervisor be maximally permissive. We consider the general case where the system's events are partitioned into observable and unobservable events, and controllable and uncontrollable events, and we do not make any assumptions about these two partitions; in particular, we do not assume that all controllable events are observable. Our uniform approach first maps the considered property to a suitably-defined information state for the partially-observed system and then develops a supervisor synthesis methodology based on a finite bipartite transition system that embeds all reachable information states and all admissible supervisory control strategies. This transition system is called the All Enforcement Structure (or AES). We present an algorithm for the construction of the AES and discuss its properties. Then we use the AES to develop a synthesis algorithm that constructs a supervisor that is provably property enforcing and maximally permissive. We illustrate the application of our uniform approach to the enforcement of the above-mentioned properties.
  • Supervisory Control of Discrete-Event Systems for Infinite-Step Opacity
    Yifan Xie, Xiang Yin · 2020 American Control Conference (ACC), pp. 3665–3671 · doi.org/10.23919/ACC45564.2020.9148014
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In this paper, we investigate the problem of synthesizing maximally-permissive opacity-enforcing supervisors for partially-observed discrete-event systems. We focus on a specific type of opacity called infinite-step opacity requiring that the intruder, which is modeled as a passive observer, can never determine for sure that the system is/was at a secret state for any specific instant. When the original system is verified to be non-opaque, one is interested in synthesizing a supervisor that controls the system in a least-restrictive manner such that the closed-loop system is opaque. We provide an effective approach for solving the infinite-step opacity control problem by re-formulating this problem as a two-player game over a generalized information structure that involves information delays. We show that the proposed synthesis algorithm is sound and complete, and the resulting supervisor is maximally-permissive. Most of the existing works on opacity-enforcing supervisory control only consider current-state opacity in which no delayed information is involved. Our work provides a complete solution to the infinite-step opacity control problem without any assumption on the relationship between controllable events and observable events.
  • Verification and Enforcement of Strong Infinite- and K-Step Opacity Using State Recognizers
    Ziyue Ma, Xiang Yin, Zhiwu Li · Automatica, 133, article 109838, 2021 · doi.org/10.1016/j.automatica.2021.109838
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In this paper, we study the verification and enforcement problems of strong infinite-step opacity and k-step opacity for partially observed discrete-event systems modeled by finite state automata. Strong infinite-step opacity is a property such that the visit of a secret state cannot be inferred by an intruder at any instance along the entire observation trajectory, while strong k-step opacity is a property such that the visit of a secret state cannot be inferred within k steps after the visit. We propose two information structures called an ∞-step recognizer and a k-step recognizer to verify these two properties. The complexities of our algorithms to verify strong infinite- and k-step opacity are O(22⋅|X|⋅|Eo|) and O(2(k+2)⋅|X|⋅|Eo|), respectively, which are lower than that of existing methods in the literature (|X| and |Eo| are the numbers of states and observable events in a plant, respectively). We also derive an upper bound for the value of k in strong k-step opacity, and propose an effective algorithm to determine the maximal value of k for a given plant. Finally, we note that enforcement of strong infinite- and k-step opacity can be transformed into a language specification enforcement problem and hence be solved using supervisory control.
  • Opacity Enforcing Supervisory Control Using Nondeterministic Supervisors
    Yifan Xie, Xiang Yin, Shaoyuan Li · IEEE Transactions on Automatic Control, 67(12), pp. 6567–6582, 2021 · doi.org/10.1109/TAC.2021.3131125
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In this article, we investigate the enforcement of opacity via supervisory control in the context of discrete-event systems. A system is said to be opaque if the intruder, which is modeled as a passive observer, can never infer confidently that the system is at a secret state. The design objective is to synthesize a supervisor such that the closed-loop system is opaque even when the control policy is publicly known. In this article, we propose a new approach for enforcing opacity using nondeterministic supervisors. A nondeterministic supervisor is a decision mechanism that provides a set of control decisions at each instant, and randomly picks a specific control decision from the decision set to actually control the plant. Compared with the standard deterministic control mechanism, such a nondeterministic control mechanism can enhance the plausible deniability of the controlled system as the online control decision is a random realization and cannot be implicitly inferred from the control policy. We provide a sound and complete algorithm for synthesizing a nondeterministic opacity-enforcing supervisor. Furthermore, we show that nondeterministic supervisors are strictly more powerful than deterministic supervisors in the sense that there may exist a nondeterministic opacity-enforcing supervisor even when deterministic supervisors cannot enforce opacity.
  • Using Subobservers to Synthesize Opacity-Enforcing Supervisors
    Richard Hugh Moulton, Behnam Behinaein Hamgini, Zahra Abedi Khouzani, Rômulo Meira-Góes, Fei Wang, Karen Rudie · Discrete Event Dynamic Systems, 32(4), pp. 611–640, 2022 · doi.org/10.1007/s10626-022-00365-5 · preprint: arXiv:2110.04334
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In discrete-event system control, the worst-case time complexity for computing a system’s observer is exponential in the number of that system’s states. This results in practical difficulties since some problems require calculating multiple observers for a changing system, e.g., synthesizing an opacity-enforcing supervisor. Although calculating these observers in an iterative manner allows us to synthesize an opacity-enforcing supervisor and although methods have been proposed to reduce the computational demands, room exists for a practical and intuitive solution. Here we extend the subautomaton relationship to the notion of a subobserver and demonstrate its use in reducing the computations required for iterated observer calculations. We then demonstrate the subobserver relationship’s power by simplifying state-of-the-art synthesis approaches for opacity-enforcing supervisors under realistic assumptions.
  • Optimal Secret Protection in Discrete Event Systems with Dynamic Clearance Levels
    Ziyue Ma, Kai Cai · IFAC-PapersOnLine, 56(2), pp. 3579–3584, 2023 · doi.org/10.1016/j.ifacol.2023.10.1517
    classical · finite-automata · opacity · supervisory-control
    Show abstractHide abstract
    In this paper we propose a general framework to design optimal secret protection policies in discrete event systems. In the system, some secret states are associated with confidentiality levels (possibly different), and our purpose is to design an event-protecting policy such that any user (legal or unauthorized) who visits a secret state must have a security clearance level no less than the required confidentiality level. We consider the criteria of optimality on protecting policies as to protecting policies with a minimum degree of disturbance to legal users’ normal operations. We develop an auxiliary data structure called the generalized secret automaton, based on which we propose a method to design a protecting policy using the classical supervisory control theory. The minimally disruptive protecting policy is then represented by an automaton called the secret enforcer whose state size is polynomial both in the number of the plant states and the number of secret states in the plant.
  • Optimal Synthesis of Opacity-Enforcing Supervisors for Qualitative and Quantitative Specifications
    Yifan Xie, Shaoyuan Li, Xiang Yin · IEEE Transactions on Automatic Control, 69(8), pp. 4958–4973, 2024 · doi.org/10.1109/TAC.2023.3342880 · preprint: arXiv:2102.01402
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In this article, we investigate both qualitative and quantitative synthesis of optimal privacy-enforcing supervisors for partially observed discrete-event systems. We consider a dynamic system whose information flow is partially available to an intruder, which is modeled as a passive observer. We assume that the system has a “secret” that does not want to be revealed to the intruder. Our goal is to synthesize a supervisor that controls the system in a least-restrictive manner such that the closed-loop system meets the privacy requirement. For the qualitative case, we adopt the notion of infinite-step opacity as the privacy specification by requiring that the intruder can never determine for sure that the system is/was at a secret state for any specific instant. If the qualitative synthesis problem is not solvable or the synthesized solution is too restrictive, then we further investigate the quantitative synthesis problem so that the secret is revealed (if unavoidable) as late as possible within a finite security-preserving horizon. Effective algorithms are provided to solve both the qualitative and quantitative synthesis problems. Specifically, by building suitable information structures that involve information delays, we show that the optimal qualitative synthesis problem can be solved as a safety game. The optimal quantitative synthesis problem can also be solved as an optimal total-cost control problem over an augmented information structure. Our work provides a complete solution to the standard infinite-step opacity control problem, which has not been solved without an assumption on the relationship between controllable events and observable events. Furthermore, we generalize the opacity enforcement problem to the numerical setting by introducing the secret-revelation-time as a new quantitative measure.
  • Synthesis of Opacity-Enforcing Supervisory Strategies Using Reinforcement Learning
    Huimin Zhang, Li Huang, Wanling Huang, Lei Feng, Xianxian Li · IEEE Transactions on Automation Science and Engineering, 22, pp. 6896–6906, 2025 · doi.org/10.1109/TASE.2024.3456239
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In the control of discrete-event systems for current-state opacity enforcement, it is difficult to synthesize a supervisor by supervisory control theory (SCT) without explicit formal models of the systems. This study utilizes the reinforcement learning (RL) method to obtain supervisory policies for opacity enforcement in the case when the automaton model of the system is unavailable. The state space of the environment in the RL is dynamically generated through system simulation. Actions are defined according to the control patterns of the SCT. A reward function is proposed to evaluate whether the secret is exposed or not. Then, a sequence of state-action-reward chains are obtained as system simulation goes on. The frameworks of Q-learning and State-Action-Reward-State-Action (SARSA) algorithms are adopted to implement the proposed approach. The goal of the training is to maximize the total accumulative reward by optimizing the action selection in the learning process. Then, an optimal supervisory policy is obtained when the training process converges. Experiments are performed to illustrate the effectiveness of the proposed approach. The contributions are two aspects. Firstly, a supervisor for opacity enforcement is learned by RL training without an explicit formal model of the system. Secondly, the ability of the proposed method in computing supervisory policies without formal models addresses a significant gap in the literature and offers a new direction for research in opacity enforcement in discrete event systems. Note to Practitioners—Supervisory Control Theory (SCT) supplies an effective way to synthesize supervisors, which traditionally handles tasks with explicit system models for current-state opacity enforcement by restricting behavior of systems. However, formal models of systems are often confidential or otherwise unavailable. This paper presents a method for supervisor synthesis via reinforcement learning in the case of lacking formal models of systems. The proposed method leverages the characteristics of control patterns in SCT and optimizes the action selection in the training process through a reward mechanism that evaluates the secrecy of states. The approach can be applied to model-free RL frameworks such as Q-learning and State-Action-Reward-State-Action (SARSA) algorithms. The training is performed as the system simulation goes on. When the training process converges, the optimal policy can be used to enforce opacity for the system. However, Q-table is used to save the Q-value in both Q-learning and SARSA algorithms. In the worst case, the size of the Q-table grows exponentially with the number of states and controllable events increasing. This can lead to memory exhaustion when the system’s scale is large. To make the approach scalable, we will attempt to use DRL to train control policies for opacity enforcement in the future.
  • A Two-Pronged Approach to Security of Discrete-Event Systems
    Shoma Matsui, Karen Rudie, Kai Cai · Journal of Systems Science and Complexity, 38(1), pp. 178–209, 2025 · doi.org/10.1007/s11424-025-4263-8
    classical · opacity · supervisory-control
    Show abstractHide abstract
    This paper investigates a security problem of simultaneously addressing two types of attacks: Eavesdropping and infiltration. The authors model the target system as a discrete-event system (DES) with subsets of concealable events and protectable events, in order to make the proposed methodology applicable to various practical systems and employ two existing works of DES security: Degree of opacity and state protection. Specifically, the authors consider that all protectable events are observable, and some observable events are concealable. In addition, protectable events cannot be protected once they are concealed. Given such a constraint, the goal is to figure out which events to conceal and which transitions to protect so that the prescribed requirements of degree of opacity and state protection are satisfied. In this work the authors decide which events to conceal as all transitions of a given event label are concealed or not concealed. The proposed problem formulation also requires a solution to only involve absolutely necessary protectable events in order for the system to avoid superfluous protection costs. The authors first examine a general version of our security problem with an intuitive algorithm to compute acceptable solutions, and then present a special version which results in a reduced computation time compared to the general version.
  • On Prediction-Based Properties of Discrete-Event Systems: Notions, Applications and Supervisor Synthesis
    Bohan Cui, Ziyue Ma, Alessandro Giua, Xiang Yin · arXiv:2510.04616, 2025 · arXiv:2510.04616
    classical · finite-automata · opacity · supervisory-control
    Show abstractHide abstract
    In this work, we investigate the problem of synthesizing property-enforcing supervisors for partially-observed discrete-event systems (DES). Unlike most existing approaches, where the enforced property depends solely on the executed behavior of the system, here we consider a more challenging scenario in which the property relies on predicted future behaviors that have not yet occurred. This problem arises naturally in applications involving future information, such as active prediction or intention protection. To formalize the problem, we introduce the notion of prediction-based properties, a new class of observational properties tied to the system's future information. We demonstrate that this notion is very generic and can model various practical properties, including predictability in fault prognosis and pre-opacity in intention security. We then present an effective approach for synthesizing supervisors that enforce prediction-based properties. Our method relies on a novel information structure that addresses the fundamental challenge arising from the dependency between current predictions and the control policy. The key idea is to first borrow information from future instants and then ensure information consistency. This reduces the supervisor synthesis problem to a safety game in the information space. We prove that the proposed algorithm is both sound and complete, and the resulting supervisor is maximally permissive.
  • Optimal Control Strategy for K-Level Opaque Systems Based on the Optimization Method of Multi-Selection Problems at Each Stage
    Yinyin Dai, Fei Wang, Jiliang Luo · Discrete Event Dynamic Systems, 36(1), 2026 · doi.org/10.1007/s10626-026-00429-w
    classical · finite-automata · opacity · supervisory-control
    Show abstractHide abstract
    The concept of k-level opacity is used to determine the level of opacity in a system. If the tolerance level k is higher, then the degree of opacity for any secret information will also be higher. However, if more non-secret information are not distinguished from secret ones, then the cost of achieving a control strategy will also be higher. In this paper, an optimization model that minimizes the discount total choosing cost while maintaining k-level opacity and releasing all the secret string is presented. If the secret language is k-level opaque w.r.t. its closure, the closure or the infimal controllable super-language of the closure is the optimal solution. If the secret language is not k-level opaque w.r.t. its closure, then a Multi-Stage Optimization Problem with Multi-Selection at each Stage (MSOP-MSS) is proposed. By analyzing the MSOP-MSS, an algorithm for handling the situation was proposed and used to obtain control strategy for the optimization model. The control strategy has been proven to be optimal. Finally, a complete algorithm, computational complexity analysis, and application examples are described.

Insertion, edit & modification functions

Leave the system's actual behavior untouched and instead alter what the observer perceives: inserting fictitious events, substituting or deleting observed ones, or more general modifications.

  • Synthesis of Insertion Functions for Enforcement of Opacity Security Properties
    Yi-Chin Wu, Stéphane Lafortune · Automatica, 50(5), pp. 1336–1348, 2014 · doi.org/10.1016/j.automatica.2014.02.038
    The insertion-function mechanism proposed here is extended by several later entries of this section (edit and modification functions).
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity is a confidentiality property that characterizes whether a “secret” of a system can be inferred by an outside observer called an “intruder”. In this paper, we consider the problem of enforcing opacity in systems modeled as partially-observed finite-state automata. We propose a novel enforcement mechanism based on the use of insertion functions. An insertion function is a monitoring interface at the output of the system that changes the system’s output behavior by inserting additional observable events. We define the property of “i-enforceability” that an insertion function needs to satisfy in order to enforce opacity. I-enforceability captures an insertion function’s ability to respond to every system’s observed behavior and to output only modified behaviors that look like existing non-secret behaviors. Given an insertion function, we provide an algorithm that verifies whether it is i-enforcing. More generally, given an opacity notion, we determine whether it is i-enforceable or not by constructing a structure called the “All Insertion Structure” (AIS). The AIS enumerates all i-enforcing insertion functions in a compact state transition structure. If a given opacity notion has been verified to be i-enforceable, we show how to use the AIS to synthesize an i-enforcing insertion function.
  • Synthesis of Optimal Insertion Functions for Opacity Enforcement
    Yi-Chin Wu, Stéphane Lafortune · IEEE Transactions on Automatic Control, 61(3), pp. 571–584, 2016 · doi.org/10.1109/TAC.2015.2440632 · conference version: "Synthesis of Opacity-Enforcing Insertion Functions that Can Be Publicly Known", 54th IEEE Conference on Decision and Control (CDC 2015), pp. 3506–3513
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Our prior work has studied the enforcement of opacity security properties using insertion functions. Given a system that is not opaque, the so-called All Insertion Structure (AIS) is a game structure, played by the system and the insertion function, that embeds all valid insertion functions. In this paper, we first propose a more compact AIS that can be constructed with lower computational complexity. We then introduce the maximum total cost and the maximum mean cost, and use them as quantitative objectives to solve for optimal insertion functions. Specifically, we first determine if an insertion function with a finite total cost exists. If such an insertion function exists, we synthesize an optimal total-cost insertion function. Otherwise, we construct an optimal mean-cost insertion function. In either case, we find an optimal insertion strategy on the AIS, with respect to the corresponding cost objective. The algorithmic procedures are adapted from results developed for minimax games and mean payoff games. The resulting optimal strategy is represented as a subgraph of the AIS that consists of all the system actions and the optimal insertion actions. Finally, we use this subgraph to synthesize an optimal insertion function that is encoded as an I/O automaton.
  • Enforcement of Opacity by Public and Private Insertion Functions
    Yiding Ji, Yi-Chin Wu, Stéphane Lafortune · Automatica, 93, pp. 369–378, 2018 · doi.org/10.1016/j.automatica.2018.03.041
    classical · insertion-functions · opacity
    Show abstractHide abstract
    We study the enforcement of opacity, an information-flow security property, using insertion functions that insert fictitious events at the output of the system. The intruder is characterized as a passive external observer whose malicious goal is to infer system secrets from observed traces of system events. We consider the problems of enforcing opacity under the assumption that the intruder either knows or does not know the structure of the insertion function; we term this requirement as public–private enforceability. The case of private enforceability alone, where the intruder does not know the form of the insertion function, is solved in our prior work. In this paper, we address the stronger requirement of public–private enforceability, that requires opacity be preserved even if the intruder knows or discovers the structure of the insertion function. We formulate the concept of public–private enforceability by defining the notion of public safety. This leads to the notion of public–private enforcing (PP-enforcing) insertion functions. We then identify a necessary and sufficient condition for an insertion function to be PP-enforcing. We further show that if opacity is privately enforceable by the insertion mechanism, then it is also public–private enforceable. Using these results, we present a new algorithm to synthesize PP-enforcing insertion functions by a greedy-maximal strategy. This algorithm is the first of its kind to guarantee opacity when insertion functions are made public or discovered by the intruder.
  • Insertion Functions with Memory for Opacity Enforcement
    Christoforos Keroglou, Laurie Ricker, Stéphane Lafortune · IFAC-PapersOnLine, 51(7), pp. 394–399, 2018 (14th IFAC Workshop on Discrete Event Systems, WODES 2018) · doi.org/10.1016/j.ifacol.2018.06.331
    Not to be confused with the similarly named K-Memory-Embedded Insertion Mechanism paper by Liu, Mei and Lu, which is by a different group.
    classical · insertion-functions · opacity
    Show abstractHide abstract
    We investigate the enforcement of opacity, an information-flow privacy property, using insertion sequences that modify the output of the system by event insertions. Previous work considered the problem of enforcing opacity under the assumption that the insertion functions were based on the observed system strings. Now, we investigate an extension of the previous method introducing a k-memory insertion mechanism. In this case, we store k consecutive events and we compute an insertion function for a k length event sequence. The k-memory insertion mechanism can be applied to a broader class of systems than the previously proposed insertion mechanism. The first contribution of this paper is the introduction of ik-enforceability. A system is ik-enforceable if we can apply k-memory insertion mechanism to enforce privacy. The second contribution of this paper is the development of a verification algorithm for ik-enforceability.
  • Opacity Enforcement Using Nondeterministic Publicly-Known Edit Functions
    Yiding Ji, Xiang Yin, Stéphane Lafortune · IEEE Transactions on Automatic Control, 64(10), pp. 4369–4376, 2019 · doi.org/10.1109/TAC.2019.2897553 · conference version: Yiding Ji, Stéphane Lafortune, "Enforcing Opacity by Publicly Known Edit Functions", 56th IEEE Conference on Decision and Control (CDC 2017) · doi.org/10.1109/CDC.2017.8264378
    classical · insertion-functions · opacity
    Show abstractHide abstract
    This note investigates enforcement of opacity by nondeterministic edit functions. The edit functions alter the system's output by inserting fictitious events or erasing observed events. The edit decisions are randomly made while not known by the outside environment a priori. There is an intruder characterized as a passive observer with malicious goals to infer the secrets of the system. We require that opacity be enforced when the intruder may or may not know the implementation of edit functions. This requirement is termed as private and public safety. We also restrict the operation of edit functions by defining edit constraints. Then, the opacity enforcement problem is transformed to a three-player game among the edit function, the environment, and a dummy player, which helps to determine edit decisions. A game structure called the all edit structure (AES) is introduced to characterize the interaction among those players. It embeds all privately safe edit functions and may also embed publicly safe edit functions. Based on the AES, we present an algorithm that provably synthesizes nondeterministic edit functions that satisfy both private safety and public safety.
  • Enforcing Opacity by Insertion Functions Under Multiple Energy Constraints
    Yiding Ji, Xiang Yin, Stéphane Lafortune · Automatica, 108, article 108476, 2019 · doi.org/10.1016/j.automatica.2019.06.028 · conference version: "Opacity Enforcement by Insertion Functions under Energy Constraints", IFAC-PapersOnLine, 51(7), 2018 · doi.org/10.1016/j.ifacol.2018.06.315
    classical · insertion-functions · opacity
    Show abstractHide abstract
    This paper investigates the enforcement of opacity by insertion functions subject to multiple quantitative constraints capturing resource or energy limitations. There is a malicious intruder attempting to infer secrets of the system from its observations. To prevent the disclosure of secrets, the insertion function inserts fictitious events to the output of the system to obfuscate the intruder. The system is initialized with several types of resources, referred to as energy. The energy is consumed or replenished with event occurrences while always consumed with event insertions. The insertion function must enforce opacity while ensuring that each type of resource is never depleted. This problem is then reduced to a two-player game between the insertion function and the system (environment), with properly defined objectives. A game structure called the Energy Insertion Structure, denoted by EIS is proposed, which provably contains solutions to the energy constrained opacity enforcement problem. Then we further study the bounded cost rate insertion problem on the insertion function’s winning region of EIS, which requires that the long run average rate of insertion cost be bounded. This problem is formulated as a multidimensional mean payoff game and a special method called hyperplane separation technique is applied to efficiently solve it.
  • Embedded Insertion Functions for Opacity Enforcement
    Christoforos Keroglou, Stéphane Lafortune · IEEE Transactions on Automatic Control, 66(9), pp. 4184–4191, 2020 · doi.org/10.1109/TAC.2020.3037891 · conference version: "Verification and Synthesis of Embedded Insertion Functions for Opacity Enforcement", 56th IEEE Conference on Decision and Control (CDC 2017), pp. 4217–4223
    classical · insertion-functions · opacity
    Show abstractHide abstract
    We investigate the enforcement of opacity, an information-flow privacy property, using insertion sequences that modify the output of the system by event insertions. Previous work considered the problem of enforcing the opacity under the assumption that the insertion functions were based on the observed system strings. Now, we investigate the more powerful method of insertion sequences based on the exact system states and events. In this case, the insertion function would be embedded into the system itself, rather than being an output interface. In this article, we develop methods that verify if a valid insertion function exists in this setting; if one exists, synthesize one using a computationally effective algorithm; and investigate a special case where it is possible to verify and synthesize a valid embedded insertion function with polynomial complexity in the size of the system.
  • Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement
    Sahar Mohajerani, Yiding Ji, Stéphane Lafortune · IEEE Transactions on Automatic Control, 65(8), pp. 3349–3364, 2020 · doi.org/10.1109/TAC.2019.2946165 · preprint: arXiv:1910.00417 · conference version: "Efficient Synthesis of Edit Functions for Opacity Enforcement Using Bisimulation-Based Abstractions", 57th IEEE Conference on Decision and Control (CDC 2018), pp. 3573–3578 · doi.org/10.1109/CDC.2018.8619045
    classical · insertion-functions · opacity
    Show abstractHide abstract
    This paper develops a novel compositional and abstraction-based approach to synthesize edit functions for opacity enforcement in modular discrete event systems. Edit functions alter the output of the system by erasing or inserting events in order to obfuscate the outside intruder, whose goal is to infer the secrets of the system from its observation. We synthesize edit functions to solve the opacity enforcement problem in a modular setting, which significantly reduces the computational complexity compared with the monolithic approach. Two abstraction methods called opaque observation equivalence and opaque bisimulation are first employed to abstract the individual components of the modular system and their observers. Subsequently, we propose a method to transform the synthesis of edit functions to the calculation of modular supremal nonblocking supervisors. We show that the edit functions synthesized in this manner correctly solve the opacity enforcement problem.
  • K-Memory-Embedded Insertion Mechanism for Opacity Enforcement
    Rongjian Liu, Liujuan Mei, Jianquan Lu · Systems & Control Letters, 145, article 104785, 2020 · doi.org/10.1016/j.sysconle.2020.104785
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity is a privacy property which aims to determine whether the “secret” of a system can be deduced by an outside intruder. In this paper, we investigate the enforcement of opacity using insertion functions which insert additional events if necessary to modify the output of the system. Inspired by the existing insertion mechanisms, we propose a mechanism named k-memory-embedded insertion mechanism for the enforcement of opacity. In our k-memory-embedded insertion mechanism, the insertion functions are determined based on the knowledge of system’s exact states and the stored next sequence of events with length k. Especially, we define the property of ik-E-enforceability that a k-memory-embedded insertion function needs to satisfy for opacity enforcement, and further construct a verifier to determine whether a given opacity notion of the system is ik-E-enforceable or not. Our mechanism improves the embedded insertion mechanism by applying to a broader class of systems. Also, we improve the k-memory insertion mechanism by requiring a smaller number of consecutive events which need to be stored.
  • Enforcement of K-Step Opacity with Edit Functions
    Andrew Wintenberg, Matthew Blischke, Stéphane Lafortune, Necmiye Ozay · 60th IEEE Conference on Decision and Control (CDC 2021), pp. 331–338 · doi.org/10.1109/CDC45484.2021.9682936
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity is an information flow property for dynamic systems describing plausible deniability, that is whether an eavesdropper can deduce that "secret" behavior has occurred. In particular, K-step opacity considers secret actions that have occurred within the last K-steps in the past. We consider the problem of K-step opacity enforcement over automata using obfuscation. We present a general framework for K-step opacity enforcement and transform the problem of enforcing K-step opacity to enforcing current-state opacity. We can then apply existing obfuscation synthesis methods for current-state opacity to K-step opacity. We demonstrate this approach by enforcing privacy in the context of a novel contact tracing model.
  • Extended Insertion Functions for Opacity Enforcement in Discrete-Event Systems
    Xiaoyan Li, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Transactions on Automatic Control, 67(10), pp. 5289–5303, 2022 · doi.org/10.1109/TAC.2021.3121249
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity is a confidentiality property that holds if certain secret behavior of a system, typically represented by a predicate, cannot be revealed under any system evolution. Among other proposed methodologies, when opacity is violated, it can be enforced using insertion mechanisms, i.e., by inserting symbols before an actual system output (in real time as the system evolves) in order to replace observation sequences that lead to opacity violations with observation sequences that can be generated by system behavior that does not violate opacity. This article focuses on opacity enforcement in discrete-event systems modeled with finite-state automata and proposes an extended insertion mechanism that can enforce opacity in a practical manner to a wide class of systems by inserting symbols before and after an actual system output. This article also introduces event insertion constraints that require only certain specific symbols to be inserted before and after an actual system output. For each case, we obtain a necessary and sufficient condition (based on the construction of an appropriate verifier) for opacity enforceability using the proposed extended insertion mechanism and devise a pertinent extended insertion strategy.
  • Enforcement for Infinite-Step Opacity and K-Step Opacity via Insertion Mechanism
    Rongjian Liu, Jianquan Lu · Automatica, 140, article 110212, 2022 · doi.org/10.1016/j.automatica.2022.110212
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity is an important information-flow property concerning the security and privacy of cyber–physical systems. We investigate the synthesis problem of infinite-step opacity and K-step opacity by using insertion function. An insertion function is a monitoring interface placed between the system and the outside observer that inserts fictitious events to the system output if necessary. To successfully enforce infinite-step opacity and K-step opacity, in this paper, we first review the insertion mechanism without considering the opacity enforcement issue, and propose two new automata for recognizing the safe languages for infinite-step opacity and K-step opacity respectively. Then, we enforce the infinite-step opacity and the K-step opacity with the reviewed insertion mechanism. Computational complexity issues are also discussed. Our results extend the prior results about the synthesis of insertion functions from the notion of current-state opacity to the notions of infinite-step opacity and K-step opacity.
  • Opacity Enforcement via Attribute-Based Edit Functions in the Presence of an Intended Receiver
    Rongjian Liu, Jianquan Lu, Christoforos N. Hadjicostis · IEEE Transactions on Automatic Control, 68(9), pp. 5646–5652, 2022 · doi.org/10.1109/TAC.2022.3220557
    classical · insertion-functions · opacity
    Show abstractHide abstract
    The enforcement of opacity, a security property concerning information-flow, has been investigated using edit functions, which are capable of manipulating the output of the system via insertion, replacement, and erasure operations on its symbols, in order to ensure that an outside observer (the intruder) does not gain access to critical system information. In this article, we consider situations where an intended receiver may be present and develop attribute-based edit functions, which not only obfuscate the output for the intruder, but also allow the intended receiver (who is assumed to have access to specific additional information) to recover the original output behavior. In our developed edit mechanism, edit functions modify the output by only performing insertion or replacement operations under a carefully chosen replacement regulation. Moreover, the outside observer that satisfies the intended-receiver attribute (i.e., the identity of the observer is the intended receiver) is able to recover the unedited output sequence using its ability to distinguish inserted/replaced symbols, and its knowledge of the replacement regulation. We provide an algorithmic procedure, based on a backtracking technique, to obtain suitable replacement regulations for the attribute-based edit function and the intended receiver.
  • Edit Mechanism Synthesis for Opacity Enforcement Under Uncertain Observations
    Wei Duan, Ruotian Liu, Maria Pia Fanti, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Control Systems Letters, 7, pp. 2041–2046, 2023 · doi.org/10.1109/LCSYS.2023.3284340
    classical · insertion-functions · opacity
    Show abstractHide abstract
    This letter addresses the problem of opacity enforcement by using edit functions in discrete event systems modelled as deterministic finite automata under partial observation. The edit function is an output interface of the system that manipulates actual observations to confuse a malicious intruder. We assume that the edit function simply knows whether the intruder observes a larger or smaller set of events than itself, but does not know the exact set of events observed by the intruder. In this uncertain observation setting, the edit function aims to confuse the intruder while relying on its own set of observable events, which requires the edit function to be u-enforcing. The opacity enforcement problem is then transformed to a two-player game between the system and the edit function under partial information. A so-called edit mechanism is proposed in a game scheme to enumerate all possible edited operations following the system behavior. We show that an edit function synthesized from the edit mechanism (if any) can be used to enforce opacity in the system under the uncertain observation setting.
  • Opacity Enforcement in Discrete Event Systems Using Extended Insertion Functions Under Inserted Language Constraints
    Xiaoyan Li, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Transactions on Automatic Control, 68(11), pp. 6797–6803, 2023 · doi.org/10.1109/TAC.2023.3239433
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity is a confidentiality property capturing the fact that certain secret behavior of a system cannot be revealed under any system evolution. Current-state opacity can be enforced by using an extended insertion mechanism, which is capable of inserting fake symbols before and after an actual output, in real time as the system evolves. This article studies the enforcement of current-state opacity for systems modeled by finite state automata using an extended insertion strategy under constraints on the way symbols can be inserted before and after an actual symbol generated by the system (e.g., constraints on the type, order, and number of inserted symbols). More specifically, we consider inserted language constraints captured by the notion of (Lb, La)-enforceability, where Lb is the set of strings that can be inserted before, and La is the set of strings that can be inserted after an observed event. If Lb and La are regular languages, a verifier is constructed to derive a necessary and sufficient condition for opacity enforceability, and also to formulate an extended insertion strategy (if viable).
  • Privacy-Preserving Co-synthesis Against Sensor-Actuator Eavesdropping Intruder
    Ruochen Tai, Liyong Lin, Yuting Zhu, Rong Su · Automatica, 150, article 110860, 2023 · doi.org/10.1016/j.automatica.2023.110860 · preprint: arXiv:2104.14919
    classical · opacity · supervisory-control
    Show abstractHide abstract
    In this work, we investigate the problem of privacy-preserving supervisory control against an external passive intruder via co-synthesis of dynamic mask, edit function, and supervisor for opacity enforcement and requirement satisfaction. We attempt to achieve the following goals: 1) the system secret cannot be inferred by the intruder, i.e., opacity of secrets against the intruder, and the existence of the dynamic mask and the edit function should not be discovered by the intruder, i.e., covertness of dynamic mask and edit function against the intruder; 2) the closed-loop system behaviors should satisfy some safety and nonblockingness requirement. We assume the intruder can eavesdrop both the sensing information generated by the sensors and the control commands issued to the actuators, and we refer to such an intruder as a sensor-actuator eavesdropping intruder. The effectiveness of our approach is illustrated on an example about the enforcement of location privacy for an autonomous vehicle.
  • Opacity Enforcement via Greedy Privately-and-Publicly Known Insertion Functions
    Rongjian Liu, Jianquan Lu, Yang Liu, Xiang Yin, Christoforos N. Hadjicostis · IEEE Transactions on Automatic Control, 69(4), pp. 2500–2506, 2024 · doi.org/10.1109/TAC.2023.3307791
    classical · insertion-functions · opacity
    Show abstractHide abstract
    In this article, we investigate the enforcement of (current-state) opacity, an important information-flow security property, via insertion functions. An insertion function is an obfuscation mechanism that inserts fictitious events to the outputs in order to confuse the outside observer (intruder) such that the secret of the system is not revealed. In some situations, the secret may be revealed when the insertion mechanism is (or becomes) publicly known. This leads to the problem of synthesizing private-and-public enforcing (PP-enforcing) insertion functions in the sense that opacity is still enforced even when the mechanism is discovered or published by the designer. Existing works that have investigated this synthesis problem are either only sound or have limited applicability as we show in this work. For this reason, and more importantly, to better solve the synthesis problem, a new approach is proposed upon an improved greedy criterion. We show that the proposed algorithm is both sound and complete, and can be used to completely solve the synthesis problem for the PP-enforcing insertion function. With slight modifications of our algorithm, infinite-step opacity and K-step opacity can also be enforced under publicly-known insertion mechanisms.
  • Improved Synthesis of Nondeterministic Publicly-Known Edit Functions for Opacity Enforcement
    Rongjian Liu, Christoforos N. Hadjicostis · IEEE Transactions on Automatic Control, 2025 (early access; volume/pages not yet assigned) · ieeexplore.ieee.org/document/10985817
    classical · insertion-functions · opacity
    Show abstractHide abstract
    In this paper, we investigate the synthesis problem of edit functions for opacity enforcement in systems modelled as partially-observed finite-state automata. For better plausible deniability for the edit functions, in cases where the intruder may learn/know their existence, a synthesis problem for nondeterministic edit functions under a publicly-known setting was introduced in the literature, but not yet fully solved. In light of this, we revisit the publicly-known edit mechanism by proposing a sound and complete approach for solving the synthesis problem of nondeterministic publicly-known edit functions. For practical applications, the edit function is assumed to have limited erasure and insertion ability. Our approach is based on a new labelled finite-state structure, and results in wider applicability than previously-proposed in the literature.
  • Obfuscation Mechanism for Simultaneous Public Event Information Release and Private Event Information Hiding in Discrete Event Systems
    Wei Duan, Christoforos N. Hadjicostis, Zhiwu Li · Information Sciences, 690, article 121554, 2025 · doi.org/10.1016/j.ins.2024.121554
    classical · insertion-functions · opacity
    Show abstractHide abstract
    In this paper, we study the problem of simultaneous public event information release and private event information hiding in discrete event systems modeled by partially observed non-deterministic finite automata, where the public and private event information is respectively defined as unobservable fault and secret events. The notion of D-C-compossibility is introduced to characterize whether a system simultaneously conceals the occurrences of secret events while releasing the occurrences of fault events. When such a property does not hold, we investigate its enforcement through a defensive function. This function takes each observable event of a system as input and generates a suitably modified event sequence at the system's output using event deletion, insertion, or substitution. Specifically, our focus is on prioritizing the concealment of the secret events while maximizing the detection of the fault events through the use of defensive functions. The notion of D-C-enforceability that refers to the capability of a defensive function to employ a strategy for manipulating observations of a system to enforce D-C-compossibility is proposed. That is, a D-C-enforcing defensive function ensures that all occurrences of fault events can be revealed while concealing all occurrences of secret events. A D-C-diagnoser construction is proposed to enumerate all feasible defensive actions following system behavior. By taking advantage of the D-C-diagnoser, we obtain a necessary and sufficient condition for D-C-enforceability, along with a corresponding obfuscation strategy for defensive functions.
  • Opacity Enforcement in Discrete Event Systems Using Modification Functions
    Xiaoyan Li, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Transactions on Automation Science and Engineering, 22, pp. 3252–3264, 2025 · doi.org/10.1109/TASE.2024.3391617
    classical · insertion-functions · opacity
    Show abstractHide abstract
    Opacity of a discrete event system is a confidentiality property that characterizes instances when the secret behavior of the system cannot be revealed. This paper considers current-state opacity with respect to a set of secret states, and addresses the opacity enforcement problem via modification functions that are capable of replacing in real-time the output of the underlying system with another output, aiming to prevent the intruder from inferring the secret. We study modification functions that are constrained, i.e., they may not be able to modify certain outputs or they may have restrictions in how they modify a particular output. A system is said to be emc-enforceable if opacity can be enforced via modification functions under the given event modification constraints (emc). To verify whether a system is emc-enforceable, we construct a verifier, based on which a necessary and sufficient condition is obtained. If a system is emc-enforceable, an algorithm is developed to compute a modification strategy based on the verifier to enforce opacity. For m-enforceability, a special case of emc-enforceability without constraints, two necessary and sufficient conditions to verify and enforce opacity with reduced complexity are presented, one based on a system estimator and the other based on a detector. Note to Practitioners—Discrete event systems provide appropriate mathematical models for analysing information-flow properties of cyber-physical systems, such as intelligent transportation systems, command-control systems, and networked communication systems, in dynamically changing environments. Opacity is a general property capable of capturing safe information-flow in a cyber-physical system. This article targets the enforcement of opacity using modification functions that mask the output of the system into another output in a manner that appears consistent to an external observer as the system evolves. The designed modification function can be realized via triggers equipped with digital logic and storage functionality. As an output is generated by a system, a trigger displays a fake output based on the stored real and fake states.

Other enforcement mechanisms

Runtime monitoring, obfuscation-with-utility trade-offs, reordering/deleting observations, and enforcement on models other than plain automata.

  • Enforcement and Validation (at Runtime) of Various Notions of Opacity
    Yliès Falcone, Hervé Marchand · Discrete Event Dynamic Systems, 25(4), pp. 531–570, 2015 · doi.org/10.1007/s10626-014-0196-4 · hal-00987985
    classical · enforcement · opacity
    Show abstractHide abstract
    We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specifically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality.
  • Synthesis of Obfuscation Policies to Ensure Privacy and Utility
    Yi-Chin Wu, Vasumathi Raman, Blake C. Rawlings, Stéphane Lafortune, Sanjit A. Seshia · Journal of Automated Reasoning, 60(1), pp. 107–131, 2018 · doi.org/10.1007/s10817-017-9420-x · conference version: Yi-Chin Wu, Vasumathi Raman, Stéphane Lafortune, Sanjit A. Seshia, "Obfuscator Synthesis for Privacy and Utility", NFM 2016, LNCS vol. 9690, pp. 133–149 · doi.org/10.1007/978-3-319-40648-0_11
    classical · enforcement · opacity
    Show abstractHide abstract
    We consider the problem of privacy enforcement for dynamic systems using the technique of obfuscation. Our approach captures the trade-off between privacy and utility, in a formal reactive framework. Specifically, we model a dynamic system as an automaton or labeled transition system with predefined secret behaviors. The system generates event strings for some useful computation (utility). At the same time, it must hide its secret behaviors from any outside observer of its behavior (privacy). We formally capture both privacy and utility specifications within the model of the system. We propose as obfuscation mechanism for privacy enforcement the use of edit functions that suitably alter the output behavior of the system by inserting, deleting, or replacing events in its output strings. The edit function must hide secret behaviors by making them observationally equivalent to non-secret behaviors, while at the same time satisfying the utility requirement on the output strings. We develop algorithmic procedures that synthesize a correct-by-construction edit function satisfying both privacy and utility specifications. The synthesis procedure is based on the solution of a game where the edit function must react to the system moves by suitable output editing. After presenting an explicit algorithm for solving for the winning strategies of the game, we present two complementary symbolic implementations to address scalability of our methodology. The first symbolic implementation uses a direct encoding of the explicit algorithm using binary decision diagrams (BDDs). The second symbolic implementation reframes the synthesis of edit functions as a supervisory control problem and then applies a recently-developed tool for solving supervisory control problems using BDDs. Experimental results comparing the two symbolic implementations are provided.
  • Enforcing Current-State Opacity Through Shuffle and Deletions of Event Observations
    Raphael J. Barcelos, João Carlos Basilio · Automatica, 133, article 109836, 2021 · doi.org/10.1016/j.automatica.2021.109836 · conference precursor: “Enforcing Current-State Opacity Through Shuffle in Event Observations”, IFAC-PapersOnLine, 51(7), pp. 100–105, 2018 · doi.org/10.1016/j.ifacol.2018.06.286
    classical · enforcement · opacity
    Show abstractHide abstract
    In this paper, we deal with current-state opacity, and propose an Opacity-Enforcer that is able to change, in an appropriate way, the order of observation of event occurrences in the system, and also to delete event observations, so as to mislead the Intruder to never be sure if the current state of the system is a secret state. We then present two necessary and sufficient conditions for the feasibility of current-state opacity enforceability (CSOE), i.e., if a current-state opacity enforcer that shuffles and deletes events can be synthesized for the system, and present an automaton-based verification test for CSOE and an algorithm to build the automaton that realizes the proposed opacity enforcement. We also present a protocol to mitigate the negative effect of opacity enforcement on the capability of a legitimate recipient to accurately estimate the current state of the system in the case when the information is also intended to be sent to some receiver that needs to be aware of the system evolution.
  • A Dynamic Obfuscation Framework for Security and Utility
    Andrew Wintenberg, Matthew Blischke, Stéphane Lafortune, Necmiye Ozay · 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), pp. 236–246 · doi.org/10.1109/ICCPS54341.2022.00028
    classical · enforcement · opacity
    Show abstractHide abstract
    Obfuscation can be used by dynamic systems to ensure private and secure communication over networks vulnerable to eavesdroppers. Balancing the utility of sending information to intended recipients and privacy by hiding information from unintended recipients presents an interesting challenge. We propose a new framework for obfuscation that includes an inference interface to allow intended recipients to interpret obfuscated information. We model the security of the obfuscation with opacity, a formal notion of plausible deniability. Using techniques from distributed reactive synthesis, we show how to automatically design a privacy-enforcing obfuscator along with the inference interface that is given to intended recipients to use as a “key”. We demonstrate this approach by enforcing privacy while maintaining utility in a contact tracing model.
  • Enforcement of Current-State Opacity in Signal Interpreted Petri Nets
    Andreas Köhler, Pascal Marijan, Ping Zhang · IEEE Transactions on Automatic Control, 69(11), pp. 8104–8111, 2024 · doi.org/10.1109/TAC.2024.3412008
    classical · enforcement · opacity
    Show abstractHide abstract
    This article proposes a new approach for the enforcement of current-state opacity in signal interpreted Petri nets (SIPN). In order to enforce current-state opacity in SIPNs, the properties of iterative firing and simultaneous firing of transitions are considered. To prevent the intruder from inferring the current marking, signals associated with the secret marking are compared to signals associated with alternative markings. This allows to determine which signals need to be encrypted to confuse the secret marking with markings leading to the secret marking, markings directly reachable from the secret marking or markings reachable from the premarking of the secret marking. The proposed approach applies to any system that can be described by an SIPN.
  • Integrating Obfuscation and Control for Privacy
    Andrew Wintenberg, Necmiye Ozay, Stéphane Lafortune · IEEE Transactions on Automatic Control, 2025 · doi.org/10.1109/TAC.2025.3564221
    classical · enforcement · opacity
    Show abstractHide abstract
    Networked systems must often balance privacy in avoiding leaking sensitive information, with utility in communicating the information that is needed by components to operate correctly. We consider the problem of enforcing privacy and utility with both obfuscation (altering communications to mislead eavesdroppers) and control (restricting system behavior to avoid information leakage). We present a formulation of this problem that models components of the networked system as interconnected reactive processes. Tools from distributed reactive synthesis are then used to automatically design obfuscators and controllers, which coordinate to enforce requirements. In particular, we develop formal specifications capturing privacy using the information flow property of opacity and utility ensuring availability of information or imposing constraints on the closed-loop system. This synthesis approach is applicable to a large class of network architectures, which we demonstrate on three representative problems over a building access control system.
  • Protect Your Knowledge: Epistemic Property Enforcement of Discrete Event Systems with Asymmetric Information
    Shaowen Miao, Bohan Cui, Yiding Ji, Xiang Yin · IEEE Control Systems Letters, 9, pp. 1832–1837, 2025 · doi.org/10.1109/LCSYS.2025.3578993
    classical · enforcement · opacity
    Show abstractHide abstract
    Many property verification and enforcement problems of partially observed discrete event systems (DES) are typically addressed solely from the outside observer’s perspective. However, systems may be monitored not only by a designated observer but also by a potentially malicious intruder when deployed in complex and open environments. The observer infers the information of the system based on its observation, which is referred to as knowledge. In addition, the intruder not only eavesdrops on the system’s behaviors but also attempts to infer the observer’s knowledge from its own observation. Notably, the information flow from the system to the observer and the intruder is asymmetric, resulting in incomparable observable events for each agent. Such an inference scenario is formalized as the epistemic property. This letter addresses the enforcement of the epistemic property in a partially observed DES through supervisory control. Specifically, we propose a game-theoretic framework to reflect the interaction between the observer/supervisor, the intruder, and the environment. A bipartite structure named all-protect structure is constructed as the game area, from which we solve the game and synthesize maximally permissive controllable and observable supervisors to provably enforce the properties.
  • Opacity Enforcement in Discrete Event Systems Using Differential Privacy
    Jie Zhang, Yifan Dong, Li Yin, Almetwally M. Mostafa, Zhiwu Li · Information Sciences, 688, article 121284, 2025 · doi.org/10.1016/j.ins.2024.121284
    classical · enforcement · opacity
    Show abstractHide abstract
    Opacity is an important information security property that characterizes whether the secret of a system can be inferred by an intruder who can partially observe the behavior of the system. In this paper, we touch upon the enforcement of the current-state opacity and initial-state opacity of discrete event systems modeled by automata. Specifically, given a partially observed discrete event system that is not current-state opaque (resp., initial-state opaque), by observing the system's behavior, the intruder stands a chance to infer that the current state (resp., initial state) is within the secret of the system. To prevent the exposure of secret information, we introduce a differential privacy mechanism to enforce a non-opaque system to be opaque. Particularly, the designed mechanism is settled to receive the observations of the system. Suppose that there are two observations such that one of them can lead to the exposure of the secret and the other is randomly observed. When the two observations are received by the designed mechanism that provides differential privacy, a randomly modified output with an approximate probability is exported, exposing to the intruder. In this way, since the observation from which the secret can be inferred by the intruder, is befuddled with one randomly generated by the system, he/she is not able to deduce which one is truly generated and received by the mechanism, even if the probabilistic generation rule of the mechanism is public.
  • Enforcing Current-State Opacity and Utility of Cyber-Physical Systems Using Multipath Event Routing
    Lucas N. R. Reis, Lilian K. Carvalho, Marcos V. Moreira · IEEE Transactions on Automatic Control, 71(6), pp. 4208–4214, 2026 · doi.org/10.1109/TAC.2026.3653255
    classical · continuous · distributed · enforcement · opacity
    Show abstractHide abstract
    Several strategies have been proposed in the literature to ensure data security in cyber-physical systems abstracted as networked discrete-event systems, such as enforcing opacity by using obfuscation policies. In these cases, if it is considered the existence of an intended receiver, the useful information can be hidden from him/her. This problem becomes worse when the confidentiality of the data must be ensured, i.e., when the intended receiver must always know the system current state from the observation of the obfuscated transmitted sequence. In this article, we propose a defense strategy to enforce current-state opacity using an obfuscation policy based on event replacements that also ensures the utility of the transmitted information. The notion of utility used, called current-state utility, is associated with the ability of the intended receiver to be always certain of the system current state. In order to implement the defense strategy, a multipath event routing technique is considered.

Active / adversarial intruders

Everywhere else on this page, the intruder is passive: it only watches. Here the intruder is itself a controller, able to influence the system (inject inputs, tamper with sensors) while trying to defeat opacity.

  • Opacity of Discrete Event Systems with Active Intruder
    Alireza Partovi, Taeho Jung, Hai Lin · arXiv:2007.14960, 2020 · arXiv:2007.14960
    adversarial-intruders · classical · opacity
    Show abstractHide abstract
    Opacity is a security property formalizing the information leakage of a system to an external observer, namely intruder. The conventional opacity that has been studied in the Discrete Event System (DES) literature usually assumes passive intruders, who only observe the behavior of the system. However, in many cybersecurity concerns, such as web service, active intruders, who are capable of influencing the system's behavior beyond passive observations, need to be considered and defended against. We are therefore motivated to extend the opacity notions to handle active intruders. For this, we model the system as a non-deterministic finite-state transducer. It is assumed that the intruder has a full knowledge of the system structure and is capable of interacting with the system by injecting different inputs and observing its responses. In this setup, we first introduce reactive current-state opacity (RCSO) notion characterizing a property that the system does not leak its secret state regardless of how the intruder manipulates the system behavior. We furthermore extend this notion to language-based and initial-state reactive opacity notions, and study the relationship among them. It turns out that all the proposed reactive opacity notions are equivalent to RCSO. We therefore focus on RCSO and study its verification problem. It is shown that the RCSO can be verified by constructing an observer automaton.
  • Synthesis of Opacity-Enforcing Winning Strategies Against Colluded Opponent
    Chongyang Shi, Abhishek N. Kulkarni, Hazhar Rahmani, Jie Fu · 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 7240–7246, 2023 · doi.org/10.1109/CDC49753.2023.10384109 · preprint: arXiv:2304.01286
    adversarial-intruders · classical · opacity
    Show abstractHide abstract
    This paper studies language-based opacity enforcement in a two-player, zero-sum game on a graph. In this game, player 1 (P1) wins if he can achieve a secret temporal goal described by the language of a finite automaton, no matter what strategy the opponent player 2 (P2) selects. In addition, P1 aims to win while making its goal opaque to a passive observer with imperfect information. However, P2 colludes with the observer to reveal P1's secret whenever P2 cannot prevent P1 from achieving its goal, and therefore, opacity must be enforced against P2. We show that a winning and opacity-enforcing strategy for P1 can be computed by reducing the problem to solving a reachability game augmented with the observer's belief states. Furthermore, if such a strategy does not exist, winning for P1 must entail the price of revealing his secret to the observer. We demonstrate our game-theoretic solution of opacity-enforcement control through a small illustrative example and in a robot motion planning problem.
  • Opacity Enforcing Supervisory Control with a Priori Unknown Supervisors
    Bohan Cui, Ziyue Ma, Alessandro Giua, Xiang Yin · arXiv:2604.04070, 2026 · arXiv:2604.04070
    adversarial-intruders · classical · opacity
    Show abstractHide abstract
    We investigate the enforcement of opacity in discrete-event systems via supervisory control. A system is said to be opaque if a passive intruder can never unambiguously infer whether the system is in a secret state through its observations. In this context, the intruder's knowledge about the supervisor plays a critical role in both problem formulation and solvability. Existing studies typically assume that the policy of the supervisor is either fully unknown to the intruder or fully known a priori, the latter leading to severe technical challenges and unresolved problems under incomparable observations. This paper investigates opacity supervisory control under a new intermediate information setting, which we refer to as the a priori unknown supervisor setting. In this setting, the supervisor's internal realization is not publicly available, but the intruder can partially infer its behavior by eavesdropping on the control decisions issued online during system execution. We formalize the intruder's information-flow under both observation-triggered and decision-triggered decision-issuance mechanisms and define the corresponding notions of opacity. We provide sound and complete algorithms for synthesizing opacity-enforcing supervisors without imposing any restrictions on the observable or controllable event sets. By constructing an information-state structure that embeds the supervisor's estimate of the intruder's belief, the synthesis problem is reduced to a safety game. Finally, we show that, under strictly finer intruder observations, the proposed setting coincides with the standard a priori known supervisor model.
C

Applications & Case Studies

Where opacity gets applied to a concrete domain: mobile agent trajectories, location privacy, web services, and the sensor-deception line of work, which flips the usual defender's-eye framing around.

D

Surveys & Overviews

Surveys and reference works that cover opacity broadly rather than contributing a single new result.