A new approach for the verification of infinite-step and K-step opacity using two-way observers

In the context of security analysis for information flow properties, where a potentially malicious observer (intruder) tracks the observed behavior of a given system, infinite-step opacity (respectively, K-step opacity) holds if the intruder can never determine for sure that the system was in a secret state for any instant within infinite steps (respectively, K steps) prior to that particular instant. We present new algorithms for the verification of the properties of infinite-step opacity and K-step opacity for partially-observed discrete event systems modeled as finite-state automata. Our new algorithms are based on a novel separation principle for state estimates that characterizes the information dependence in opacity verification problems, and they have lower computational complexity than previously-proposed ones in the literature. Specifically, we propose a new information structure, called the two-way observer, that is used for the verification of infinite-step and K-step opacity. Based on the two-way observer, a new upper bound for the delay in K-step opacity is derived, which also improves previously-known results.