Layered graph logic as an assertion language for access control policy models

Matthew Collinson, Kevin McDonald, David Pym

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives, for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture, and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system. We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.
Original languageEnglish
Pages (from-to)41-80
Number of pages40
JournalJournal of Logic and Computation
Volume27
Issue number1
Early online date12 Jun 2015
DOIs
Publication statusPublished - Feb 2017

Fingerprint

Control Policy
System Architecture
Access Control
Assertion
Access control
Logic
Local Properties
Graph in graph theory
Vulnerability
Reasoning
Model
Language
Graph
Architecture
Framework

Keywords

  • substructural logic
  • layered graphs
  • access control
  • modelling

Cite this

Layered graph logic as an assertion language for access control policy models. / Collinson, Matthew; McDonald, Kevin; Pym, David.

In: Journal of Logic and Computation, Vol. 27, No. 1, 02.2017, p. 41-80.

Research output: Contribution to journalArticle

@article{3a90378ef3a547daa8266579523593c5,
title = "Layered graph logic as an assertion language for access control policy models",
abstract = "We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives, for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture, and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system. We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.",
keywords = "substructural logic , layered graphs, access control, modelling",
author = "Matthew Collinson and Kevin McDonald and David Pym",
year = "2017",
month = "2",
doi = "10.1093/logcom/exv020",
language = "English",
volume = "27",
pages = "41--80",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "1",

}

TY - JOUR

T1 - Layered graph logic as an assertion language for access control policy models

AU - Collinson, Matthew

AU - McDonald, Kevin

AU - Pym, David

PY - 2017/2

Y1 - 2017/2

N2 - We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives, for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture, and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system. We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.

AB - We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives, for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture, and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system. We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.

KW - substructural logic

KW - layered graphs

KW - access control

KW - modelling

U2 - 10.1093/logcom/exv020

DO - 10.1093/logcom/exv020

M3 - Article

VL - 27

SP - 41

EP - 80

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 1

ER -