A comprehensive approach to the automatic refinement and verification of access control policies