2020/01/04 by Florian Kammüller, Kammüller, Florian · 1 citation
Computer Science · Social Sciences · #Access Control and Trust #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Information and Cyber Security #Security and Verification in Computing #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2001.08983
openalex publication_date 2020/01/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper, we show a security engineering process based on a formal notion of refinement fully formalized in the proof assistant Isabelle. This Refinement-Risk Cycle focuses on attack analysis and security refinement supported by interactive theorem proving. Since we use a fully formalized 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 refinement 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 fully formal security engineering framework. The process is illustrated on an IoT healthcare case study introducing GDPR requirements and blockchain.