Needham-Schroeder協議的形式化描述語言

一、對TLS1.3協議形式化描述過程

第一步：   Needham-Schroeder 過程的分析

 常量和變量的定義：

/*

* Needham-Schroeder過程的形式化描述  

*/

// THE  protocol description 

protocol TLS-1.3(a, b ){

 //  首先定義協議 指定使用 TLS1.3協議的名字是 TLS-1.3

   roel a{

    }

   role b{

  }

}

要點補充：

   在使用  Scyther  的SPDL語言進行對眼研究的協議進行形式化描述的時候，使用的語法規則必須聽從，否則Scyther軟件就會報錯，後續壓根不會有輸出圖，其次協議必須按照本來要驗證的協議通訊的過程來抽象描述，若是中間環節少了驗證，那麼Scyther 中的路徑就會沒法生成，勢必會形成不能驗證協議的安全性。

下面是對協議Needham-Schroeder 的形式化分析的代碼部分和執行結構。結果顯示在角色I 中不存在攻擊可是在 角色R中存在至少四個攻擊

 

在驗證的結果說明就是 comment行，若是顯示的是  " NO attack within bounds 」意思是說在設置的狀態界限內是不存在攻擊的，可是狀態外不肯定是否存在攻擊。

若是鏈接箭頭是紅色的表示，發送信息和接受信息不匹配，黃色的鏈接箭頭表示-----，綠色的箭頭表示信息正常的接受和發送，