rather wide gap in abstraction between policies and mechanisms. In this paper, we propose a general approach for property veriﬁcation for MAC models. The approach deﬁnes a standardized structure for MAC models, providing for both property veriﬁcation and automated generation of test cases. The approach expresses MAC models in the speciﬁcation language of a model checker and expresses generic access control properties in the property language. Then the approach uses the model checker to verify the integrity, coverage, and conﬁnement of these properties for the MAC models and ﬁnally generates test cases via combinatorial covering array for the system implementations of the models.