Timed opacity verification for switching output automata

In this paper, we consider timed opacity verification for switching output automata (SOA). We define a subset of global states of the SOA as vulnerable and associate to each of them a secret dwell interval. A SOA is opaque if an intruder, based on the observation of the outputs over time, cannot determine whether the current global state is vulnerable and the corresponding dwell time belongs to the secret dwell interval. We define a secret-dependent evolution automaton as the logical abstraction of the SOA's evolution when incorporating timed secrets. We show how an observer, i.e., the deterministic finite automaton equivalent to the secret-dependent evolution automaton, can be used to verify timed opacity.