Assuring logical consistency among the specification of entities, relations and constraints in a role-based access control (RBAC) schema becomes increasingly important and urgent as the access control systems increase their spatial and temporal span. This paper reports an attempt to employ ALLOY, a lightweight modeling system with automatic semantic analysis capability, to verify internal consistency of RBAC schema as well as explicit manifestation of certain algebraic properties.