Specifying and Analyzing Security Automata

Security automata are a variant of Buechi automata used to
specify security policies that can be enforced by monitoring system
execution.  We propose using CSP-OZ for specifying security automata,
formalizing their combination with target systems, and analyzing the
security of the resulting system specifications.  CSP-OZ is a rich
specification language that combines Communicating Sequential Processes
(CSP) and Object-Z (OZ).  Our thesis is that this language is very well
suited for specifying and reasoning about complex security automata and
their combination with large-scale systems. This includes the ability to
specify concisely complex operations and complex control, support for
structured specifications, refinement, and transformational design, as
well as automated, tool supported analysis.  We present two case
studies, which provide support for this thesis.