Introducing Distributed Ledger Security into System Specifications with the Isabelle RR-Cycle

We present an approach to developing secure system specifications for IoT systems with decentralized data using the Refinement-Risk cycle (RR-cycle), a method for security engineering implemented in the proof assistant Isabelle. The RR-cycle enables interleaving attack analysis with system refinement using rigorous machine assisted proof in Isabelle to scrutinize and refine system specifications until security requirements are met. We illustrate this approach by a case study of a privacy critical scenario by refining it with a distributed ledger. The case study is motivated by the IoT project SUCCESS on security and privacy of healthcare IoT applications. We briefly summarize the RR-cycle method before focusing on its application of identifying a privacy attack that leads to a security refinement introducing the distributed ledger.