Molly: A Verified Compiler for Cryptoprotocol Roles.
CoRR(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要