Security Property Verification by Transition Model

Published

January 31, 2025

Author(s)

Chung Tong Hu

Abstract

Verifying the security properties of access control policies is a complex and critical task. The policies and their implementation often 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 are used to describe these policies and verify the system's security properties. This approach ensures that access control mechanisms can be 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 then focuses on discussing 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.

Citation

NIST Interagency/Internal Report (NISTIR) - 8539

Report Number

8539

NIST Pub Series

NIST Interagency/Internal Report (NISTIR)

Pub Type

NIST Pubs

Download Paper

https://doi.org/10.6028/NIST.IR.8539

Local Download

Keywords

access control, access control policy, model test, policy test, policy verification.

Citation

Hu, C. (2025), Security Property Verification by Transition Model, NIST Interagency/Internal Report (NISTIR), National Institute of Standards and Technology, Gaithersburg, MD, [online], https://doi.org/10.6028/NIST.IR.8539, https://tsapps.nist.gov/publication/get_pdf.cfm?pub_id=959317 (Accessed February 16, 2025)