Autori: Michael Backes, Alex Busenius, Catalin Hritcu

Editorial: Springer, 4th NASA Formal Methods Symposium (NFM 2012), p.371-387, 2012.

Rezumat:

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.

Cuvinte cheie: security protocols, code generation, translation, machine-checked proofs, type system

URL: http://www.infsec.cs.uni-saarland.de/~hritcu/publications/expi2java-nfm2012.pdf