Probabilistic verification of attack detection using logical observer

This paper focuses on the detection of cyber-attacks in a timed probabilistic setting. The plant and the possible attacks are described in terms of a labeled continuous time Markov model that includes both observable and unobservable events, and where each attack corresponds to a particular subset of states. Consequently, attack detection is reformulated as a state estimation problem. A verification methodology is described using a parallel-like composition of the Markov model and its logical observer. The construction of this parallel composition allows us to (i) concisely characterize the set of attacks that can be detected based on the sequences of observations they generate, and (ii) compute performance indicators of interest, such as the a priori probability of an undetectable attack, the average detectability, and the mean delay to detection.