Sylvia Grewe et al. published three entries in the Isabelle Archive of Formal Proofs: A Formalization of Assumptions and Guarantees for Compositional Noninterference, A Formalization of Strong Security, and A Formalization of Declassification with WHAT-and-WHERE-Security.