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

Alfredo Capozucca, Maximiliano Cristia, Ross Horne, Ricardo Katz

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

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.
Original languageEnglish
Title of host publication2024 IEEE 37th Computer Security Foundations Symposium (CSF)
Place of PublicationLos Alamitos, CA, USA
Pages112-126
Number of pages15
ISBN (Electronic)979-8-3503-6203-9
DOIs
Publication statusPublished - 20 Sept 2024
Event37th IEEE Computer Security Foundations Symposium, CSF 2024 - Enschede, Netherlands
Duration: 8 Jul 202412 Jul 2024

Publication series

Name2024 IEEE 37th Computer Security Foundations Symposium (CSF)
Publisher IEEE Computer Society Press
ISSN (Print)2374-8303

Conference

Conference37th IEEE Computer Security Foundations Symposium, CSF 2024
Country/TerritoryNetherlands
CityEnschede
Period8/07/2412/07/24

Keywords

  • security policies
  • information flow
  • confidentiality
  • revocation
  • set theory
  • automated verification

Fingerprint

Dive into the research topics of 'Brewer-Nash scrutinised: mechanised checking of policies featuring write revocation'. Together they form a unique fingerprint.

Cite this