On the development and formalization of an extensible code generator for real life security protocols

Abstract

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 v1.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. © 2012 Springer-Verlag.