CRMay 13, 2014
Compositional properties of crypto-based components
arXiv:1405.3006v18 citations
Originality Synthesis-oriented
AI Analysis
This work addresses formal verification challenges for cryptographic components, but it is incremental as it builds on existing formal methods without broad new breakthroughs.
The paper tackles the problem of verifying composition properties of crypto-based components by introducing a formalization of data secrecy in Isabelle/HOL+Isar, resulting in a set of theories with definitions and proofs for verification.
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.