Provides a detailed refinement of the definitions and concepts in the access control architecture and framework defined by the NGAC-FA standard. To provide a precise specification of the abstractions involved, the refinements are based on the mathematics of set theory and predicate calculus in consonance with the Z notation. By capturing the essential properties of NGAC mathematically, free from constraints on how these properties are achieved, NGAC-GOADS serves as a formal, conceptual model for the composition and working of NGAC.