ASPASyA: WMF

Description of the protocol

As a case study we have considered the Wide Mouthed Frog Protocol and tested it for authentication. The protocol has been designed to achieve authentication of a principal A to B by means of a trusted server S and the exchange of a session key. The informal specification is:

(1) A --> S: A,{ta, B, kab}_ksa (2) S --> B: {ts, A, kab}_ksb
A generates a timestamp ta and a session key kab.A then sends a message to a server S with its own identity, the identity of the responder and the two secrets, encrypted with the symmetric key shared with S. Once received this message S checks the freshness of the timestamp and sends B a new timestamp with the session key of A, encrypted with the symmetric key shared with B.

cIP-calculus specification

The cIP specification need some attention:

A: (x, s) [out((A, {(na,(x,kab))}s))];
S: (u, a, v, b) [in((u,{(?t,(v,?r))}a)).out({(ns,(u,r))}b)];
B: (s) [in({(?t,(?z,?r))}s)];

A needs two open variables: x to connect with B and s to store the secret shared with S. S needs the name of the initiator and its shared key (u,a). The same for the responder (v,b). B needs only a variable for the shared key because gets the identity of the initiator from the message sent by S. Messages don't have timestamps, so whenever we have to use them, they are replaced with nonces. Note that a variable is identified with its name and with the name of the principal it belongs. So there is no problem using the same names in different principals.

Invariant specification

ASPASyA begins 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. In this case we want principals to be connected properly.

(exists A.m: true) and
(exists B.n: true) and
(exists S.o: true) and
forall S.l:
	(exists A.i: (u_l = A_i => a_l = s_i) and (v_l = A_i => b_l = s_i))  and
	(exists B.j: (u_l = B_j => a_l = s_j) and (v_l = B_j => b_l = s_j));

This formula specifies that we are interested in checking those context with at least an instance of every principal. Moreover every server S should be connected in such a way that if u=A then s=a is the corresponding shared key bettwen S and A. The same for the responder connection. This formula may seem correct but it fails to capture an implicit assumption of the WMF protocol, namely that keys shared with S by different principal must be different. Running ASPASyA with such condition produce an obvious attack (see next section for security property) where every cryptogram is encrypted with the same key. So the correct formula is:

(exists A.m: true) and
(exists B.n: true) and
(exists S.o: true) and
forall S.l: (a_l <> b_l) and
	(exists A.i: (u_l = A_i => a_l = s_i) and (v_l = A_i => b_l = s_i))  and
	(exists B.j: (u_l = B_j => a_l = s_j) and (v_l = B_j => b_l = s_j));

Property specification

The protocol is intended to achieve authentication of A to B and exchange of a session key. Secrecy of the session key is simply checked by ensuring that the intruder is not able to derive it. More interesting is authentication. B has to be sure that A sent him/her the session key in that session.

(forall B.j: 
        exists S.l: 
               exists A.i: (
                         (v_l = B_j and u_l = A_i and x_i = B_j) => (t_l = na_i and t_j = ns_l and r_j = kab_i)
                           )
);

For every instance of B there exist an instance of S and an instance of A such that if A wants to communicate with B (x_i = B_j) and S receive a message with correct initiator and responder (u_l = A_i and v_l = B_j) then S must receive a fresh timestamp (t_l = na_i means that A_i has generated na_i in the current session, so it is fresh) and B must receive the timestamp generated by S in that session with the key generated by the correct initiator (t_j = ns_l and r_j = kab_i).

Initial knowledge specification

Tuning the initial knowledge allow us to search for replay attacks (those attacks where old messages of previous sessions are used again). Observing the protocol definition we see that B has no way to check the freshness of the server timestamp. To let the intruder know a previous run of the protocol we have to insert some cryptograms representing messages exchanged by A, B and S in the past:

I_0,  {(naold_3,(B_1,kold_3))}s_A_3, {(nsold_2,(A_3,kold_3))}s_B_1;

Old timestamps are represented with 'old' nonces.

Results

To run ASPASyA we need to put the above information (namely protocol specification, security property, invariant property and initial knowledge) in the 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/widefrog/ in the distribution directory. It uses the second invariant property specified above and the initial knowledge with old cryptograms. To test the protocol we need to give the following command in a shell:

aspasya widefrog.pr widefrog.pl widefrog.pj widefrog.kb -V -f -nprinc 3 > 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 three principal instances (-nprinc 3). The output is then redirected to a file to better analyse the result. Result content (adapted to be shorter):

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

Violated Constraints:
(v_S_2 <> B_1)
(u_S_2 <> A_3)
(x_A_3 <> B_1)
(t_B_1 = ns_2)
(r_B_1 = kab_3)


***************
Context:
A_3: () [Out(A_3,{na_3,B_1,kab_3}k2,3_0)]
S_2: () [In(A_3,{na_3,B_1,kab_3}k2,3_0).Out({ns_2,A_3,kab_3}k2,1_0)]
B_1: () [In({nsold_2,A_3,kold_3}k2,1_0)]

Knowledge:
Kid: 54
{[ns_2,[A_3,kab_3]]}k2,1_0
{[na_3,[B_1,kab_3]]}k2,3_0
A_3
A_3+
S_2
S_2+
B_1
B_1+
{[nsold_2,[A_3,kold_3]]}k2,1_0
{(naold_3,(B_1,kold_3))}k2,3_0
I_0
.

Model:
a_S_2 -> k2,3_0
s_A_3 -> k2,3_0
b_S_2 -> k2,1_0
s_B_1 -> k2,1_0
t_S_2 -> na_3
r_S_2 -> kab_3
t_B_1 -> nsold_2
z_B_1 -> A_3
r_B_1 -> kold_3
v_S_2 -> B_1
b_S_2 -> s_B_1
a_S_2 -> s_A_3
u_S_2 -> A_3
x_A_3 -> B_1

Intruder:
A_3 -> I: [A_3,{[na_3,[B_1,kab_3]]}k2,3_0]
I -> S_2: [A_3,{[na_3,[B_1,kab_3]]}k2,3_0]
S_2 -> I: {[ns_2,[A_3,kab_3]]}k2,1_0
I -> B_1: {[nsold_2,[A_3,kold_3]]}k2,1_0


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

ASPASyA finds more attacks but they are permutations. 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.

Attacks

This attack is found because B receives a message with a timestamp not generated by the server in this session and has no way to check its freshness.

If we run ASPASyA with the 'incorrect' invariant property we can find the following attack:

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

Violated Constraints:
(v_S_2 <> B_1)
(u_S_2 <> A_3)
(x_A_3 <> B_1)
(t_B_1 = ns_2)


***************
Context:
A_3: () [Out(A_3,{na_3,B_1,kab_3}k1,2,2,3,1_0)]
S_2: () [In(A_3,{na_3,B_1,kab_3}k1,2,2,3,1_0).Out({ns_2,A_3,kab_3}k1,2,2,3,1_0)]
B_1: () [In({na_3,B_1,kab_3}k1,2,2,3,1_0)]

Knowledge:
Kid: 81
{[ns_2,[A_3,kab_3]]}k1,2,2,3,1_0
{[na_3,[B_1,kab_3]]}k1,2,2,3,1_0
A_3
A_3+
S_2
S_2+
B_1
B_1+
{[naold_3,[B_1,kold_3]]}k1,2,2,3,1_0
{[nsold_2,[A_3,kold_3]]}k1,2,2,3,1_0
I_0
.

Model:
v_S_2 \> A_3
r_B_1 -> kab_3
s_B_1 -> k1,2,2,3,1_0
t_B_1 -> na_3
z_B_1 -> B_1
s_B_1 -> s_B_1
a_S_2 -> k1,2,2,3,1_0
a_S_2 -> s_B_1
a_S_2 -> s_A_3
b_S_2 -> k1,2,2,3,1_0
s_A_3 -> k1,2,2,3,1_0
t_S_2 -> na_3
r_S_2 -> kab_3
v_S_2 -> B_1
b_S_2 -> s_B_1
s_A_3 -> s_B_1
b_S_2 -> s_A_3
u_S_2 -> A_3
x_A_3 -> B_1



Intruder:
A_3 -> I: [A_3,{[na_3,[B_1,kab_3]]}k1,2,2,3,1_0]
I -> S_2: [A_3,{[na_3,[B_1,kab_3]]}k1,2,2,3,1_0]
S_2 -> I: {[ns_2,[A_3,kab_3]]}k1,2,2,3,1_0
I -> B_1: {[na_3,[B_1,kab_3]]}k1,2,2,3,1_0


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

This attack is possible because all principals share the same symmetric key and the intruder can use messages sent by A to S to force B accepting a timed-out message.

Feedback

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

--------------------------------------------
Total traces: 95
Total terminal traces: 86
Total nodes: 246
Total starting nodes: 10
Total pruned starting nodes: 9

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

node/s: 4099
trace/s: 1583
verification/s: 358
branching factor: 1.72222222222, (217/126)
max branching factor: 6
min branching factor: 1
initial branching factors: 0 0 0 0 14 0 0 0 0 0
trace length: 3 4 3 5 4 3 6 5 4 3

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

We can see that only one initial state satisfies the invariant property.

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