We present SEAL, a language for specification and analysis of safety properties for label-based access control systems. A SEAL program represents a possibly infinite-state non-deterministic transition system describing the dynamic behavior of entities and their relevant access control operations. The features of our language are derived directly from the need to model new access control features arising from state-of-the art models in Windows 7, Asbestos, HiStar and others. We show that the reachability problem for this class of models is undecidable even for simple SEAL programs, but a bounded model-checking algorithm is able to validate interesting properties and discover relevant attacks.