Compositional properties of crypto-based components
Maria Spichkova
TL;DR
This paper introduces a formal framework using Isabelle/HOL+Isar to specify and verify the compositional security properties of crypto-based components, focusing on data secrecy.
Contribution
It provides a novel formalisation and verification approach for cryptographic component composition using Isabelle/HOL+Isar.
Findings
Formalisation of data secrecy property
Verification of composition properties
Framework for cryptographic component analysis
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Distributed systems and fault tolerance · Mass Spectrometry Techniques and Applications