Molly: A Verified Compiler for Cryptoprotocol Roles
Cryptography and Security
2023-11-27 v1
Abstract
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.
Keywords
Cite
@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}
}