Elyjah
 

A security analyzer for Java implementations of communications protocols

Elyjah converts Java implementations of secure communications protocols into the LySa process calculus. Elyjah is itself written in Java. The LySa process calculus output from Elyjah can be directly processed by the LySatool, an efficient static analyser for the language which can detect security flaws in communications protocols.

Elyjah

To be a valid input for Elyjah Java implementation of communications protocols must adhere to the Elyjah implementation rules as described in the documentation. It is highly unlikely that the current release of Elyjah will be able to process an arbitrary implementation of a protocol in Java.

Example

Given an example like this: 

/*
 * TestEasySendReceiveEncrypt.java
 *
 * Created on 16 November 2005, 11:13
 *
 */
import java.util.Vector;
import javax.crypto.*;
/**
 *
 * @author Nicholas O'Shea
 */
public class TestEasySendReceiveEncrypt extends KeyGenerationClass {
    public static void main(String[] args) {      
        Network net = new Network();
        A a = new A(net);
        net.register("A", a);
        B b = new B(net);
        net.register("B", b);
 
        SecretKey key = generateSharedKey();
        net.shareKey(key, "K");
        
        b.start();
        a.start();
    }
}

class A extends ComClass {
    Network net;
    
    
    public A (Network net){
        this.net = net;
    }
    
    public void  run(){
        Vector v = new Vector();
        v.add("A");
        String msg = generateMessage("this is a message");
        Vector vEnc = new Vector();
        vEnc.add(msg);
        SecretKey key = (SecretKey) keys.get("K");
        v.add(encrypt(vEnc, key, "a", "b"));
        net.send(this, "B", v);
        


    }
    
    public void processIncoming(Vector<String> v){
        switch (receivedNum) {
            case 0 :
        }
    }
    
}
class B extends ComClass {
    Network net;
    
    
    public B (Network net){
        this.net = net;
    }
    
    public void processIncoming(Vector<String> v){
        switch (receivedNum) {
            case 0 :
                assert (check(v.elementAt(0), "A"));
                assert (check(v.elementAt(1), "B"));
                String source = v.elementAt(2);
                String msgToBeDecoded = v.elementAt(3);
                SecretKey key = (SecretKey) keys.get("K");
                Vector<String> decode = decrypt(msgToBeDecoded, key, "b", "a");
                String message = decode.elementAt(0);
                
                theLogger.info(source);
                theLogger.info(msgToBeDecoded);
                theLogger.info(message);
        }
    }
    
}

We run Elyjah like this: 

java -jar elyjah.jar testcases/TestEasySendReceiveEncrypt.java -lysatool

to obtain this output: 

(new K) (
!(new msg) <A,B,A,{msg} : K [ at a dest {b} ] >.0
|
!(A,B;source,msgToBeDecoded). decrypt msgToBeDecoded as {;message}:K [ at b orig {a} ]  in 0
)

Documentation

You can read about Elyjah in this document.

Download Elyjah

Elyjah is available for download as a Java archive.

Testcases

You can obtain an archive of Elyjah test cases implementing simple protocols in Java.

Sample outputs

You can obtain an archive of Elyjah test cases together with the corresponding output from Elyjah.

Running the Java implementations

The Java implementations which are input to Elyjah can be executed on the JVM but require a small number of supporting classes.

README

Simple instructions for getting started with Elyjah.

Usage:

java -jar elyjah.jar [FileName]...
Options:
	-lysatool   	Replaces 'v' with 'new'. 
			Allows direct input into the lysatool
        -toFile 	Outputs to a file named after the Java input with .lysa extension
	--XMLtoFile	Generates XML Files of abstract syntax tree before and after

Example 1 (Windows):
	java -jar elyjah.jar testcases\TestEasySend.java -lysatool

Example 1 (Linux):
	java -jar elyjah.jar testcases/TestEasySend.java -lysatool


Example 2 (Windows):
	java -jar elyjah.jar testcases\TestEasySend.java -lysatool -toFile testcases\TestEasySend.lysa

Example 2 (Linux):
	java -jar elyjah.jar testcases/TestEasySend.java -lysatool -toFile testcases/TestEasySend.lysa
Last modified: Mon Jun 19 16:07:21 BST 2006 -- Validate this page.