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

Protecting physical spaces in large organizations presents unique challenges that standard cybersecurity models simply cannot solve. Traditional physical security usually relies on rigid user roles that struggle to adapt to complex building layouts, real-time changes, and emergency situations. This paper introduces the Reliable Access Control (RAC) framework, a graph-based approach designed specifically for physical security. Instead of forcing a single, rigid method, RAC smoothly blends user roles, personal attributes, live context, and company structure into one flexible system. By mapping out buildings and access rules as a network graph, it separates your high-level security goals from the actual hardware locks. Finally, RAC uses mathematical verification to automatically guarantee that all security rules are safe and conflict-free before they are ever deployed.