Combining secure system design with risk assessment for IoT healthcare systems

In this paper, we show how to derive formal spec- ifications of secure IoT systems by a process that uses the risk assessment strategy of attack trees on infrastructure models. The models of the infrastructure are logical models in the Isabelle Infrastructure framework. It comprises actors, policies and a state transition of the dynamic evolution of the system. This logical framework also provides attack trees. The process we propose in this paper incrementally uses those two features to refine a system specification until expected security and privacy properties can be proved. Infrastructures allow modeling logical as well as physical elements which makes them well suited for IoT applications. We illustrate the stepwise application of the proposed process in the Isabelle Insider framework on the case study of an IoT healthcare system.

© 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.”