You Don't Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems

TL;DR

This paper introduces the concept of high-order opacity in discrete-event systems, focusing on the knowledge of system users and how intruders cannot determine what the user knows, with algorithms for verification.

Contribution

It defines high-order opacity, a novel security property related to user knowledge, and provides algorithms for its verification with complexity analysis.

Findings

High-order opacity formalized and defined.

Two algorithms for verification with different complexities.

Illustrative examples demonstrating the new notion.

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.