Molly：一个经过验证的密码协议角色编译器
密码学与安全
2023-11-27 v1
摘要
Molly 是一个将用高级记号书写的密码协议角色编译为中级命令式语言中线型程序的程序，适于在常规编程语言中实现。我们基于运行时公理化为协议角色定义了指称语义。我们方法的一个显著特征是假设加密是随机化的。因此，在运行时层面我们将加密视为关系而非函数。Molly 用 Coq 编写，并生成机器可检查的证明，表明其构造的过程相对于运行时语义是正确的。利用 Coq 的提取机制，可构建高效的编译函数式程序。
引用
@article{arxiv.2311.13692,
title = {Molly: A Verified Compiler for Cryptoprotocol Roles},
author = {Daniel J. Dougherty and Joshua D. Guttman},
journal= {arXiv preprint arXiv:2311.13692},
year = {2023}
}