@Article{	  brucker.ea:verification:2005,
  abstract	= {We present a method for the security analysis of realistic
		  models over off-the-shelf systems and their configuration
		  by formal, machine-checked proofs. The presentation follows
		  a large case study based on a formal security analysis of a
		  CVS-Server architecture.\\\\The analysis is based on an
		  abstract architecture (enforcing a role-based access
		  control), which is refined to an implementation
		  architecture (based on the usual discretionary access
		  control provided by the \posix{} environment). Both
		  architectures serve as a skeleton to formulate access
		  control and confidentiality properties.\\\\Both the
		  abstract and the implementation architecture are specified
		  in the language Z. Based on a logical embedding of Z into
		  Isabelle/HOL, we provide formal, machine-checked proofs for
		  consistency properties of the specification, for the
		  correctness of the refinement, and for security properties.},
  author	= {Achim D. Brucker and Burkhart Wolff},
  copyright	= {\copyright Springer-Verlag},
  copyrighturl	= {http://www.springeronline.com/sgw/cda/frontpage/0,11855,1-40109-70-1119401-0,00.html}
		  ,
  issn		= {1433-2779},
  journal	= {International Journal on Software Tools for Technology
		  Transfer (STTT)},
  language	= {USenglish},
  number	= 3,
  doi		= {10.1007/s10009-004-0176-3},
  pages		= {233--247},
  pdf		= {papers/2005/sttt_03.pdf},
  title		= {A Verification Approach for Applied System Security},
  volume	= 7,
  year		= 2005,
  user		= {wolff}
}