  A new logic for verification of security policies is proposed. The logic,
HyperLTL, extends linear-time temporal logic (LTL) with connectives for
explicit and simultaneous quantification over multiple execution paths, thereby
enabling HyperLTL to express information-flow security policies that LTL
cannot. A model-checking algorithm for a fragment of HyperLTL is given, and the
algorithm is implemented in a prototype model checker. The class of security
policies expressible in HyperLTL is characterized by an arithmetic hierarchy of
hyperproperties.
