文件名称：csec-modex:验证C中的加密协议实现
文件大小：5.23MB
文件格式：ZIP
更新时间：2024-05-19 23:40:04
OCaml
这是Mihhail Aizatulin，Andy Gordon和JanJürjens撰写的“通过符号执行从C协议代码提取和验证密码模型”和“通过符号执行对C协议实现的计算验证”中描述的验证方法的实现。 该发行版包括在论文中分析的协议的源代码：CSur，simple mac，simple xor，RPC，RPC-enc和NSL。 不幸的是，由于许可限制，我们无法分发计量协议的源代码。 ProVerif验证工具正在被重写，目前无法使用。 下载 git clone git://github.com/tari3x/csec-modex.git 不要使用github提供的zip文件，因为它会破坏符号链接。 依存关系 发行版将捆绑并自动构建大多数依赖关系，但以下情况除外： gcc，ocaml，cmake，openssl，polarssl，markdown Yices SMT求解器，由于许可限制