30 April 2018: Florian Kammueller Attack Trees in Isabelle In this talk, I present a proof theory for attack trees. Attack trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, I define a generic theory of attack trees using a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of attack trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of attack tree validity and CTL. The application is illustrated on the GDPR (General Data Privacy Regulation) compliance verification with the example of a healthcare IoT systems. Bio Florian Kammueller is an Associate Professor in the Department of Computer Science at Middlesex University London and Privatdozent (honorary professor) at Technische Universitaet Berlin. He holds a PhD from the University of Cambridge on "Modular Reasoning in Isabelle" and a Habilitation from Technische Universitaet Berlin on "Interactive Theorem Proving in Software Engineering". His research is centered around applying interactive theorem proving and other formal methods to applications from software and security engineering. He has led and contributed to several research projects in Germany and the UK and is currently leading the European CHIST-ERA project SUCCESS on security and privacy for the IoT where formal security engineering is applied to support cost-efficient transparent health care monitoring systems. Apr 30 2018 14.00 - 15.00 30 April 2018: Florian Kammueller Attack Trees in Isabelle IF 4.31/4.33
30 April 2018: Florian Kammueller Attack Trees in Isabelle In this talk, I present a proof theory for attack trees. Attack trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, I define a generic theory of attack trees using a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of attack trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of attack tree validity and CTL. The application is illustrated on the GDPR (General Data Privacy Regulation) compliance verification with the example of a healthcare IoT systems. Bio Florian Kammueller is an Associate Professor in the Department of Computer Science at Middlesex University London and Privatdozent (honorary professor) at Technische Universitaet Berlin. He holds a PhD from the University of Cambridge on "Modular Reasoning in Isabelle" and a Habilitation from Technische Universitaet Berlin on "Interactive Theorem Proving in Software Engineering". His research is centered around applying interactive theorem proving and other formal methods to applications from software and security engineering. He has led and contributed to several research projects in Germany and the UK and is currently leading the European CHIST-ERA project SUCCESS on security and privacy for the IoT where formal security engineering is applied to support cost-efficient transparent health care monitoring systems. Apr 30 2018 14.00 - 15.00 30 April 2018: Florian Kammueller Attack Trees in Isabelle IF 4.31/4.33
