ssprove:Coq中模块化密码证明的基础框架 源码

SSProve:Coq中模块化密码证明的基础框架 该存储库包含论文结果的Coq形式化: SSProve:Coq中模块化密码证明的基础框架。 胭脂红(Carmine Abate),菲利普·G·哈瑟尔沃特(Philipp G. 2021年3月 本自述文件可作为安装此项目的指南,以及在白皮书中的声明与Coq中的形式证明之间的对应关系,以及列出形式化所依赖的一小套标准公理(主要是通过使用mathcomp-analysis进行mathcomp-analysis ) 。 先决条件 迷彩 8.12.0 方程1.2.3+8.12 Mathcomp分析0.3.2 Coq挤出物0.2.2 您可以从ocaml的opam软件包管理器中获取它们: opam repo add coq-released https://coq.inria.fr/opam/released opam update opam