SPIN 输出结果答案

【问题标题】：SPIN output resultsSPIN 输出结果
【发布时间】：2015-11-24 21:07:46
【问题描述】：

我编写了 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 代码，请告诉我！ 任何反馈表示赞赏！

【问题讨论】：

我的回答不值得投赞成票吗？还是将“复选标记”作为正确答案更好？

标签： spin promela

【解决方案1】：

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

【讨论】：

非常感谢您的反馈！你建议我怎么做？我不知道我写的代码是否有错误，或者它是否应该给我这个输出。它似乎没有显示出任何入侵者攻击协议的迹象。我可以采取的下一步是什么？
首先，确保在每个 proctype 中标记了有效的结束状态。请参阅关于 a) 结束状态的含义和 b) 如何标记它们的 SPIN 文档（使用以 end 开头的标签:) 本质上，如果被测协议没有错误，则所有 procs 都应重复通过有效的结束状态（或到达 proctype 的末尾，这隐含地是有效的结束状态）。
其次，标记了结束状态，如果发生超时，您需要手动分析导致死锁的原因。这意味着跟踪输出并了解每个流程所采取的每一步。打印输出显示所采取的步骤。
第三，您已经在“模拟”模式下运行了 SPIN。另一种方法是在“验证”模式下运行 SPIN；发生错误时，您会以更小的深度重新运行 SPIN，以找到尽可能少的死锁步数。查看“-I”和“-i”标志（我认为，记忆消失了）；还需要一个编译标志。