| Dr Florian Kammueller |
| Mon 20 May 2019, 14:00 - 15:00 |
| IF 4.31/4.33 |
If you have a question about this talk, please contact: Allison Kruk (v1atayl6)
Refreshments provided
Title
Security Engineering in Isabelle
Abstract
In this talk, we show a security engineering process based on model transformations fully formalized in the proof assistant Isabelle. This Refinement-Risk Loop focuses on attack analysis and security refinement supported by interactive theorem proving. Since we use a fully formal model of infrastructures with actors and policies we can support a novel way of formal security refinement for system specifications. This formal process is built practically as an extension to the Isabelle Infrastructure framework with attack trees. We define a formal notion of model transformations on infrastructure models. Thanks to the formal foundation of Kripke structures and branching time temporal logic in the Isabelle Infrastructure framework, these stepwise transformations can be interleaved with attack tree analysis thus providing a full security engineering framework. The process is illustrated on an IoT healthcare case study introducing GDPR requirements and blockchain.