Verification and transformation for a trajectory-based weak K-step opacity

Opacity, as an important property in information-flow security, characterizes the ability of a system to keep some secret information from an outside intruder. In this paper, a version of K -step opacity, named trajectory-based weak K -step opacity, is proposed for meeting different level of privacy and security requirement. Compared to the standard weakly K -step opacity in the discrete-event systems modeled as finite-state automata, our proposed trajectory-based weak K -step opacity not only requires that the secret is kept within the last K -steps, but also requires that intruder cannot make sure whether or not a secret state has been passed before the last K -steps. For verification purpose, we propose a traced automaton and a parallel-computation-based method to verify the system. Furthermore, a transformation method from trajectory-based weak K -step opacity to current-state opacity is proposed.