Event Systems and Access Control

TL;DR

This paper explores how access control policies can be verified and preserved in event-based information systems, proposing methods to refine user rights and combine system obligations for effective enforcement.

Contribution

It introduces proof rules for verifying access control enforcement and presents a novel approach to refine user rights through combining low-level rights with system obligations.

Findings

Proof rules for verifying access control enforcement

Methods for preserving access control during system refinement

A new approach to refine user rights by combining rights and obligations

Abstract

We consider the interpretations of notions of access control (permissions, interdictions, obligations, and user rights) as run-time properties of information systems specified as event systems with fairness. We give proof rules for verifying that an access control policy is enforced in a system, and consider preservation of access control by refinement of event systems. In particular, refinement of user rights is non-trivial; we propose to combine low-level user rights and system obligations to implement high-level user rights.