Abstract
Usage control is a generalization of access control that also addresses how data is handled after it is released. Usage control requirements are specified in policies. We present tool support for the following analysis problems. Is a policy consistent, i.e., satisfiable? Is an abstractly specified usage controlmechanism capable of enforcing a given policy? Can we configure such a mechanism by analyzing respective policies? In the context of propagation, where upon re-distribution of data duties may only be increased and rights decreased, can we check if a policy is only strengthened in this sense? — Our solution uses a modelchecker as theorem prover and is based on a translation ofusage control policies into a Linear Time Logic (LTL) dialect. We provide evidence that even complex policies can be analyzed efficiently.