Part 5 - Security Protocols Modeling and Verification (with AnBx-IDE)

These exercises require the AnBx-IDE. Alternatively you can use the command line interface version.

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

Documentation

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

TASK 0 - Configuration of the plugin and verifiers

Install and configure the AnBx-IDE as described here (requires Eclipse).

In Eclipse, create a new AnBx project. (File -> New -> Project -> AnBx -> AnBx Project)

Download the following AnBx files and copy them in the src folder.

• AnBx_From_A.AnBx
• AnBx_From_A_Secret.AnBx
• Fresh_From_A.AnBx
• Fresh_From_A_Secret.AnBx

TASK 1 - Protocol Verification

N.B.: The detailed explaination on how to run the tools under Eclipse is available here.

1. In Eclipse, open the AnBx_From_A.AnBx file.
2. Configure OFMC to verify protocols for one session. Click on the OFMC button on the toolbar and set "Number of sessions" to 1.
3. Run the AnBx compiler (Click on the AnBxC button on the toolbar) to convert the AnBx file to AnB and launch OFMC.
4. Set the "Output format" to AnB, and check the "Launch associate validator" option.
5. Click on OK to verify the protocol for one session.
6. Now repeat the same operation for 2 parallel sessions.

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.