2023/11/22 by Daniel J. Dougherty, Dougherty, Daniel J., Joshua D. Guttman +1
Computer Science · #Advanced Malware Detection Techniques #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic, programming, and type systems #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2311.13692
openalex publication_date 2023/11/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.