Part 7 - Automatic Generation of Specifications and Implementations of Attacks on Security Protocols

We will automatically generate attack scenarios, both in AnBx and Java, using the AnBx Compiler and the OFMC model checker.

Instructions are provided for both the command line and the Eclipse AnBx IDE option.
However, we strongly recommend using Eclipse, as it simplifies the configuration and utilization of the tool.

Before attempting these tasks, double check that your environment is configured as discussed in Part 6.

For these tasks, we will use the WooLam1.AnBx file as an example. This protocol is vulnerable to a reflection attack that OFMC can identify and provide an attack trace for.

TASK 1 - Attack Trace Reconstruction - Command Line

Export the WooLam1 protocol to AnB first:

anbxc WooLam1.AnBx -out:AnB

This will generate the AnB specification file WooLam1.AnB.

The next step is to run OFMC on it to verify the protocol:

ofmc --numSess 1 WooLam1.AnB

You should obtain an attack trace, similar to what you encountered in Part 5.

ATTACK TRACE:
i -> (x501,1): x502
(x501,1) -> i: NB(1)
i -> (x501,1): NB(1)
(x501,1) -> i: {|x502,x501,NB(1)|}_(shk(x501,s))
i -> (x501,1): {|x502,x501,NB(1)|}_(shk(x501,s))

% Reached State:
%
% request(x501,x502,pBANB,NB(1),1)
% state_rB(x501,3,shk(x501,s),s,x502,NB(1),NB(1),{|x502,x501,NB(1)|}_(shk(x501,s)),{|x502,x501,NB(1)|}_(shk(x501,s)),1)
% state_rA(x20,0,shk(x20,s),s,x25,1)
% state_rs(s,0,shk(x28,s),shk(x29,s),x28,x29,1)

While relatively close to an AnB notation, extensive knowledge of OFMC's internals is necessary to fully understand the attack trace.
Therefore, it is convenient to reconstruct this trace to the AnBx notation, so that it is possible to better understand the nature of the attack.

First, we export the trace into a file for later use, using output redirection:

ofmc --numSess 1 WooLam1.AnB > WooLam1_trace.ofmctrace

You will see that WooLam1_trace.ofmctrace file has been generated.

Second, we reconstruct this trace into the AnBx notation.

anbxc WooLam1.AnBx -out:AnB -ofmctrace WooLam1_trace.ofmctrace

This procedure will generate a file called WooLam1_AttackTrace.AnBx.

Protocol: WooLam1_AttackTrace

Types:
Agent Intr;
Agent A,B,s;
Number NB;
Function [Agent,Agent ->* SymmetricKey] shk;

Knowledge:
Intr: A,B,Intr,s,shk(Intr,s);
A: A,Intr,s,shk(A,s);
B: B,Intr,s,shk(B,s);
s: Intr,Intr,s,shk(Intr,s),shk(Intr,s)

Actions:
# A -> Intr: A
# Intr -> B: A
Intr -> B: Intr
B -> Intr: NB

# Intr -> A: NB
# A -> Intr: {|A,B,NB|}shk(A,s)

# Intr -> B: {|A,B,NB|}shk(A,s)
Intr -> B: NB

# B -> Intr: {|A,B,{|A,B,NB|}shk(A,s)|}shk(B,s)
B -> Intr: {|Intr,B,NB|}shk(B,s)

# Intr -> s: {|A,B,{|A,B,NB|}shk(A,s)|}shk(B,s)
# s -> Intr: {|A,B,NB|}shk(B,s)

# Intr -> B: {|A,B,NB|}shk(B,s)
Intr -> B: {|Intr,B,NB|}shk(B,s)

Goals:
# B authenticates A on NB
B authenticates Intr on NB

It contains translated trace actions and goals, but also displays the original actions  and goals as comments, so that you can compare the original specification and the attack strategy.
You will notice that a new agent Intr has been added. This is the intruder, and the actions the intruder performs constitute the attack on the protocol.

What do you observe?
Describe how the attack works.
Why do we call it a reflection attack?

Now that we have a more user-friendly description of the attack in AnBx, we can also generate an implementation of this attack scenario.
To do this, run the previous command line but with the "Java" output option:

anbxc WooLam1.AnBx -out:Java -ofmctrace WooLam1_trace.ofmctrace

This will generate both the Woolam1_AttackTrace.AnBx file and a Java implementation of the attack. You should see a new file in the /genAnBx/src folder for the WooLam1 protocol.

Use the build.xml Ant file in the generated folder for this attack to run the code, as seen in Part 6.

What happens? Observe the log of the protocol run.
Is the attack successful? Explain why.

TASK 2 - Attack trace reconstruction - Eclipse IDE

The Eclipse AnBx IDE plugin streamlines the trace reconstruction steps. Ensure that the plugin is installed and configured (see Part 5).

1. Open the WooLam1.AnBx file
2. Open the AnBxC dialog through F6 key or with the "AnBxC" toolbar button.
   Note: the file should already be under the casestudies folder if you have installed it from the AnBx distribution package.
3. Select the "AnB" output format and check Reconstruct OFMC Attack Trace.
   The appropriate commands will be automatically run for you: the file is first compiled to AnB, given to OFMC for verification, and the attack trace is stored in a temporary file that is fed to the compiler for reconstruction.
   You can visualize the commands execution in the console.

You will notice that a WooLam1_AttackTrace.AnBx file has been generated in the same folder where the WooLam1.AnBx is stored.
The file contains the original actions and goals in comments, and the translated trace actions and goals.

What do you observe?
Describe how the attack works.
Why do we call it a reflection attack?

With the file WooLam1_AttackTrace.AnBx we now have a more user-friendly description of the attack in AnBx.

We can also generate the implementation of this attack scenario.
To do this, reproduce the previous steps, but selecting the "Java" output format in the "AnBxC" dialog.

This will generate the Java code. This implementation can be run with the build.xml Ant file in the generated Java folder (/genAnBx/src/woolam1_attacktrace/), or directly if the Launch associated validator checkbox is on in the AnBxC dialog.

This will both generate the Woolam1_AttackTrace.AnBx file and a Java implementation of the attack.

After running this Java attack, what happens?
Observe the log of the protocol run.
Is the attack successful? Explain why.

TASK 3 - Attack trace reconstruction - Additional reading

Rémi Garcia and Paolo Modesti
Automatic Generation of Security Protocols Attacks Specifications and Implementations
Cyber Security and Applications, Volume 1, January 2024, 1000138, 2024

Rémi Garcia contributed to the development of this part of the tutorial