Abstract: Specifying and analysing Security Automata using CSP-OZ David Basin ETH Zürich AND Ernst-Rüdiger Olderog University of Oldenburg AND Paul E. Sevinc ETH Zürich Security automata are a variant of Büchi automata ued to sepcify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communication Sequential Processes (CSP) and Object-Z (OZ) , to specify security automata, formalize their combination with with target systems, and analyse the security of the resulting system specifications. We provide theoretical rsults relating CSP-OZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for proactical usefulness of this approach. This includs the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as wll as automated, tool-supported analysis.