ASPASyA: Needham-Schroeder

Description of the protocol

As a case study we have considered the asymmetric Needham-Schroeder protocol and tested it for authentication. The protocol has been designed to achieve reciprocal authentication of two principal A and B by exchanging of secret nonces. The informal specification is:

(1) A --> B: {na, A}_B+ (2) B --> A: {na, nb}_A+ (3) A --> B: {nb}_B+
A sends B a message containing a fresh nonce na and its own identity. B then replays a message with na and its own nonce nb used to authenticate A. A ends the protocol by sending back nb to B.

cIP-calculus specification

cIP specification is quite straightforward:

A: (x) [out({(A, na)}x+).in({(na, ?y)}A-).out({y}x+)];
B: () [in({(?z, ?u)}B-).out({(u, nb)}z+).in({nb}B-)];

The open variable x is used by A as the placeholder for the name of its partner. Variable y stands for the nonce received by A. z and u are intended to hold the identity of the partner of B and the nonce B receives. Generally speaking, the protocol designer must specify open variables of principal. We can give some rule of thumbs:

Initiator usually needs an open variable which the responder should join;
if the identity of the partner is acquired in a communication no open variable is required from that partner;
an open variable might be necessary when a principal must interact with a server.

Invariant specification

ASPASyA begin the exploration of state space only from those initial states that satisfy an invariant property, discarding the others. Usually invariant properties are used to connect principals that share secrets. As this is not the case we show how invariants can be used to prune the state space allowing for refined search.

If we want to explore the whole state space we simply use as invariant:

true;

Indeed, all possible initial states satisfy true. If we want to test only the runs where there are Initiators and Responders we can specify:

(exists A.i: true) and (exists B.j: true);

This means that the initial states must contains at least an instance of A and an instance of B.

Property specification

The protocol is intended to achieve reciprocal autentication between A and B. This means that in the same session only A can generate na sending it to B, and only B can replay na to A (due to asymmetric cryptography). This is authentication of B to A. B authenticates A because only A can send back nb. Moreover na and nb have to remain secret. In formula:

(forall B.i: (:> nb_i => z_i = I_0) or (exists A.j: z_i = A_j => x_j = B_i))
and
(forall A.k: (:> na_k => x_k = I_0));

This amount saying:

Authentication of A to B: For every instance i of B exists an instance j of A which correctly communicates with B_i or the intruder discovers nb_i by direct connection with B_i (z_i = I_0).

Authentication of B to A: For every instance k of A the intruder I can get na_k only by direct connection with A_k

Initial knowledge specification

The initial knowledge represent the information the intruder have when the protocol starts. Sinc it is an asymmetric protocol we need the private and pubic key of the Intruder I and is name. This is specified with:

I_0, I_0+, I_0-;

Results

To run ASPASyA we need to put the above information (namely protocol specification, security property, invariant property and initial knowledge) in th corresponding files. Protocol specification goes in a .pr file. Security properties in .pl while invariant in .pj. Initial knowledge is specified in .kb. This example can be found under protocols/needham/ in the distribution directory. It uses true as invariant property. To test the protocol we need to give the following command in a shell:

aspasya needham.pr needham.pl needham.pj needham.kb -V -f -nprinc 2 > result

This tells ASPASyA to gather information and start a verification (-V) giving us a feedback on the status of computation (-f). A context will contain two principal instances (-nprinc 2). The output is then redirected to a file to better analyse the result. Result content (adapted to be shorter):

  ATTACK SET 1
--------------------------------------------------------------

Violated Constraints:
( K !:> na_2)
( K !:> nb_1)
(z_B_1 = I_0)
(z_B_1 <> A_2)
(x_A_2 = B_1)


***************
Context:
A_2: () [Out({A_2,na_2}I_0+).In({na_2,nb_1}A_2-).Out({nb_1}I_0+)]
B_1: () [In({A_2,na_2}B_1-).Out({na_2,nb_1}A_2+).In({nb_1}B_1-)]

Knowledge:
Kid: 48
nb_1
{[na_2,nb_1]}A_2+
na_2
A_2
A_2+
B_1
B_1+
I_0
I_0+
I_0-
.

Model:
u_B_1 -> na_2
z_B_1 -> A_2
x_A_2 -> I_0
y_A_2 -> nb_1



Intruder:
A_2 -> I: {[A_2,na_2]}I_0+
I -> B_1: {[A_2,na_2]}B_1+
B_1 -> I: {[na_2,nb_1]}A_2+
I -> A_2: {[na_2,nb_1]}A_2+
A_2 -> I: {nb_1}I_0+
I -> B_1: {nb_1}B_1+


***************


--------------------------------------------------------------

  ATTACK SET 2
--------------------------------------------------------------

Violated Constraints:
( K !:> nb_2)
( K !:> nb_1)
(z_B_2 = I_0)


***************
Context:
B_2: () [In({B_1,I_0}B_2-).Out({I_0,nb_2}B_1+).In({nb_2}B_2-)]
B_1: () [In({I_0,nb_2}B_1-).Out({nb_2,nb_1}I_0+).In({nb_1}B_1-)]

Knowledge:
Kid: 64
nb_2
nb_1
{[I_0,nb_2]}B_1+
B_2
B_2+
B_1
B_1+
I_0
I_0+
I_0-
.

Model:
u_B_1 -> nb_2
z_B_1 -> I_0
u_B_2 -> I_0
z_B_2 -> B_1



Intruder:
I -> B_2: {[B_1,I_0]}B_2+
B_2 -> I: {[I_0,nb_2]}B_1+
I -> B_1: {[I_0,nb_2]}B_1+
B_1 -> I: {[nb_2,nb_1]}I_0+
I -> B_1: {nb_1}B_1+
I -> B_2: {nb_2}B_2+


***************

The first attack is Lowe's one while the second is a syubtle type flaw. ASPASyA finds more attacks but they are permutations of the second. Note that ASPASyA give us a lot of information:

The violated constraints are the atoms of the security property formula which are false. This is a useful hint to patch flaws in protocols.
The final context togheter with the knowledge.
The model is a collection of variable assignments that falsifies the property
The representation of the intruder is returned.

Type Flaw attack

The second attack found by ASPASyA is an example of type flaw attack. I uses its own name as a nonce sending it to B₂ and then forwards the replay message of B₂ to B₁. B₁ thinks that I is trying to init a run of the protocol with him/her. B₁ decrypt the third message for I sendig back the two nonces. Now I can authenticate himself with B₂ with the indetity of B₁.

Feedback

With -f option ASPASyA give us a summary of the computation. In this case:

--------------------------------------------
Total traces: 59
Total terminal traces: 17
Total nodes: 156
Total starting nodes: 3
Total pruned starting nodes: 0

Total time: 0:0:1
Search time: 0:0:1
Join time: 0:0:0
Verify time: 0:0:1

node/s: 624
trace/s: 236
verification/s: 424
branching factor: 1.65555555556, (149/90)
max branching factor: 3
min branching factor: 1
initial branching factors: 1 1 1
trace length: 6 6 6

Number of attacks: 5
--------------------------------------------

This test is done on a Athlon 2200+ with 512Mb of Ram under Mandrake Linux 9.1