Biblio

Cyber-Physical systems (CPSs) are exposed to cyber- physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes of the systems.We define two probabilistic metrics to estimate the physical impact of attacks targeting cyber-physical systems formalised in terms of a probabilistic hybrid extension of Hennessy and Regan's Timed Process Language. Our impact metrics estimate the impact of cyber-physical attacks taking into account: (i) the severity of the inflicted damage in a given amount of time, and (ii) the probability that these attacks are actually accomplished, according to the dynamics of the system under attack. In doing so, we pay special attention to stealthy attacks, i. e., attacks that cannot be detected by intrusion detection systems. As further contribution, we show that, under precise conditions, our metrics allow us to estimate the impact of attacks targeting a complex CPS in a compositional way, i.e., in terms of the impact on its sub-systems.

Gorrieri and Martinelli’s timed Generalized Non-Deducibility on Compositions () schema is a well-known general framework for the formal verification of security protocols in a concurrent scenario. We generalise the  schema to verify wireless network security protocols. Our generalisation relies on a simple timed broadcasting process calculus whose operational semantics is given in terms of a labelled transition system which is used to derive a standard simulation theory. We apply our  framework to perform a security analysis of three well-known key management protocols for wireless sensor networks: , LEAP+ and LiSP.