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.