The Role and Mathematical Foundations of Use Management and Formal Verification Models in Ensuring Information Security

This article profoundly investigates access control systems, which constitute the fundamental cornerstone of information security, and explores their conceptual correlation with the CIA triad and Saltzer-Schroeder principles. To design error-free security policies in contemporary complex, distributed, and reactive cyber-systems, access matrices along with their storage methods—ACL and Capability Lists—are analyzed. The primary scientific novelty of the paper lies in the mathematical analysis of formal modeling and automated verification (Model Checking) mechanisms using Kripke structures and temporal logic operators (LTL, CTL) aimed at eliminating logical errors during the initial stages of system security design.