Provided by: Saarland University
Date Added: Jan 2012
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.