Sensitive data are increasingly available on-line through the Web and other distributed protocols. System designers often create policies to capture conditions on the access to data. To reduce source clutter and improve maintenance, developers increasingly use domain-specific, declarative languages to express these policies. In turn, administrators need to analyze policies relative to properties, and to understand the effect of policy changes even in the absence of properties. This talk discusses models and techniques that support both kinds of analyses for role-based access-control policies. It discusses Margrave, a software tool that implements these analyses for standalone policies, and discusses work in progress on models that also account for the dynamic environment in which policies execute. This extension enables reasoning about interactions between policies and the programs that employ them, but using analyses that extend beyond conventional model checking.