@InProceedings{	  basin.ea:specifying:2007,
  abstract	= {Security automata are a variant of B\"uchi 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.},
  author	= {David Basin and Ernst-R\"udiger Olderog and Paul E.
		  Sevin{\c{c}}},
  booktitle	= {AsiaCCS 2007},
  copyright	= {ACM, 2007},
  copyrighturl	= {http://www.acm.org/pubs/copyright_policy/},
  language	= {USenglish},
  month		= {March},
  organization	= {ACM},
  pdf		= {papers/2007/asiaccs.pdf},
  publisher	= {ACM},
  title		= {Specifying and Analyzing Security Automata using CSP-OZ},
  url		= {http://www.zisc.ethz.ch/research/publications},
  year		= 2007,
  user		= {psevinc}
}