Part 5 - Security Protocols Modeling and Verification (Command Line)

These exercises use the command line interface. Alternatively you can use the Eclipse based AnBx-IDE

Create a folder AnB inside the folder
Our working directory is now \AnB

We are going to use the OFMC model checker to verify some security protocols specified with the AnB language (Alice and Bob).

Download ofmc.zip and unzip it. (This is an executable for Windows 64-bit). A version for Mac can be downloaded here.
Download also the following AnB files

• AnBx_from_A.AnB
• AnBx_from_A_Secret.AnB
• Fresh_From_A.AnB
• Fresh_From_A_Secret.AnB

Documentation

• OFMC Manual and Tutorial (S.Mödersheim)

TASK 1 - Protocol Verification

ofmc --numSess 1 AnBx_from_A.AnB

to verify the protocol for one session

You can verify the protocol for 2 parallel sessions

ofmc --numSess 2 AnBx_from_A.AnB

Is the protocol "safe"? Compare the verification time for 1,2,3,... sessions. Why the verification time is increasing?

N.B. If you are using the command line, please use the files with AnB extension (not AnBx).

TASK 2 - Authentication

Edit AnBx_From_A.AnBx

substitute this line  A -> B: {B,Msg}inv(sk(A)) with A -> B: {Msg}inv(sk(A))

save the file. Do you think the protocol is still "safe"? Why?

Run now OFMC for 1 and 2 sessions and check if your conjecture holds and try to understand why.

TASK 3 - Weak vs Strong Authentication

Edit AnBx_From_A.AnBx and remove the keyword weakly from the authentication goal.

Verify the protocol.

If the goals fail, explain why.

TASK 4 - Protocol verification

Run OFMC for the other protocols. Are they safe? (1 and 2 sessions)

Try to "break" the protocol, changing the specification, and violate the security goals. Try to understand the protocol behaviour, and the verifier output.

TASK 5 - Key-establishment protocol (optional)

Download the Protocol Security Verification Tutorial by S.Mödersheim.

Section 2 describes an example of building a Key-Establishment Protocol. You can build step by step a protocol answering a security problem at each step.

N.B.: If you are using the AnBx-IDE, and you want to use the .AnBx extension, you woul need to rename the .AnB files to .AnBx, open the files and add AnB after the protocol name in line 1.

Example:    Protocol AnBx_From_A  ->  Protocol AnBx_From_A AnB

TASK 6 - Implementation of security protocols in Java

Based on the examples developed in the previous parts of the tutorial, try to write the Java code of the protocol AnBx_From_A.AnBx
Along with the action performed by honest agents it is crucial to specify the check each agent has to perform on the incoming messages.

You can complete the same task for the other protocols.