Molly is a program that compiles cryptographic protocol roles written in a high-level notation into straight-line programs in an intermediate-level imperative language, suitable for implementation in a conventional programming language. We define a denotational semantics for protocol roles based on an axiomatization of the runtime. A notable feature of our approach is that we assume that encryption is randomized. Thus, at the runtime level we treat encryption as a relation rather than a function. Molly is written in Coq, and generates a machine-checked proof that the procedure it constructs is correct with respect to the runtime semantics. Using Coq's extraction mechanism, one can build an efficient functional program for compilation.

翻译：Molly是一个将高级符号语言编写的密码协议角色编译为中间级命令式语言直线程序（适用于常规编程语言实现）的编译工具。我们基于运行时系统的公理化定义，为协议角色建立了指称语义。本方法的一个显著特征在于我们假设加密过程是随机化的——这意味着在运行时层面将加密视为关系而非函数。Molly使用Coq实现，可生成经机器验证的证明，确保其所构造过程符合运行时语义。通过Coq的提取机制，可构建高效的函数式编译程序。