Isabelle 中安全工程的正式开发周期
密码学与安全
2020-01-27 v1 软件工程
摘要
在本文中，我们展示了一种基于精化(formal notion of refinement)的正式概念的安全工程过程，该概念在证明辅助工具 Isabelle 中完全形式化。此精化-风险周期(Refinement-Risk Cycle)侧重于由交互式定理证明支持的攻击分析与安全精化。由于我们使用具有参与者和策略的完全形式化基础设施模型，我们能够为系统规范支持一种新颖的正式安全精化方式。该正式过程实际构建为带有攻击树的 Isabelle Infrastructure 框架的扩展。我们在基础设施模型上定义了正式的精化概念。得益于 Isabelle Infrastructure 框架中 Kripke 结构与分支时间时序逻辑的形式化基础，这些逐步变换可与攻击树分析交错进行，从而提供一个完全正式的安全工程框架。该过程在一个引入 GDPR 要求与区块链的物联网医疗案例研究中得到说明。
引用
@article{arxiv.2001.08983,
title = {A Formal Development Cycle for Security Engineering in Isabelle},
author = {Florian Kammüller},
journal= {arXiv preprint arXiv:2001.08983},
year = {2020}
}