| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
| Title: | An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties |
| Authors: | Oliver Bračevac (bracevac /at/ st /dot/ informatik /dot/ tu-darmstadt /dot/ de), Richard Gay (gay /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de), Sylvia Grewe (grewe /at/ st /dot/ informatik /dot/ tu-darmstadt /dot/ de), Heiko Mantel (mantel /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de), Henning Sudbrock (sudbrock /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de) and Markus Tasch (tasch /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de) |
| Submission date: | 2018-05-07 |
| Abstract: | 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. |
| BibTeX: |
@article{Modular_Assembly_Kit_Security-AFP,
author = {Oliver Bračevac and Richard Gay and Sylvia Grewe and Heiko Mantel and Henning Sudbrock and Markus Tasch},
title = {An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties},
journal = {Archive of Formal Proofs},
month = may,
year = 2018,
note = {\url{http://isa-afp.org/entries/Modular_Assembly_Kit_Security.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |