Specification and Refinement of Access Control

Abstract: we consider the extension of fair event system specifications by concepts of access control (prohibitions, user rights, and obligations). we give proof rules for veri- fying that an access control policy is correctly implemented in a system, and consider preservation of access control by refinement of event systems. prohibitions and obliga- tions are expressed as properties of traces and are preserved by standard refinement notions of event systems. preservation of user rights is not guaranteed by construction; we propose to combine implementation-level user rights and obligations to implement high-level user rights.