This repository contains formalizations of some of the theories presented in the lecture "Grundlagen der Sicherheitsanalyse und des Designs" for the interactive theorem prover Isabelle.
Currently, it contains formalizations of
- noninterference à la Goguen-Meseguer, and
- reference monitors à la Rushby.
Formalizations of some of the other parts of the lecture are available elsewhere. For example, the Volpano-Smith security type system can be found here in the Archive of Formal Proofs.