NIST Internal Report (IR) 8539, Security Property Verification by Transition Model, is now available.
Verifying the security properties of access control policies is a complex and critical task. Often, the policies and their implementation do not explicitly express their underlying semantics, which may be implicitly embedded in the logic flows of policy rules, especially when policies are combined. Instead of evaluating and analyzing access control policies solely at the mechanism level, formal transition models can describe these policies and prove the system’s security properties, ensuring that access control mechanisms are designed to meet security requirements.
This document explains how to apply model-checking techniques to verify security properties in transition models of access control policies. It provides a brief introduction to the fundamentals of model checking and demonstrates how access control policies are converted into automata from their transition models. The document also discusses property specifications in terms of linear temporal logic (LTL) and computation tree logic (CTL) languages with comparisons between the two. Finally, the verification process and available tools are described and compared.
