Re: [isabelle] New in the AFP: Sigma Protocols and Commitment Schemes



> 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?


--
  Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.