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

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

- 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.

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.

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

Authentication of B to A: For every instance *k* of A the intruder I can get *na _{k}* only by direct connection
with A

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-;

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 > resultThis 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.

-------------------------------------------- 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