SPIN输出结果

Question

我已经编写了 Promela 代码来使用 SPIN 验证 Needham-Schroeder 协议。运行随机模拟代码后，我收到此输出：

  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

我可以看到为发起者、响应者和入侵者创建的进程。我发现很难确切地看出这如何证明 Needham-Schroeder 协议可以被破坏，即使我理解它背后的理论。

任何人都可以理解这个输出并指导我到我应该看的地方吗？ 如果您想查看我的 Promela 代码，请告诉我！ 感谢任何反馈！

Answer 1

接近输出的末尾，您会看到 timeout - 这意味着无法取得进一步的进展，这通常表示某种死锁。在进程列表（最后）中，您会看到行号，其中 none 被标记为有效的 end 状态。因此，要么你有一个真正的死锁，要么你的模型是错误的，因为它无法识别其有效的结束状态。

SPIN输出结果

SPIN output results

spin

promela