Alex Busenius and me are pleased to announce that Expi2Java 1.6 was released two days ago. And by the way, Alex has recently finished his MSc and is looking for a job in industry. If you know anything interesting in a German or English speaking country, please let him know.

Expi2Java 1.6 was released yesterday (11.05.2011)

The highlights of this release are the new symbolic library and a mechanized formalization in Coq.

The symbolic library abstracts away cryptographic primitives as symbolic terms and networking as pi-calculus-like channels. It is designed to be sound and simple enough to simplify proving the transformation secure. Both the symbolic and concrete libraries can be used interchangeably with all provided examples.

We have formalized the transformation from Expi Calculus to a subset of Java performed by Expi2Java using the Coq proof assistant and proved the symbolic library and the produced Java code to be well-typed. The formalization and all proofs can be found on the project homepage.

The full list of changes: Read the rest of this entry »