Policy engineering for access-control security has traditionally focused on specification and verification of safety properties (``nothing bad happens''). In most real systems however, resources and access mechanisms are ...