A Formalization of Declassification with WHAT-and-WHERE-Securityby Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer23 Apr