Automated and Efficient Analysis of Role-Based Access Control with Attributes