A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules