Verification of K-step opacity and analysis of its complexity

In this paper, we analyze the verification of K-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. A system is K-step opaque if the entrance of the system state within the last K observations to a set of secret states remains opaque to an intruder who has complete knowledge of the system model and observes system activity through some projection map. We establish that the verification of K-step opacity is NP-hard. We also investigate the role of delay K in K-step opacity and show that there exists a delay K* such that K-step opacity and K´-step opacity become equivalent for K´ > K ¿ K*.