Modal Location-Resource-Process Logic for Access Control

The logic MBI is a substructural modal logic of locations, resources, and processes that is closely related to both the bunched logic BI and Hennessy-Milner logic. MBI stands in a (slightly weak) Hennessy-Milner correspondence with the synchronous process calculus of located resources, LSCRP. Starting from motivations in large-scale systems modelling, I will introduce MBI and LSCRP, and explain how they can be used to address some theoretical and practical questions in access control.