Specifying and Analyzing Security Automata

David Basin - Department of Computer Science, ETH Zurich
Date and time
Monday, September 17, 2007 at 4:00 PM
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
External reference
Publication date
September 12, 2007


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.

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234