logo screenshot
elyjah lyte papers downloads

Elyjah is a software tool which developers can use to increase their understanding of security protocols and also help them develop more secure programs. Security protocols can be represented using the LySa process calculus. This method of representing protocols is both precise and concise, however is rather confusing to those who haven't spent time learning the syntax. Even more usefully, a protocol represented in LySa can be analysed using the LySatool to determine how secure it is.

Wouldn't it be useful for it to be possible to automatically analyse actual implementations of protocols rather than an abstract academic model? Elyjah converts implementations into a LySa representation, thus opening up automatic security anlaysis of java implementations of protocols.

Encryption

Security protocols use encryption extensively. Encrypting a message means that nobody can read it unless they know a key which will allow them to decrypt the message. As well as allowing a message to be kept secret, using encryption allows two principals to prove that they are who they claim to be. If one person sends another an encrypted message and only one person knows the key needed to decrypt it, if that person then replies with an unencrypted version of the message then we know that they are not an imposter.

Protocols

Security protocols are a series of messages between two or more principals. The purpose of the protocol may be to prove the identity of one or more of the principals, securely share some secret or some combination of these. Encryption is heavily used in protocols, both to encrypt secrets and also to provide authentication methods. It is notoriously hard to design a security protocol correctly such that it is impossible for anyone else to decrypt part of a message and learn a secret or be able to be authenticated as someone else.

Elyjah output of the Wide Mouth Frog Protocol implementation

Below is the LySa code representing the Wide Mouth Frog protocol. This was generated from a Java program which, like all ELyjah inputs, is a fully runnable program capable of prouding debugging and diagnosis logs at the developer's wishes. This implementation is as succinct as possible but is still four pages long. This

(new KAS) (new KBS) (
    !(new K) (new msg1) (new msg2)
   <A,S,A,{B,K} : KAS [ at a1 dest {s1} ] >.
   <A,B,{msg1,msg2} : K [ at a2 dest {b2} ] >.0
|
    !(S,B;msgToBeDecoded).
   decrypt msgToBeDecoded as {A;KAB}:KBS [ at b1 orig {s2} ] in
   (A,B;msgToBeDecoded2).
   decrypt msgToBeDecoded2 as {;msg1,msg2}:KAB [ at b2 orig {a2} ] in 0
|
    !(A,S,A;msgToBeDecoded).
   decrypt msgToBeDecoded as {B;keyRepresentation}:KAS [ at s1 orig {a1} ] in
   <S,B,{A,keyRepresentation} : KBS [ at s2 dest {b1} ] >.0
)

Output of the LySatool

The following is part of the output from the LySatool when presented with the output given above. It clearly states that the protocol is secure, and even if the developer doesn't understand the LySa code itself, they can understand that one sentance.

Values that may not be confidential
{LB, LK}LKAS[at a1 dest { s1 }], {LA, LkeyRepresentation}LKBS [at s2 dest { b1 }], {Lmsg1, Lmsg2}LK [at a2 dest { b2 }], n, m+, m-, S, B, A, {l, l}l [at CPDY]
Violation of authentication properties (ψ)
No violations possible

In Summary...

Elyjah allows a developer to utilise the properties of LySa and the powers of the LySatool without having to actually understand either of them!

More information, references and details of implementation and experiments can be found in my project report.

logo
LFCS
Laboratory for Foundations of Computer Science
logo