Analysis of access control protocols using labelled tableaux

Access control Systems are used to authenticate and authorize users. For specifying and reasoning about the security properties of access control Systems, many researchers have proposed the use of belief logics. Since authentication protocols are designed to operate in dynamic environments, it is important to model the evolution of access control systems through time. This paper proposes a state logic called SL. With the logic SL and its associated modal tableaux, we are able to reason about and verify security properties of access control systems operating in dynamic environments.