1、對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 ”意思是說在設置的狀態界限內是不存在攻擊的，但是狀態外不確定是否存在攻擊。
如果連接箭頭是紅色的表示，發送信息和接受信息不匹配，黃色的連接箭頭表示-----，綠色的箭頭表示信息正常的接受和發送，