  We introduce a framework for reasoning about the security of computer systems
using modal logic. This framework is sufficiently expressive to capture a
variety of known security properties, while also being intuitive and
independent of syntactic details and enforcement mechanisms. We show how to use
our formalism to represent various progress- and termination-(in)sensitive
variants of confidentiality, integrity, robust declassification and transparent
endorsement, and prove equivalence to standard definitions. The intuitive
nature and closeness to semantic reality of our approach allows us to make
explicit several hidden assumptions of these definitions, and identify
potential issues and subtleties with them, while also holding the promise of
formulating cleaner versions and future extension to entirely novel properties.
