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)


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
Issue number1
Early online date12 Jun 2015
Publication statusPublished - Feb 2017



  • substructural logic
  • layered graphs
  • access control
  • modelling

Cite this