  The paper studies dynamic information flow security policies in an
automaton-based model. Two semantic interpretations of such policies are
developed, both of which generalize the notion of TA-security [van der Meyden
ESORICS 2007] for static intransitive noninterference policies. One of the
interpretations focuses on information flows permitted by policy edges, the
other focuses on prohibitions implied by absence of policy edges. In general,
the two interpretations differ, but necessary and sufficient conditions are
identified for the two interpretations to be equivalent. Sound and complete
proof techniques are developed for both interpretations. Two applications of
the theory are presented. The first is a general result showing that access
control mechanisms are able to enforce a dynamic information flow policy. The
second is a simple capability system motivated by the Flume operating system.
