Abstract

Formal Methods including interactive theorem proving are increasingly applied in the area of IoT and other networked systems because they allow verification of security and privacy at design time as well as supporting rigorous processes of deploying these designs into certified system and network architectures.
In this talk we present past work on developing dedicated frameworks for the formal modelling and analysis of infrastructures with human actors for insider threats.
We will then show how these works can be suitably extended to support misbehaviour detection and mitigation strategies for OSNEM (Online Social Media and Networks) for this call by a twofold strategy:
(a) extending the shallow human actors' model in the existing frameworks by injecting more aspects of cognition to enable misbehaviour detection
(b) building on foundations for attack trees to provide additional foundations and verification techniques for attack-defence trees which allows automatically generating mitigation strategies.