Brewer-Nash scrutinised : mechanised checking of policies featuring write revocation

Capozucca, Alfredo and Cristiá, Maximiliano and Horne, Ross and Katz, Ricardo (2024) Brewer-Nash scrutinised : mechanised checking of policies featuring write revocation. Other. arXiv. (https://doi.org/10.48550/arXiv.2405.12187)

[thumbnail of 2405.12187v1]
Preview
 Text. Filename: 2405.12187v1.pdf
Final Published Version
Download (287kB)| Preview

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.

ORCID iDs

Capozucca, Alfredo, Cristiá, Maximiliano, Horne, Ross ORCID logoORCID: https://orcid.org/0000-0003-0162-1901 and Katz, Ricardo;
  • Item type:Monograph(Other)
    ID code:89642
    Dates:
    Date
    Event
    20 May 2024
    Published
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:UNSPECIFIED
    Depositing user: Pure Administrator
    Date deposited:18 Jun 2024 13:59
    Last modified:14 Oct 2024 00:10
    URI:https://strathprints.strath.ac.uk/id/eprint/89642
CORE (COnnecting REpositories)