Graph-based formal modeling and implementation of access control policies with automated conflict and redundancy detection | Synapse