Formal analyses of usage control policies

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 control mechanism 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 model checker as theorem prover and is based on a translation of usage control policies into a Linear Time Logic (LTL) dialect. We provide evidence that even complex policies can be analyzed efficiently.