Opacity综述

中文版

本文根据关于 Discrete Event Systems 中 Opacity 的手写阅读笔记整理，所参考的综述由 Jacob et al. 撰写，发表于 Annual Reviews in Control。笔记涉及 Models、Validation 和 Quantification。

研究背景

Network Communication 与 Online Services 中的 Security 和 Privacy 需求推动了 Information Flow 研究，也促使研究者发展相关理论，以设计满足 Opacity 的系统。相关概念包括 Anonymity、Non-interference、Secrecy、Privacy、Security 和 Opacity。

Opacity 用于描述系统如何保护 Secret：对于每一种 Secret Behavior，都存在至少一种在 Intruder 看来完全相同的 Non-secret Behavior。 因此，Intruder 无法仅凭 Observation 断定 Secret 已经发生。

这里假设 Intruder 完全了解系统的 Model，但对系统行为仅具有 Partial Observability，并根据获得的 Observation 估计系统的实际情况。当 Secret Behavior 与 Non-secret Behavior 产生相同的 Observation 时，后者便为前者提供了掩护。

笔记记录的综述内容包括：

• Logical Models 中的 Opacity Validation。
• Probabilistic Models 中的 Opacity Quantification 与 Information Leakage 风险。
• Decidability 和 Complexity 结果。
• 已有 Verification Tools，以及工具是否支持 Quantification 的问题。
• Discrete Event Systems 中的应用与未来研究方向。

Logical Models 通常回答系统是否满足 Opacity；Probabilistic Models 则用于衡量 Information Leakage 风险。

Opacity 的发展脉络

手稿记录的研究进展	作者线索
在 Computer Science 中引入 Opacity，用于分析 Cryptographic Protocols	Mazaré (2004)
在 Discrete Event Systems 的 Petri Net Models 中研究 Opacity	Bryans, Koutny, and Ryan (2005)
扩展到 Labeled Transition Systems（LTS），将 Secret 定义为 Run 上的 Predicate	Bryans, Koutny, Mazaré, and Ryan (2008)
在 Finite-State Automata 中研究 State-Based Opacity	Saboori and Hadjicostis (2007); Saboori (2011)

Cassandras and Lafortune (2008) 是了解 DES 背景的良好参考。

综述结构

原综述的章节安排如下：

• 第 2、3 节介绍记号与定义。
• 第 4 节讨论 Validation Methods。
• 第 5 节介绍 Probabilistic Models。
• 第 6 节讨论 Decidability 与 Complexity。
• 第 7、8 节介绍应用与未来研究方向。

基本记号

下文采用手稿中的 Automaton 记号：

$$G=(X,E,f,X_0).$$

• $X$：State Set。
• $E$：Event Set。
• $f$：Transition Function，同时定义其在 Event String 上的扩展。
• $X_0\subseteq X$：可能的 Initial State Set。
• $\mathcal L(G,i)$：从 State $i$ 出发能够发生的 Event String 集合。
• $\mathcal L(G,X_0)$：从某个 Initial State 出发能够发生的 Event String 集合。
• $E_o\subseteq E$：Observable Event Set。
• $P:E^*\to E_o^*$：Natural Projection，用于删除 Unobservable Event。

若 $P(t)=P(t')$，Intruder 就无法通过 Observation 区分 Event String $t$ 与 $t'$。符号 $\varepsilon$ 表示 Empty String。

Opacity 的定义主要分为 Language-Based Opacity 和 State-Based Opacity 两类。

Language-Based Opacity

Language-Based Opacity（LBO）也称 Trace-Based Opacity，以一组 Event String 表示 Secret，而非以单个 State 表示。

笔记提到了 Badouel et al. (2007)、Dubreil et al. (2008) 和 Lin (2011) 的研究。Lin 的表述使用两个 Sublanguage。

设

$$L_S\subseteq\mathcal L(G,X_0),\qquad L_{NS}\subseteq\mathcal L(G,X_0)$$

分别表示 Secret Language 和 Non-secret Language。

Strong Opacity

系统满足 Strong LBO，当且仅当

$$\forall t\in L_S,\quad \exists t'\in L_{NS}:\quad P(t)=P(t').$$

等价地，

$$L_S\subseteq P^{-1}\bigl(P(L_{NS})\bigr),$$

也可写成

$$P(L_S)\subseteq P(L_{NS}).$$

也就是说，每个 Secret String 都有一个产生相同 Observation 的 Non-secret String。通常，未作特别说明的 LBO 指 Strong Opacity。

Weak Opacity

系统满足 Weak LBO，当且仅当

$$\exists t\in L_S,\quad \exists t'\in L_{NS}:\quad P(t)=P(t').$$

等价地，

$$L_S\cap P^{-1}\bigl(P(L_{NS})\bigr)\ne\varnothing.$$

Weak Opacity 只要求至少一个 Secret String 存在 Non-secret String 作为掩护，并不保证所有 Secret Behavior 都受到保护。

No Opacity

手稿将以下情形称为 No Opacity：

$$L_S\cap P^{-1}\bigl(P(L_{NS})\bigr)=\varnothing.$$

此时，任何 Secret String 都无法找到产生相同 Observation 的 Non-secret String。

例子：Secret Language 的选择会影响结论

手稿中的 Automaton 如下，Initial State 为 $0$：

取 $E_o=\{a,b,c\}$，因此 $d$ 为 Unobservable Event。

当

$$L_S=\{abd\},\qquad L_{NS}=\{abc^nd\mid n\ge0\}\cup\{adb\},$$

有

$$P(abd)=ab=P(adb).$$

由于 Secret String $abd$ 有 Non-secret String $adb$ 作为掩护，因此满足 LBO。

如果改为

$$L_S=\{abcd\},\qquad L_{NS}=\{adb,abd\}\cup\{abc^nd\mid n\ge2\},$$

则

$$P(abcd)=abc,\qquad P(adb)=P(abd)=ab.$$

其余 Non-secret String 产生的 Observation 为 $abc^n$，其中 $n\ge2$，也不同于 $abc$。因此不满足 LBO。

即使 Automaton 与 Observation Projection 相同，选择不同的 Secret Language 和 Non-secret Language，也可能得到不同的 Opacity 结论。

手稿第 4 页第二个例子中，Non-secret Language 的写法与后续 Observation 计算不一致。这里依据后续的 $abcc^*$ 计算，将相关 Event String 限定为至少包含两个 $c$。如果 Non-secret Language 包含 $abcd$，该串就能为自身提供掩护，原稿预期的反例便不成立。

State-Based Opacity

State-Based Opacity（SBO）以 State、Initial State，或 Initial State 与 Final State 的组合表示 Secret。

Current-State Opacity

Current-State Opacity（CSO）用于隐藏系统当前是否处于 Secret State。

设 $X_S\subseteq X$ 和 $X_{NS}\subseteq X$ 分别为 Secret State Set 与 Non-secret State Set。每条到达 Secret State 的 Execution，都必须有一条产生相同 Observation、但到达 Non-secret State 的 Execution 与之对应：

$$\begin{aligned} &\forall i\in X_0,\ \forall t\in\mathcal L(G,i),\quad f(i,t)\in X_S\\ &\qquad\Longrightarrow \exists j\in X_0,\ \exists t'\in\mathcal L(G,j):\\ &\qquad\qquad f(j,t')\in X_{NS}\ \land\ P(t)=P(t'). \end{aligned}$$

作为掩护的 Execution 可以从另一个 Initial State 出发，但必须产生相同的 Observation，并结束于 Non-secret State。

手稿还提到 always opacity / total opacity：对于所考虑的一组 Run，每个访问到的 State 都应满足相应的 Current-State Opacity。原稿没有进一步给出形式化定义。

例子。 以下 Automaton 的 Initial State 为 $0$：

令 $X_S=\{3\}$，其余 State 为 Non-secret State。

• 若 $E_o=\{b\}$，则 $P(ab)=P(cb)=b$。到达 Secret State $3$ 的 Execution 与到达 Non-secret State $4$ 的 Execution 无法通过 Observation 区分，因此满足 CSO。
• 若 $E_o=\{a,b\}$，则 Observation $ab$ 足以确定系统到达了 Secret State $3$，因此不满足 CSO。

可见，Opacity 也取决于 Intruder 的 Observability。

Initial-State Opacity

Initial-State Opacity（ISO）用于隐藏系统是否从 Secret State 开始运行。

这里，$X_S$ 与 $X_{NS}$ 分别表示需要比较的 Secret Initial State Set 和 Non-secret Initial State Set。ISO 的定义为

$$\forall i\in X_S,\ \forall t\in\mathcal L(G,i),\quad \exists j\in X_{NS},\ \exists t'\in\mathcal L(G,j):\quad P(t)=P(t').$$

从 Secret Initial State 出发产生的每一种 Observation，都必须也能从某个 Non-secret Initial State 出发产生。

例子。 手稿中的 Automaton 如下，其中 $\tau$ 为 Unobservable Event，$E_o=\{a,b\}$：

若 $2$ 为 Secret Initial State，且 $0$ 是允许的 Non-secret Initial State，则从 $2$ 出发的任意 Execution 都有掩护：从 $0$ 出发，先通过 Unobservable Event $\tau$ 到达 $2$，再沿同一 Execution 继续。两者产生相同的 Observation，因此对于手稿比较的 Initial State Set，系统满足 ISO。

若改为将 $0$ 设为 Secret Initial State，则 Observation $aa$ 只能由从 $0$ 出发的 Execution 产生。其余 State 必须经过 Observable Event $b$，才能再次产生 $a$，因而无法产生连续两个 $a$ 的 Observation。当其他 State 为 Non-secret Initial State 时，系统不满足 ISO。

此例比较了多个可能的 Initial State。不能将图中指向 $0$ 的 Initial Arrow 理解为仅允许 $0$ 作为 Initial State；这种理解会排除笔记中使用的、从 $2$ 出发的 Secret Execution。

Initial-and-Final-State Opacity

Initial-and-Final-State Opacity（IFO）用于隐藏 Initial State 与 Final State 的组合信息。手稿将这一概念关联到 Wu and Lafortune (2013)。

设 Secret State Pair Set 与 Non-secret State Pair Set 分别为

$$X_{SP}\subseteq X_0\times X,\qquad X_{NSP}\subseteq X_0\times X.$$

定义为

$$\begin{aligned} &\forall (x_0,x_f)\in X_{SP},\quad \forall t\in\mathcal L(G,x_0),\quad f(x_0,t)=x_f\\ &\qquad\Longrightarrow \exists (x_0',x_f')\in X_{NSP},\quad \exists t'\in\mathcal L(G,x_0'):\\ &\qquad\qquad f(x_0',t')=x_f'\ \land\ P(t)=P(t'). \end{aligned}$$

作为掩护的 Event String $t'$ 必须从对应的 Initial State $x_0'$ 出发。原稿在这一位置漏写了撇号，整理时已修正。

ISO 和 CSO 可以视为 IFO 的特殊情形：

• 若 $X_{SP}=X_S\times X$，$X_{NSP}=X_{NS}\times X$，其中 $X_S,X_{NS}\subseteq X_0$，只限制 Initial State，得到 ISO。
• 若 $X_{SP}=X_0\times X_S$，$X_{NSP}=X_0\times X_{NS}$，只限制 Final State，得到 CSO。

K-step Opacity

原稿第 7 页仅写出了“K-step Opacity”的标题，没有给出定义、公式或例子，暂留待补充。

Verification 与保障 Opacity

给定系统 $G$、Secret 和 Intruder 获取 Observation 的方式，需要回答两个问题：系统是否满足所要求的 Opacity？若不满足，如何使其满足？

手稿列出了三种主要方法：

方法	目的	手稿中的描述
Verification	判断系统是否满足 Opacity	对 Opacity 性质进行 Model Checking
Supervisory Control Theory（SCT）	限制系统行为以保护 Secret	通过约束系统允许发生的行为维持 Opacity
Enforcement	在 Observation 的输入与输出环节保障 Opacity	手稿写到“输入 Observable Events，输出修改后的信息”后中断

4.1 Verification

Opacity Verification $\iff$ Universality Problem，这一结论由 Cassez, Dubreil & Marchand, 2012 给出。

此外，通过对 Opacity Properties 进行编码，可以将求解归约为经典的 Model-Checking 方法与工具。

4.2 SCT

核心问题是构造特定类型的 Supervisor。Supervisor 用于控制 Controllable Events，以保护 Secret。

这篇综述没有给出 Mathematical Definition。

4.3 Enforcement（Non-intrusive）

主要有三种方法：

• 从输出中删除 Event 的出现；
• 向输出中添加 Event；
• 延迟输出。

这篇综述同样没有给出 Mathematical Definition。

尚待补充的内容

这份手稿主要介绍研究背景、LBO 和几类 SBO 的定义。以下主题虽已提及，但尚未展开：

• K-step Opacity 的正式定义与例子。
• Verification Algorithms 及工具。
• Enforcement 的具体输入、输出和处理机制。
• Probabilistic Models 中的 Opacity Quantification。
• Decidability 与 Complexity 结果。
• 应用案例与未来研究方向。

完整英文文献及链接已补充至文末 References。

核心问题是：Secret 如何定义、Intruder 能观察到什么，以及是否存在 Observation 相同的 Non-secret Explanation。

---

English Version

This article is organized from handwritten reading notes on a review of Opacity in Discrete Event Systems by Jacob et al., published in Annual Reviews in Control. The notes concern models, validation, and quantification.

Background

Security and privacy concerns in network communication and online services motivate research on information flow, and some theories are proposed to design opaque system. Related concepts include anonymity, non-interference, secrecy, privacy, security, and opacity.

Opacity describes the protection of secrets: every secret behavior has a non-secret behavior that looks identical to the intruder. Consequently, the intruder cannot conclude from the observation alone that the secret has occurred.

The intruder is assumed to know the complete system model but to have only partial observability of its behavior. It constructs estimates of the system from observations. When secret and non-secret behaviors produce the same observation, the non-secret behavior provides a cover for the secret.

The review topics recorded in the notes include:

• Opacity validation in logical models.
• Opacity quantification and information leakage risk in probabilistic models.
• Decidability and complexity results.
• Existing verification tools and whether they also support quantification.
• Applications in discrete event systems and future research directions.

Logical models usually answer whether the system is opaque; probabilistic models quantify information leakage risk.

Historical Development of Opacity

Development recorded in the manuscript	Author clues
Opacity introduced in computer science to analyze cryptographic protocols	Mazaré (2004)
Opacity investigated in Petri net models of discrete event systems	Bryans, Koutny, and Ryan (2005)
Extension to labeled transition systems(LTS), with secrets defined as predicates over runs	Bryans, Koutny, Mazaré, and Ryan (2008)
State-based opacity investigated in finite-state automata	Saboori and Hadjicostis (2007); Saboori (2011)

Cassandras and Lafortune (2008) is a very good guidance for DES background.

Review Structure

It records the review structure as follows:

• Sections 2 and 3 introduce notation and definitions;
• Section 4 discusses validation methods;
• Section 5 covers probabilistic models;
• Section 6 addresses decidability and complexity;
• Sections 7 and 8 concern applications and future research.

Basic Notation

The automaton notation used in the manuscript is

$$G=(X,E,f,X_0).$$

• $X$: the state set.
• $E$: the event set.
• $f$: the transition function, extended to event strings.
• $X_0\subseteq X$: the set of possible initial states.
• $\mathcal L(G,i)$: the set of event strings executable from state $i$.
• $\mathcal L(G,X_0)$: the set of event strings executable from some initial state.
• $E_o\subseteq E$: the observable event set.
• $P:E^*\to E_o^*$: the natural projection that erases unobservable events.

If $P(t)=P(t')$, the intruder cannot distinguish event strings $t$ and $t'$ through observation. The symbol $\varepsilon$ denotes the empty string.

Opacity definitions are mainly divided into language-based opacity and state-based opacity.

Language-Based Opacity

Language-Based Opacity (LBO), also called trace-based opacity, represents secrets as a set of event strings rather than as individual states.

The notes mention work by Badouel et al. (2007), Dubreil et al. (2008), and Lin (2011). Lin’s formulation uses two sublanguages. Let

$$L_S\subseteq\mathcal L(G,X_0),\qquad L_{NS}\subseteq\mathcal L(G,X_0)$$

denote the secret and non-secret languages, respectively.

Strong Opacity

The system satisfies strong LBO if and only if

$$\forall t\in L_S,\quad \exists t'\in L_{NS}:\quad P(t)=P(t').$$

Equivalently,

$$L_S\subseteq P^{-1}\bigl(P(L_{NS})\bigr),$$

or

$$P(L_S)\subseteq P(L_{NS}).$$

Every secret string therefore has a non-secret string with the same observation. Unless otherwise qualified, LBO usually refers to this strong version.

Weak Opacity

The system satisfies weak LBO if and only if

$$\exists t\in L_S,\quad \exists t'\in L_{NS}:\quad P(t)=P(t').$$

Equivalently,

$$L_S\cap P^{-1}\bigl(P(L_{NS})\bigr)\ne\varnothing.$$

The weak version requires only one secret string to have a non-secret cover. It does not ensure protection for all secret behaviors.

No Opacity

The manuscript labels the following case “no opacity”:

$$L_S\cap P^{-1}\bigl(P(L_{NS})\bigr)=\varnothing.$$

No secret string then shares an observation with a non-secret string.

Example: The Choice of Secret Language Matters

The automaton in the manuscript has initial state $0$ and the following transitions:

Take $E_o=\{a,b,c\}$, so that $d$ is unobservable. For

$$L_S=\{abd\},\qquad L_{NS}=\{abc^nd\mid n\ge0\}\cup\{adb\},$$

we have

$$P(abd)=ab=P(adb).$$

LBO holds because the secret string $abd$ has the non-secret cover $adb$.

If instead

$$L_S=\{abcd\},\qquad L_{NS}=\{adb,abd\}\cup\{abc^nd\mid n\ge2\},$$

then

$$P(abcd)=abc,\qquad P(adb)=P(abd)=ab.$$

The remaining non-secret strings have observations $abc^n$ with $n\ge2$, which also differ from $abc$. LBO therefore fails.

The same automaton and observation projection can yield different results for different secret and non-secret languages.

In the second example on manuscript page 4, the written non-secret language conflicts with the subsequent observation calculation. Following the later $abcc^*$ calculation, the example above uses strings containing at least two occurrences of $c$. If the non-secret language included $abcd$, that string would cover itself, and the intended counterexample would fail.

State-Based Opacity

State-Based Opacity (SBO) represents secrets through states, initial states, or combinations of initial and final states.

Current-State Opacity

Current-State Opacity (CSO) protects the information that the system is currently in a secret state.

Let $X_S\subseteq X$ be the secret state set and $X_{NS}\subseteq X$ the non-secret state set. Every execution reaching a secret state must have an execution with the same observation that reaches a non-secret state:

$$\begin{aligned} &\forall i\in X_0,\ \forall t\in\mathcal L(G,i),\quad f(i,t)\in X_S\\ &\qquad\Longrightarrow \exists j\in X_0,\ \exists t'\in\mathcal L(G,j):\\ &\qquad\qquad f(j,t')\in X_{NS}\ \land\ P(t)=P(t'). \end{aligned}$$

The alternative execution may start from another initial state. Its observation must be identical, and its final state must be non-secret.

The manuscript also mentions always opacity / total opacity: requiring the corresponding current-state opacity at every visited state over a considered set of runs. It does not formalize this concept further.

Example. The initial state is $0$, with transitions

Let $X_S=\{3\}$; all other states are non-secret.

• If $E_o=\{b\}$, then $P(ab)=P(cb)=b$. The execution reaching secret state $3$ is covered by the execution reaching non-secret state $4$, so CSO holds.
• If $E_o=\{a,b\}$, observing $ab$ identifies state $3$, so CSO fails.

Opacity thus also depends on the intruder’s observability.

Initial-State Opacity

Initial-State Opacity (ISO) protects the information that the system started from a secret state.

Here $X_S$ and $X_{NS}$ denote the secret and non-secret initial state sets being compared. The definition is

$$\forall i\in X_S,\ \forall t\in\mathcal L(G,i),\quad \exists j\in X_{NS},\ \exists t'\in\mathcal L(G,j):\quad P(t)=P(t').$$

Every observation produced from a secret initial state must also be producible from some non-secret initial state.

Example. The manuscript gives the following transitions, where $\tau$ is unobservable and $E_o=\{a,b\}$:

If state $2$ is the secret initial state and $0$ is an allowed non-secret initial state, every execution from $2$ is covered by an execution from $0$ that first takes the unobservable $\tau$ transition to $2$ and then follows the same execution. ISO holds for the initial state sets compared in the manuscript.

If initial state $0$ is instead secret, the observation $aa$ can only arise from an execution starting at $0$. Other states cannot produce two consecutive occurrences of $a$ without an observable $b$. ISO therefore fails when the other states are the non-secret initial states.

This example compares multiple possible initial states. The initial arrow pointing to $0$ in the drawing cannot be interpreted as allowing only $0$ as an initial state; that interpretation would exclude the secret executions starting from $2$ used in the notes.

Initial-and-Final-State Opacity

Initial-and-Final-State Opacity (IFO) protects combinations of initial and final states. The manuscript associates this concept with Wu and Lafortune (2013).

Let the secret and non-secret state-pair sets be

$$X_{SP}\subseteq X_0\times X,\qquad X_{NSP}\subseteq X_0\times X.$$

The definition is

$$\begin{aligned} &\forall (x_0,x_f)\in X_{SP},\quad \forall t\in\mathcal L(G,x_0),\quad f(x_0,t)=x_f\\ &\qquad\Longrightarrow \exists (x_0',x_f')\in X_{NSP},\quad \exists t'\in\mathcal L(G,x_0'):\\ &\qquad\qquad f(x_0',t')=x_f'\ \land\ P(t)=P(t'). \end{aligned}$$

The alternative string $t'$ must start from the alternative initial state $x_0'$. The manuscript omits the prime at the corresponding location; it has been made consistent here.

ISO and CSO can be viewed as special cases of IFO:

• Setting $X_{SP}=X_S\times X$ and $X_{NSP}=X_{NS}\times X$, where $X_S,X_{NS}\subseteq X_0$, restricts only the initial state and yields ISO.
• Setting $X_{SP}=X_0\times X_S$ and $X_{NSP}=X_0\times X_{NS}$ restricts only the final state and yields CSO.

K-step Opacity

Page 7 of the manuscript contains only the heading “K-step Opacity,” with no definition, formula, or example. This topic remains to be completed.

Verifying and Ensuring Opacity

Given a system $G$, a secret, and the intruder’s observation mechanism, two questions arise: does the system satisfy the required opacity property, and, if it does not, how can it be made to satisfy that property?

The manuscript identifies three main approaches:

Approach	Purpose	Description in the manuscript
Verification	Determine whether the system satisfies opacity	Model checking of opacity properties
Supervisory Control Theory (SCT)	Restrict system behavior to protect secrets	Constrain possible system behaviors to preserve opacity
Enforcement	Ensure opacity between observation inputs and outputs	The manuscript stops after “input observable events, output modified information”

4.1 Verification

opacity verification $\iff$ universality problem, this is stated by Cassez, Dubreil & Marchand, 2012.

Also, by encoding the opacity properties, the solutions can be reduced to classical model-checking approaches and tools.

4.2 SCT

The core problem is construct specific types of supervisor. Supervisor is used to controll the controllable events to protect the secrets.

Mathematical definition is not mentioned in this review.

4.3 Enforcement(non-intrusive)

There are three main approaches:

• deleting occurrences of events from the output;
• adding events to output;
• delaying the output;

Mathematical definition is also not mentioned in this review.

Topics Still to Be Completed

The manuscript mainly covers background, LBO, and several SBO definitions. It mentions but does not develop the following topics:

• Formal definitions and examples of K-step opacity.
• Verification algorithms and tools.
• The specific inputs, outputs, and mechanisms of enforcement.
• Opacity quantification in probabilistic models.
• Decidability and complexity results.
• Applications and future research directions. Complete English references and links are provided below.

The central questions are how the secret is defined, what the intruder can observe, and whether a non-secret explanation with the same observation exists.

---

References

These references are shared by the Chinese and English versions. Titles, author names, and publication venues are retained in English. Bibliographic information missing from the handwritten manuscript has been supplemented from the linked sources.

1. Jacob, R., Lesage, J.-J., and Faure, J.-M. (2016). Overview of discrete event systems opacity: Models, validation, and quantification. Annual Reviews in Control, 41, 135-146. Author’s bibliographic record.

2. Mazaré, L. (2004). Using Unification For Opacity Properties. Verimag Technical Report, TR-2004-24. The report identifies a conference version in the Workshop on Issues in the Theory of Security (WITS’04). The linked report is an English original supplied by the author’s institution.

3. Bryans, J. W., Koutny, M., and Ryan, P. Y. A. (2005). Modelling Opacity Using Petri Nets. Electronic Notes in Theoretical Computer Science, 121, 101-115. Institutional full text.

4. Bryans, J. W., Koutny, M., Mazaré, L., and Ryan, P. Y. A. (2008). Opacity generalised to transition systems. International Journal of Information Security, 7(6), 421-435. Institutional publication record. This is the 2008 journal article, distinct from the earlier conference chapter with the same title.

5. Saboori, A., and Hadjicostis, C. N. (2007). Notions of security and opacity in discrete event systems. Proceedings of the 46th IEEE Conference on Decision and Control, 5056-5061.

6. Saboori, A. (2011 repository record; December 2010 graduation). Verification and Enforcement of State-Based Notions of Opacity in Discrete Event Systems. Ph.D. dissertation, University of Illinois at Urbana-Champaign. The review and manuscript use 2011; the institutional record gives an issue/ingest date of January 14, 2011, a graduation semester of December 2010, and copyright 2010. Hadjicostis is listed as the advisor, not as a coauthor of this dissertation.

7. Badouel, E., Bednarczyk, M., Borzyszkowski, A., Caillaud, B., and Darondeau, P. (2007). Concurrent Secrets. Discrete Event Dynamic Systems, 17(4), 425-446. This citation refers to the journal article rather than the earlier report or conference version.

8. Dubreil, J., Darondeau, P., and Marchand, H. (2008). Opacity enforcing control synthesis. Proceedings of the 9th International Workshop on Discrete Event Systems (WODES), 28-35. Author’s publication list. The conference paper is distinct from the same-title research report.

9. Lin, F. (2011). Opacity of discrete event systems and its applications. Automatica, 47(3), 496-503.

10. Ben-Kalefa, M., and Lin, F. (2009). Opaque superlanguages and sublanguages in discrete event systems. Proceedings of the 48th IEEE Conference on Decision and Control held jointly with the 28th Chinese Control Conference, 199-204.

11. Wu, Y.-C., and Lafortune, S. (2013). Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discrete Event Dynamic Systems, 23(3), 307-339. Author’s project bibliography. The journal issue is dated 2013; the publisher also records online publication in 2012.

12. Cassandras, C. G., and Lafortune, S. (2008). Introduction to Discrete Event Systems. 2nd edition. Springer. The edition has copyright year 2008; the publisher records the eBook publication date as November 27, 2007.

13. Cassez, F., Dubreil, J., and Marchand, H. (2012). Synthesis of opaque systems with static and dynamic masks. Formal Methods in System Design, 40(1), 88-115. Institutional publication record.