This paper introduces Expi2Java, a new code generator for cryptographic protocols that translates models written in an extensible variant of the Spi calculus into executable code in a substantial fragment of Java, featuring concurrency, synchronization between threads, exception handling and a sophisticated type system with generics and wildcards. Our code generator is highly extensible and customizable, which allows it to generate interoperable implementations of complex real life protocols from detailed verified specifications. As a case study, we have generated an interoperable implementation of TLS v 1.0 client and server from a protocol model verified with ProVerif. Furthermore, we have formalized the translation algorithm of Expi2Java using the Coq proof assistant, and proved that the generated programs are well-typed if the original models are well-typed. This constitutes an important step towards the first machine-checked correctness proof of a code generator for cryptographic protocols.
展开▼
机译：本文介绍了Expi2Java，一种用于加密协议的新代码生成器，它将在SPI微积分的可扩展变体中写入的模型转换为Java的大量片段中的可执行代码，具有与泛型的线程，例外处理和复杂类型系统之间的并发性，同步和通配符。我们的代码生成器是高度可扩展和可自定义的，它允许它从详细验证规范生成复杂实际协议的可互操作性实现。作为一个案例研究，我们从用纤维原验证的协议模型生成了TLS V 1.0客户端和服务器的可互操作实现。此外，我们使用COQ验证助手正式化了Expi2Java的翻译算法，并证明了如果原始型号符合良好的型号，则生成的程序是良好的键入。这构成了朝着加密协议的代码发生器的第一个机器检查正确证明的重要步骤。
展开▼
