Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation
<|reference_start|>Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation: 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.<|reference_end|>
@article{capozucca2024brewer-nash,
    title={Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write
  Revocation},
    author={Alfredo Capozucca and Maximiliano Cristi'a and Ross Horne and Ricardo
  Katz},
    journal={arXiv preprint arXiv:2405.12187},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.12187},
    primaryClass={cs.CR}
}