@Article{	  WHATandWHERE_Security-AFP,
  author	= {Sylvia Grewe and Alexander Lux and Heiko Mantel and Jens
		  Sauer},
  title		= {A Formalization of Declassification with
		  WHAT-and-WHERE-Security},
  journal	= {Archive of Formal Proofs},
  month		= apr,
  year		= 2014,
  note		= {\url{http://afp.sf.net/entries/WHATandWHERE_Security.shtml},
		  Formal proof development},
  issn		= {2150-914x}
}