Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910460864888832 |
|---|---|
| author | Capozucca, Alfredo Cristiá, Maximiliano Horne, Ross Katz, Ricardo |
| author_facet | Capozucca, Alfredo Cristiá, Maximiliano Horne, Ross Katz, Ricardo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_12187 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation Capozucca, Alfredo Cristiá, Maximiliano Horne, Ross Katz, Ricardo Cryptography and Security 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. |
| title | Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation |
| topic | Cryptography and Security |
| url | https://arxiv.org/abs/2405.12187 |