On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols

Download Now Date Added: Jan 2012
Format: PDF

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. The authors' 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, their have generated an interoperable implementation of TLS v1.0 client and server from a protocol model verified with ProVerif.