Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving