[isabelle] New in the AFP: An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties



Dear all,

I’m happy to announce a new AFP entry from TU Darmstadt. 
The entry consists of a framework to specify and verify security properties.

Cheers,
René


An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
  by Oliver Bračevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock, and Markus Tasch


The "Modular Assembly Kit for Security Properties" (MAKS) is
a framework for both the definition and verification of possibilistic
information-flow security properties at the specification-level. MAKS
supports the uniform representation of a wide range of possibilistic
information-flow properties and provides support for the verification
of such properties via unwinding results and compositionality results.
We provide a formalization of this framework in Isabelle/HOL.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.