A Unified Method to Efficiently Verify Opacity of Discrete-Timed Automata
摘要
Opacity is a powerful confidentiality property which guarantees that secret information of a system cannot be inferred from its observable behavior. To account for timing attacks, opacity has been extended to continuous-time systems, but the verification problem was proven to be generally undecidable. As a result, multiple recent works study the opacity verification problem of discrete-timed automata. The advantage of a discrete time setting is that it can discretize any timed automaton as a discrete-state system, where opacity can be verified. However, such verification methods usually rely on separating time steps into distinct hybrid states. This results in state explosion and limited scalability for real-world problems. In this paper, we present a new, more efficient verification method for opacity in a discrete time setting that avoids the state explosion problem. Our verification method groups multiple time steps to intervals, instead of evaluating each time step individually. We define four timed opacity notions and show that our method is capable of verifying all of them in a unified manner. We analyze the efficiency of our method on a case study of a wireless sensor network and randomized systems.