Email Gateway (Aug 22 2022 at 18:50): Email Gateway (Aug 22 2022 at 18:50):From: Lawrence Paulson <lp15@cam.ac.uk>
Andreas Lochbihler and S. Reza Sefidgar have continued their stream of crypto-related work with a new entry entitled Constructive Cryptography in HOL:
Inspired by Abstract Cryptography, we extend CryptHOL, a framework for formalizing game-based proofs, with an abstract model of Random Systems and provide proof rules about their composition and equality. This foundation facilitates the formalization of Constructive Cryptography proofs, where the security of a cryptographic scheme is realized as a special form of construction in which a complex random system is built from simpler ones. This is a first step towards a fully-featured compositional framework, similar to Universal Composability framework, that supports formalization of simulation-based proofs.
It is online at https://www.isa-afp.org/entries/Constructive_Cryptography.html. Many thanks to them!
Larry Paulson
Last updated: Apr 20 2024 at 04:19 UTC