This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in the Brewer-Nash model, by adopting a more precise definition adapted from Kessler. For our modernised reformulation, we provide full mechanised coverage for all theorems proposed by Brewer & Nash. Most theorems are established automatically using the tool {log} with the exception of a theorem regarding information flow, which combines a lemma in {log} with a theorem mechanised in Coq. Having covered all theorems originally posed by Brewer-Nash, achieving modern precision and mechanisation, we propose this work as a step towards a methodology for automated checking of more complex security policy models.

翻译：本文重新审视了受伦理中国墙策略启发的Brewer-Nash安全策略模型。我们指出，在Brewer-Nash模型中写访问权限可被撤销。原始规范对写访问语义的定义存在不足，导致多种解释，为此我们提供了一种现代操作语义。通过采用Kessler提出的更精确定义，我们进一步现代化了Brewer-Nash模型中信息流的分析方法。针对现代化后的重构公式，我们为Brewer & Nash提出的所有定理提供了完整的机械化覆盖。除了一则关于信息流的定理需结合{log}中的引理与Coq中机械化的定理外，其余定理均通过{log}工具自动建立。在完成Brewer-Nash原始所有定理的覆盖并实现现代精度与机械化后，我们将此工作视为迈向自动化检测更复杂安全策略模型方法论的一步。