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:
- Removed support for user-provided imports. All implementation classes should be included into the used implementation library
- Refactored concrete library
- A symbolic library can now be generated from the provided configuration
- Both concrete and symbolic libraries can be used interchangeably with all provided example protocols
- New restrictions for the type of constructors:
- The return type can no longer be a type variable
- All type variables used in the type of an Expi constructor must appear in its return type
- Return type can no longer be Top (unimplementable)
- Constructors used in the destructor declarations must always be annotated
- Changes to the type inference algorithm:
- The variables from the right side of the reduction rule are no longer used to infer type of the variables on the left side of the reduction rule
- More precise type inference in some cases
- Changed the set of default types
- Merged Expi types String and ConstString to ExpiString
- Changed variance of some default types to avoid problems with destructor inconsistency
As always, an updated version of the documentation is available as well.
Please take a look at the project homepage for more details and download links: