论文标题
Isabelle安全工程的正式开发周期
A Formal Development Cycle for Security Engineering in Isabelle
论文作者
论文摘要
在本文中，我们根据证明助手伊莎贝尔（Isabelle）中完全正式形式化的正式改进概念展示了安全工程过程。这种改进风险周期的重点是攻击分析和安全性改进，并由交互式定理证明。由于我们使用与参与者和政策的完全形式化的基础设施模型，因此我们可以支持一种新颖的系统规范安全性改进方式。这种正式过程实际上是作为使用攻击树的Isabelle基础设施框架的扩展。我们在基础设施模型上定义了正式的完善概念。得益于Kripke结构的正式基础和Isabelle基础架构框架中的分支时间逻辑，这些逐步转换可以与攻击树分析交织在一起，从而提供了完全正式的安全工程框架。该过程在IOT医疗案例研究中进行了说明，该案例介绍了GDPR要求和区块链。
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.
