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

• 10.04.2012:  Looking for new maintainer(s)
• 31.01.2012:  Our paper about developing and formalizing Expi2Java was accepted at  NFM 2012.
• 11.05.2011: Released Coq Formalization and Proofs
• 11.05.2011: Expi2Java 1.6 release (changes)
• 29.07.2009: Expi2Java 1.5 release (changes)
• 06.05.2009: Expi2Java 1.4 release (changes)
• 20.04.2009: Expi2Java 1.3 release (changes)
• 17.03.2009: Expi2Java 1.2 release (changes)
• 07.03.2009: Expi2Java 1.1 release (changes)
• 10.12.2008: First Expi2Java release

Research

• New:  Michael Backes,  Alex Busenius,  Cătălin Hriţcu.  On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.  4th NASA Formal Methods Symposium (NFM 2012), pages 371-387. April 2012.
  •  Online appendix containing details that had to be omitted in the NFM paper due to the lack of space.
  •  Slides from NFM 2011 talk
•  Alex Busenius.  Mechanized Formalization of a Transformation from an Extensible Spi Calculus to Java, Master's Thesis, Information Security and Cryptography Group, Saarland University, Advisor:  Cătălin Hriţcu, 04.04.2011 [PDF 1.7 MB]
•  Alex Busenius.  Expi2Java - An extensible code generator for security protocols, Bachelor's Thesis, Information Security and Cryptography Group, Saarland University, Advisor:  Cătălin Hriţcu, 28.10.2008 [PDF 620 KiB]

Documentation

• Latest README
•  Expi2Java 1.6 User Manual, 11.05.2011 [PDF 415 KiB]
•  Expi2Java 1.6 Code Generation Tutorial, 11.05.2011 [PDF 262 KiB]
•  Expi2Java 1.6 Online Development Documentation (JavaDoc), 11.05.2011

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

•  Coq Formalization and Proofs, 12.05.2011 [369 KiB, SHA1: d785f195844f6ddc911ae3cf5a17218aa18ba14b]

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.