@Article{	  brucker.ea:verification:2005,
  author	= {Achim D. Brucker and Burkhart Wolff},
  title		= {A Verification Approach for Applied System Security},
  journal	= {International Journal on Software Tools for Technology
		  (STTT)},
  year		= {2005},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  pdf		= {http://www.brucker.ch/bibliography/download/2005/brucker.ea-verification-2005.pdf},
  language	= {USenglish},
  keywords	= {verification, security, access control, refinement, POSIX,
		  CVS, Z },
  classification= {journal},
  areas		= {security, formal methods, software},
  issn		= {1433-2779},
  doi		= {10.1007/s10009-004-0176-3},
  volume	= {7},
  number	= {3},
  pages		= {233--247},
  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.},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-verification-2005}
		  
}