Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: An Isabelle/HOL Formalization ...


view this post on Zulip Email Gateway (Aug 22 2022 at 17:15):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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.


Last updated: Apr 25 2024 at 08:20 UTC