Security Property Verification by Transition Model

#1646310: Security Property Verification by Transition Model - November 25, 2024

Description:	Announcement 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 prove 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. NOTE: A call for patent claims is included on page ii of this draft. For additional information, see the Information Technology Laboratory (ITL) Patent Policy – Inclusion of Patents in ITL Publications. 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 prove 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. Keywords access control; access control policy; model test; policy test; policy verification
More info:	https://csrc.nist.gov/pubs/ir/8539/ipd

Description:

Announcement
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 prove 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.

NOTE: A call for patent claims is included on page ii of this draft. For additional information, see the Information Technology Laboratory (ITL) Patent Policy – Inclusion of Patents in ITL Publications.

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 prove 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.

Keywords
access control; access control policy; model test; policy test; policy verification

More info:

https://csrc.nist.gov/pubs/ir/8539/ipd

Date added	Oct. 9, 2024, 4:55 a.m.
Source	NIST
Subjects	NIST / DISA / DoD (Dept of Defence) / NSA USA Guidelines and Checklists PodCasts / Webcast / Webinar / eSummit / Virtual Event etc.
Venue	Nov. 25, 2024, midnight - Nov. 25, 2024, midnight