wiki:WikiStart
Last modified 2 years ago Last modified on 04/10/12 16:40:24

Expi2Java

Expi2Java is an extensible code generator for cryptographic protocols. It takes protocol specifications written in an extensible variant of the Spi calculus, configurations that provide the low-level information needed for code generation and produces interoperable Java code. The main features of Expi2Java are:

  • High customizability and extensibility
    • User-defined types, cryptographic primitives and low-level configurations
    • User-provided implementation classes
    • Code generation using code templates
  • An expressive type system prevents incorrect use of crypto primitives and configurations
    • The type-checker performs type inference, which decreases the annotation burden on the user
    • The type-checker catches errors early and provides helpful error messages
    • When type-checking the specification succeeds the tool is guaranteed to generate a well-typed Java program (modulo implementation bugs and bad customizations)
  • Input language compatible with ProVerif protocol verifier
  • Interoperable generated code
    • Generated implementation uses Java cryptographic providers
    • Most common cryptographic primitives and data types are supported out of the box
    • Full control over the low-level data format
    • As a case study, we have generated an interoperable implementation of TLS v1.0 client and server from a protocol model verified with ProVerif
  • Free software (GPL v3) developed in the open
  • Well-documented (see User Manual and Code Generation Tutorial)
  • New: Symbolic crypto + networking library
    • Abstracts crypto primitives as symbolic terms and networking as pi-calculus-like channels
    • Useful for local testing and debugging, as well as for our proofs
    • Concrete and symbolic libraries can be used interchangeably with all provided examples
  • New: Mechanized formalization and proofs in the Coq proof assistant

News

Research

Documentation

Download

Implementation by Alex Busenius. GNU GPL, Version 3

  • Expi2Java 1.6, 11.05.2011 [8.8 MiB, SHA1: 164ce45c8121bdac9adcfc88e54ec12e1d4cc11c]

Formalization by Alex Busenius. GNU LGPL, Version 3

Credits

Expi2Java originated as an extension of the Spi2Java framework by Davide Pozza, Alfredo Pironti, Riccardo Sisto and Luca Durante, and still uses a little of the Spi2Java code.

Bug Tracker

To create a new ticket use the New Ticket button.

Mailing List

Announcements and discussions around Expi2Java can be found on our mailing list.

Wiki

As all Wiki pages, this page is editable, this means that you can modify the contents of this page simply by using your web-browser. Simply click on the "Edit this page" link at the bottom of the page. WikiFormatting will give you a detailed description of available Wiki formatting commands.