- Conference Paper
Security automata are a variant of Büchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results 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 the practical usefulness of this approach. 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. Show more
Book titleProceedings of the 2nd ACM Symposium on Information, Computer and Communications Security (ASIACCS '07)
Pages / Article No.
PublisherAssociation for Computing Machinery
SubjectCSP-OZ; Security automata
Organisational unit03634 - Basin, David / Basin, David
MoreShow all metadata