Automated Symbolic Analysis of ARBAC Policies