K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Local Opacity Verification for Distributed Discrete Event Systems
This paper studies current-state opacity and initial-state opacity verification of distributed discrete event systems. The distributed system's global model is the parallel composition of multiple local systems: each of …
Secure Your Intention: On Notions of Pre-Opacity in Discrete-Event Systems
This paper investigates an important informationflow security property called opacity in partially-observed discrete-event systems. We consider the presence of a passive intruder (eavesdropper) that knows the dynamic mod…
Comparing the Notions of Opacity for Discrete-Event Systems
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 …
You Don't Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems
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 b…
Abstraction-Based Verification of Approximate Pre-Opacity for Control Systems
In this paper, we consider the problem of verifying pre-opacity for discrete-time control systems. Pre-opacity is an important information-flow security property that secures the intention of a system to execute some sec…