Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation

TL;DR

The paper revisits the Brewer-Nash model, clarifying the ambiguous write-semantics and revocation, and provides a precise operational semantics inspired by $Kessler$ with sanitized-data support. It achieves automatic verification by mechanising the theorems with the {log} tool and Coq in a hybrid approach for an information-flow property, and fully mechanises all original Brewer-Nash results. This work tightens definitions, demonstrates a robust methodology for computer-assisted verification of security policies, and lays groundwork for extending automated checking to more complex, confidentiality-focused models. The contributions improve precision and confidence in Brewer-Nash-style policies and highlight practical pathways for certifying policy correctness in real systems.

Abstract

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.

Figures (1)

• Figure 1: A transition where write is revoked: subject $s_1$ requests access to $o_3$ (permitted by simple security), which results in write access to $o_2$ being revoked (due to the *-property).

Theorems & Definitions (1)

• Definition 1: simple security