source: trunk/README @ 49634

                                   Expi2Java
                                   ---------
This is the README for Expi2Java, an extensible code generator for security
protocols.

The protocols are written in a variant of Spi calculus. A type system is used to
provide the needed type information and low-level implementation details for
every term and perform consistency checks.


LICENSE
--------------------------------------------------------------------------------
Expi2Java is free software: you can redistribute it and/or modify it under the
terms of the GNU General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

Expi2Java is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
A PARTICULAR PURPOSE. See the GNU General Public License for more details.


Copyright (c) 2008-2011 Alex Busenius


Expi2Java originated as an extension of the Spi2Java framework and still uses
some of the Spi2Java code.

Copyright (c) 2002-2008 Davide Pozza, Alfredo Pironti, Riccardo Sisto


See COPYING for the copy of GPL-3 license.


CONTACT & INFO
--------------------------------------------------------------------------------
Expi2Java is a research prototype and is continuously under development. Feel
free to contact us if you encounter some problems, feedback and suggestions are
very appreciated.

The homepage of the project is:

    http://www.infsec.cs.uni-sb.de/projects/expi2java

Bugs can be reported using the public bug tracker at:

    http://www.infsec.cs.uni-sb.de/projects/expi2java/newticket

We have a mailing list for announcements and discussions about Expi2Java:

    http://groups.google.com/group/expi2java

If you do not have a google account, you can join the mailing group by sending
a mail to:

    expi2java-subscribe@googlegroups.com


BUILD & INSTALL
--------------------------------------------------------------------------------
You can either build Expi2Java from source or use the provided JARs.
Building from source is necessary if you want to extend the provided set of
supported implementations of cryptographic primitives and data types.

NOTE (especially WINDOWS users):
Expi2Java is written in Java and will (probably) also work on any operating
systems. However, it was only tested on Linux and MacOS X.
The provided shell scripts are NOT needed for the Expi2Java to work, their
purpose is only to simplify invocation by setting some default options and Java
class path.


Build prerequisites:

* Ant 1.7 or newer
* Java JDK 1.6


To build Expi2Java, type

    $ ant


To install in /usr/bin and /usr/share (WARNING: Linux-only), type as root

    $ ant install

To install somewhere else, e.g. in /xxx/yyy (Linux and MacOS), type (as root if needed)
NOTE: The prefix should not contain shell extensions like ~

    $ ant install -Dprefix=/xxx/yyy


To uninstall, type as root

    $ ant uninstall

OR, if you have installed into /xxx/yyy, type (as root if needed)

    $ ant uninstall -Dprefix=/xxx/yyy


To remove all generated files, type

    $ ant clean


USAGE
--------------------------------------------------------------------------------
The bin/ directory contains two JAR files, eXpi2Java.jar and eXpiLibrary.jar

eXpi2Java.jar
Is the main program, it needs jalopy.jar, log4j.jar and bcprov-jdk16-141.jar
from the lib/ directory.

eXpiLibrary.jar
Is the library, containing the implementations of cryptographic primitives and
data types used by the generated code.


The implementation of cryptographic primitives rely on Java cryptographic
providers. The default configurations in configs.exdef use SunJCE, SUN and
BC (bouncy castle, see lib/bcprov-*.jar) providers.


Expi2Java can perform 4 basic actions:
* pretty-print an *.exdef file
* pretty-print an *.expi file
* type-check a protocol given as an *.expi file
* generate Java implementation of a protocol

Run the main program with the -h or --help switch to print the help on possible
parameters.


Linux/MacOSX/*n?x users can also use the provided scripts (run them without
parameters for short usage help):
* expi2java                 - Encapsulates the main program.
* parseExdef                - Preselects parameter for parsing exdef files
* parseExpi                 - Preselects parameter for parsing expi files
* typeCheckExpi             - Preselects parameter for running type-checker
* generateAllTests.sh       - Generates Java implementation of several examples (no help screen available)
* generateTlsChannel.sh     - Generates Java implementation of the TLS channel in the library (no help screen available)
* run-protocol.sh           - Runs one of the generated protocol implementations
* generate-key-and-cert.sh  - Creates the keys, certificate and CA key used by TLS server


DOCUMENTATION
--------------------------------------------------------------------------------
Please refer to the user manual for more detailed description of usage, calculus,
customizing Expi2Java and extending the implementation library.

We provide a code generation tutorial with a detailed explaination of the code
generation process on example of the Perrig-Song protocol.
The tutorial covers all needed steps from writing a formal protocol
specification to running the generated code.

JavaDoc development documentation can be generated by running

    $ ant docs

The generated files are placed in docs/javadoc/, to view it, open the file
docs/javadoc/index.html with your favorite browser.


CONTENTS
--------------------------------------------------------------------------------
The Expi2Java distribution contains:

- In the root directory:
    This README, NEWS file describing important changes, GPL license, various helper scripts

- bin/ directory:
    JAR files with the main program (eXpi2Java.jar) and the library (eXpiLibrary.jar)
    These JARs are generated when building the project

- data/ directory:
    Various code template files used in code generation phase

- docs/ directory:
    The user manual, code generation tutorial and JavaDoc development documentation

- lib/ directory:
    Some JAR files used by the Expi2Java framework, in particular, a Java code
    formatter, its dependencies, additional ANT tasks and the BouncyCastle
    security provider.
    All shipped libraries are released under GPL-compatible licenses. More
    details can be found in lib/lib_info.txt

- manifests/ directory:
    Manifests generated during the build and used to create JAR files.

- src/ directory:
    Expi2Java source

- testCode/ directory:
    The protocol implementations generated by the generateAllTests.sh script are
    placed into this directory

- testData/ directory:
    Various examples of *.exdef and *.expi files.
    Most important, the set of default configurations (exdef/configs.exdef),
    type definitions (exdef/default.exdef) and some annotated protocol
    definitions (expi/tls.expi, expi/perrigsong.expi, expi/http.expi,
    expi/needham.expi, expi/andrew.expi, expi/fiaba.expi)

- vim/ directory:
    VIM syntax highlighting file for *.exdef, *.expi and *.pvi (ProVerif) files.
    Some scripts and vim settings files for JavaDoc warnings filtering.


vim: tw=80