@InProceedings{	  mantel:preserving-information-flow-properties-under-refinement:2001,
  abstract	= {In a stepwise development process, it is essential
		  thatsystem properties that have been already investigated
		  insome phase need not be re-investigated in later phases.
		  Informal developments, this corresponds to the
		  requirementthat properties are preserved under refinement.
		  While safetyand liveness properties are indeed preserved
		  under moststandard forms of refinement, it is well known
		  that this is,in general, not true for information flow
		  properties, a largeand useful class of security properties.
		  In this article, wepropose a collection of refinement
		  operators as a solutionto this problem. We prove that these
		  operators preserve informationflow as well as other system
		  properties. Thus,information flow properties become
		  compatible with stepwisedevelopment. Moreover, we show that
		  our operatorsare an optimal solution.},
  address	= {Oakland, CA, USA},
  author	= {Heiko Mantel},
  booktitle	= {Proceedings of the 22nd IEEE Symposium on Security and
		  Privacy (S&P)},
  month		= {May 14--16},
  pages		= {78--91},
  pdf		= {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2001/2001ieee-ssp.pdf},
  ps		= {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2001/2001ieee-ssp.ps.zip},
  publisher	= {IEEE Computer Society},
  title		= {{Preserving Information Flow Properties under
		  Refinement}},
  year		= 2001
}