I have written Promela code to verify the Needham-Schroeder protocol using SPIN. After running a random simulation of the code I receive this output:
0: proc - (:root:) creates proc 0 (:init:)
Starting PIni with pid 1
1: proc 0 (:init:) creates proc 1 (PIni)
0 :init ini run PIni(A,I,N
Starting PRes with pid 2
3: proc 0 (:init:) creates proc 2 (PRes)
0 :init ini run PRes(B,Nb)
Starting PI with pid 3
4: proc 0 (:init:) creates proc 3 (PI)
0 :init ini run PI()
1 PIni 62 else
1 PIni 63 1
1 PIni 64 ca!self,nonce,
3 PI 128 ca?,x1,x2,x3
1 PIni 64 values: 1!A,Na
3 PI 128 values: 1?0,Na
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3
3 PI 135 x3 = 0 1 0 0 I
3 PI 101 ca!B,gD,A,B 1 0 0 0
2 PRes 79 ca?eval(self), 1 0 0 0
3 PI 101 values: 1!B,gD 1 0 0 0
2 PRes 79 values: 1?B,gD 1 0 0 0
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3 PRes(2):g2 PRes(2):g3
2 PRes 80 g3==A)&&(self= 1 0 0 0 gD A
2 PRes 80 ResRunningAB = 1 0 0 0 gD A
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3 PRes(2):g2 PRes(2):g3 ResRunning
2 PRes 82 ca!self,g2,non 1 0 0 0 gD A 1
3 PI 128 ca?,x1,x2,x3 1 0 0 0 gD A 1
2 PRes 82 values: 1!B,gD 1 0 0 0 gD A 1
3 PI 128 values: 1?0,gD 1 0 0 0 gD A 1
3 PI 135 x3 = 0 1 0 0 A gD A 1
3 PI 113 ca!( (kNa) -> 1 0 0 0 gD A 1
1 PIni 68 ca?eval(self), 1 0 0 0 gD A 1
3 PI 113 values: 1!A,Na 1 0 0 0 gD A 1
1 PIni 68 values: 1?A,Na 1 0 0 0 gD A 1
Process Statement PI(3):kNa PI(3):x1 PI(3):x2 PI(3):x3 PIni(1):g1 PRes(2):g2 PRes(2):g3 ResRunning
1 PIni 69 else 1 0 0 0 Na gD A 1
1 PIni 69 1 1 0 0 0 Na gD A 1
1 PIni 71 cb!self,g1,par 1 0 0 0 Na gD A 1
3 PI 139 cb?,x1,x2 1 0 0 0 Na gD A 1
1 PIni 71 values: 2!A,Na 1 0 0 0 Na gD A 1
3 PI 139 values: 2?0,Na 1 0 0 0 Na gD A 1
3 PI 145 x2 = 0 1 0 I 0 Na gD A 1
timeout
#processes: 4
34: proc 3 (PI) needhamNew.pml:100 (state 81)
34: proc 2 (PRes) needhamNew.pml:86 (state 10)
34: proc 1 (PIni) needhamNew.pml:73 (state 18)
34: proc 0 (:init:) needhamNew.pml:58 (state 8)
4 processes created
I can see that the processes that are created which are for the Initiator, Responder and Intruder. I'm finding it difficult to see exactly how this proves that the Needham-Schroeder protocol can be broken even though I understand the theory behind it.
Can anyone make sense of this output and maybe direct me to where I should be looking? If you would like to view my Promela code please let me know! Any feedback is appreciated!
