Compositional properties of crypto-based components
arXiv:1405.3006
Abstract
This paper presents an Isabelle/HOL+Isar set of theories which allows to specify crypto-based components and to verify their composition properties wrt. cryptographic aspects. We introduce a formalisation of the security property of data secrecy, the corresponding definitions and proofs.
Preprint. Archive of Formal Proofs, 2014, ISSN: 2150-914x