Brewer-Nash 模型审视：包含写权限撤销的策略机械化检查
密码学与安全
2024-05-29 v2
摘要
本文重新审视了受中国墙伦理策略启发的 Brewer-Nash 安全策略模型。我们提请注意，在 Brewer-Nash 模型中写权限是可以被撤销的。写权限的语义最初未被充分规范，导致了多种解释，为此我们提供了现代操作语义。接着，我们采用改编自 Kessler 的更精确定义，对 Brewer-Nash 模型中的信息流分析进行了现代化改进。针对我们现代化重构的模型，我们为 Brewer & Nash 提出的所有定理提供了完整的机械化覆盖。大多数定理使用工具 {log} 自动证明，唯一例外是关于信息流的定理，它将 {log} 中的引理与 Coq 中机械化的定理相结合。在涵盖 Brewer-Nash 最初提出的所有定理并实现现代精度与机械化之后，我们提出这项工作是迈向更复杂安全策略模型自动化检查方法论的一步。
引用
@article{arxiv.2405.12187,
title = {Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation},
author = {Alfredo Capozucca and Maximiliano Cristiá and Ross Horne and Ricardo Katz},
journal= {arXiv preprint arXiv:2405.12187},
year = {2024}
}