A Unified Graph-Based Framework for Formally Verified Physical Access Control in Large Enterprises

Securing physical assets in large-scale organizations presents unique challenges distinct from logical IT environments. Traditional Physical Access Control (PAC) methods, predominantly reliant on static Role-Based Access Control (RBAC), lack sufficient granularity, contextual flexibility, and maintainability. Existing logical access models encounter considerable challenges when ported to the physical domain, including modeling complex spatial realities, managing real-time context, and enforcing safety-critical emergency overrides. This paper introduces the Reliable Access Control (RAC) framework, a novel, graph-based methodology for designing and optimizing PAC systems. RAC intelligently synthesizes the strengths of RBAC, Attribute-Based Access Control (ABAC), Context-Based Access Control (CBAC), and Organization-Based Access Control (OrBAC) into a cohesive mathematical model. By representing physical topologies and access policies as a directed graph, RAC establishes a single source of truth decoupling high-level intent from low-level hardware permissions. Furthermore, an integrated Formal Verification Service utilizing Satisfiability Modulo Theories (SMT) solvers (Z3) mathematically guarantees policy configurations adhere to strict safety invariants prior to deployment.