  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.
