Bounded opacity for timed systems

In many security applications, system behaviors must be kept secret (opaque) to outside observers (intruders). Opacity was first studied for discrete event systems, and then it was extended to real-time systems. One of the challenges of real-time systems is the difficulty to guarantee their opacity against a potential attacker. In general, this property is undecidable for systems modeled by timed automata. A secret location, S, of a system is timed opaque to an intruder having partial observability of the system, if the intruder can never infer from the observation of any execution that the system has reached any secret location. In the present study, the static partial observability for systems modeled by nondeterministic timed automata is investigated. Thus, it focuses on systems where the timing of secret state reachability is bounded. The first contribution of this study is to define the bounded timed opacity property wherein, its complexity is proved. The second contribution is to consider systems where the secret should be kept hidden for a certain period referred to as the Delta-duration bounded opacity property. Also, a formal definition is proposed and its complexity is proved. In addition, the proposed properties are verified using timed bounded model checking. A case study "Exchange in the Cloud system" is modeled by timed automaton to verify the proposed properties using SpaceEx tool.