@InProceedings{	  brucker.wolff:case,
  author	= {Achim D. Brucker and Burkhart Wolff},
  title		= {A Case Study of a Formalized Security Architecture},
  booktitle	= {Eighth International Workshop onFormal Methods for
		  Industrial Critical Systems (FMICS'03)},
  volume	= 80,
  classification= {proceedings},
  editor	= {Thomas Arts and Wan Fokkink},
  publisher	= {Elsevier Science Publishers},
  year		= 2003,
  language	= {USenglish},
  abstract	= {CVS is a widely known version management system, which can
		  be used for the distributed development of software as well
		  as its distribution from a central database.
		  
		  In this paper, we provide an outline of a formal security
		  analysis of a CVS-Server architecture performed
		  in~\cite{brucker.ea:cvs-server:2002}. The analysis is based
		  on an abstract architecture (enforcing a role-based access
		  control on the repository), which is refined to an
		  implementation architecture (based on the usual
		  discretionary access control provided by the \posix{}
		  environment). Both architectures serve as framework to
		  formulate access control and confidentiality properties.
		  
		  Both the abstract as well as the concrete 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 some security
		  properties.
		  
		  Thus, we present a case study for the security analysis of
		  realistic models over an off-the-shelf system by formal
		  machine-checked proofs. },
  pdf		= {http://www.brucker.ch/bibliography/download/2003/fmics_03.pdf}
		  ,
  ps		= {http://www.brucker.ch/bibliography/download/2003/fmics_03.ps.gz}
		  
}