@InProceedings{	  oldenburg-and-paul-e-sevinc-eth-zurich:specifying:2007,
  abstract	= {Security automata are a variant of B\"uchi 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.},
  address	= {1515 Broadway, New York, New York 10036},
  author	= {David Basin ETH Z\"urich AND Ernst-R\"udiger Olderog
		  University of Oldenburg AND Paul E. Sevinc ETH Z\"urich},
  booktitle	= {Information, computer and Communication security,
		  ASIACCS'07},
  copyright	= {Copyright 2007 by the Association for Computing
		  Machinery},
  copyrighturl	= {permissons@acm.org},
  editor	= {Robert Deng and Pierangela Samarati},
  isbn		= {1-59593-574-6},
  language	= {USenglish},
  month		= {March},
  pages		= {70--81},
  publisher	= {The Association for Computing Machinery},
  title		= {Specifying and analysing Security Automata using CSP-OZ},
  url		= {http://asiaccs07.i2r.a-star.edu.sg/},
  year		= 2007,
  user		= {tonknaff}
}