Email Gateway (Mar 18 2021 at 07:52): Email Gateway (Mar 18 2021 at 07:52):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
there is a new AFP entry available:
Constructive Cryptography in HOL: the Communication Modeling Aspect
by Andreas Lochbihler and S. Reza Sefidgar
Abstract:
Constructive Cryptography (CC) introduces an abstract approach to composable security statements that allows one to focus on a particular aspect of security proofs at a time. Instead of proving the properties of concrete systems, CC studies system classes, i.e., the shared behavior of similar systems, and their transformations. Modeling of systems communication plays a crucial role in composability and reusability of security statements; yet, this aspect has not been studied in any of the existing CC results. We extend our previous CC formalization with a new semantic domain called Fused Resource Templates (FRT) that abstracts over the systems communication patterns in CC proofs. This widens the scope of cryptography proof formalizations in the CryptHOL library. This formalization is described in Abstract Modeling of Systems Communication in Constructive Cryptography using CryptHOL [1].
https://www.isa-afp.org/entries/Constructive_Cryptography_CM.html
Enjoy,
René
[1]: http://www.andreas-lochbihler.de/pub/basin2021.pdf
Last updated: Apr 23 2024 at 20:15 UTC