Strong current-state and initial-state opacity of discrete-event systems

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((vertical bar Sigma vertical bar vertical bar X vertical bar(2) + vertical bar Sigma(o)vertical bar vertical bar X\X-S vertical bar(2)(1+vertical bar Sigma(uo)vertical bar))2(vertical bar X\XS vertical bar)), where vertical bar X vertical bar (resp., vertical bar Sigma vertical bar, vertical bar Sigma(o)vertical bar, vertical bar Sigma(uo)vertical bar, vertical bar X\X-S vertical bar) 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. (c) 2022 Elsevier Ltd. All rights reserved.