Current-state anonymity and opacity subject to state attacks in discrete event systems

This paper introduces and analyzes novel notions of current-state anonymity and opacity, subject to state attacks, within the context of discrete event systems modeled with nondeterministic finite automata. When a state attack is performed, the intruder learns whether or not the current state of the system falls into a specific subset of states. Thus, state attacks provide additional state information to the intruder during the operation of the system. The system is considered to be current-state anonymous (resp. opaque) under a state attack if the intruder can never be certain that the current state of the system is unique (resp. the current state of the system belongs to a subset of secret states), based on its observations and the additional knowledge provided by any state attacks. A necessary and sufficient condition is presented to check the underlying current-state anonymity (resp. opacity) of a given system subject to a large class of state attacks. We also provide pertinent complexity analysis of the corresponding verification method and illustrative examples that elucidate the proposed concepts of state-attack anonymity (resp. opacity) subject to the specified class of state attacks.