Email Gateway (Aug 22 2022 at 20:42): Email Gateway (Aug 22 2022 at 20:42):From: Lawrence Paulson <lp15@cam.ac.uk>
This new entry is by David Butler and Andreas Lochbihler:
We use CryptHOL to formalise commitment schemes and Sigma-protocols. Both are widely used fundamental two party cryptographic primitives. Security for commitment schemes is considered using game-based definitions whereas the security of Sigma-protocols is considered using both the game-based and simulation-based security paradigms. In this work, we first define security for both primitives and then prove secure multiple case studies: the Schnorr, Chaum-Pedersen and Okamoto Sigma-protocols as well as a construction that allows for compound (AND and OR statements) Sigma-protocols and the Pedersen and Rivest commitment schemes. We also prove that commitment schemes can be constructed from Sigma-protocols. We formalise this proof at an abstract level, only assuming the existence of a Sigma-protocol; consequently, the instantiations of this result for the concrete Sigma-protocols we consider come for free.
You’ll find it online at https://www.isa-afp.org/entries/Sigma_Commit_Crypto.html.
Incidentally, you might want to take look at the session graph:
https://www.isa-afp.org/browser_info/current/AFP/Sigma_Commit_Crypto/session_graph.pdf
This entry depends on numerous other AFP entries, showing the extent to which material here can be reused.
Larry
Email Gateway (Aug 22 2022 at 20:42):From: Peter Lammich <lammich@in.tum.de>
You’ll find it online at
https://www.isa-afp.org/entries/Sigma_Commit_Crypto.html.Incidentally, you might want to take look at the session graph:
https://www.isa-afp.org/browser_info/current/AFP/Sigma_Commit_Crypto/session_graph.pdf
This entry depends on numerous other AFP entries, showing the extent
to which material here can be reused.
Hi.
I had a quick look at it, and it seems to contain the whole Refinement
Framework stuff, only because CryptoHOL uses MFMC_Countable, which, in
MFMC_Finite.thy re-uses a termination proof of the Ford-Fulkerson
Algorithm from EdmondsKarp_Maxflow.
The theories it imports DO NOT depend on the Refinement Framework (I
invested some work here to make the abstract network flow theory
independent from the implementation). Nevertheless, the theory graph
contains everything used by any theory in EdmondsKarp_Maxflow, so is
not particularly precise here.
Does this indicate a problem with the theory graph generation, or a
problem with the session setup in the Edmonds-Karp AFP entry?
Email Gateway (Aug 22 2022 at 20:49):From: Makarius <makarius@sketis.net>
Concerning the session graph display: there is always a bit of
variability in what to show and what to hide; included is a trimmed-down
version according to Isabelle/79d23e6436d0.
Makarius
Email Gateway (Aug 22 2022 at 20:49):From: Makarius <makarius@sketis.net>
Here is the missing attachment.
Makarius
session_graph.pdf
Last updated: Apr 24 2024 at 16:18 UTC