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.