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 ”意思是说在设置的状态界限内是不存在攻击的，但是状态外不确定是否存在攻击。

如果连接箭头是红色的表示，发送信息和接受信息不匹配，黄色的连接箭头表示-----，绿色的箭头表示信息正常的接受和发送，