Date Added: Oct 2009
Usage control is a comprehensive access control model developed to cater the security needs of the wide range of applications. Formal specification of the core usage control models and their expressivity, decidability of safety properties are explored recently. They help one to understand the usability and safety of the model. However, security of the usage control in the practical applications depends on the safety of the model as well as its correct implementation in the application. This paper presents an approach to verify the correctness of the usage control implementation using a semi-formal property verification tool. The authors also provide an illustrative case study.