Email Gateway (Aug 22 2022 at 15:28): Email Gateway (Aug 22 2022 at 15:28):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
CryptHOL
by Andreas Lochbihler
CryptHOL provides a framework for formalising cryptographic arguments
in Isabelle/HOL. It shallowly embeds a probabilistic functional
programming language in higher order logic. The language features
monadic sequencing, recursion, random sampling, failures and failure
handling, and black-box access to oracles. Oracles are probabilistic
functions which maintain hidden state between different invocations.
All operators are defined in the new semantic domain of
generative probabilistic values, a codatatype. We derive proof rules for
the operators and establish a connection with the theory of relational
parametricity. Thus, the resuting proofs are trustworthy and
comprehensible, and the framework is extensible and widely applicable.
The framework is used in the accompanying AFP entry "Game-based
Cryptography in HOL". There, we show-case our framework by formalizing
different game-based proofs from the literature. This formalisation
continues the work described in the author's ESOP 2016 paper.
Enjoy 4/5
Last updated: Apr 26 2024 at 20:16 UTC