《形式化工具Scyther优化与实例分析》--------论文摘抄整理

Scyther 工具在输出方面操做便捷，攻击输出方面方面使用图形的方式便于理解。这个详细的不在此说明了

         重要的敌手攻击能力的说明：  -------  支持   Delov-Yao模型，能够本身定义安全模型，而且支持强安全模型。这就是说能够为敌手定义更强的安全攻击能力。-------决定了敌手能力在彻底掌握通讯网络的基础上，具有腐化长期私钥和临时秘钥等能力，

        本篇论文中做者的主要共贡献是 将 scyther工具的设置界面的汉化  ，添加了  工具分析协议的运行时间 两个部分。

  

 

   做者对TLS协议的验证是使用了 软件中自身携带的协议 对其 佐证本身的 改进，   TLS协议在客户端和服务器之间创建通讯时，首先要对协议的版本、密码算法、认证方式、以及公钥加密技术进行协商，以后进入握手协议阶段。这部分我在个人论文中说的会很详细，在Scyther 工具中使用  SPDL语言 描述协议。对协议的描述是基于角色的，利用 claim时间能够对角色的认证性、变量性的机密性等进行描述。

      做者的实验结果是  在  Scyther工具 使用  Delov-Yao模型下对 TLS协议分析，验证目标属性是TLS 握手协议中秘钥协商的机密性结果是安全   。（对做者的结果验证结果以下）

       

 

      敌手在经过长期私钥泄露询问得知主体长期私钥，而在秘钥传输过程当中惟一保证传输机密性的就是主体的长期私钥，在这种强安全模型面前，TLS握手协议传输的秘钥是不安全的。

      如今我验证做者说的实验结果以下：

         如上图所示  安全做者说的   参数设置形式 。（强安全模式）   执行结果以下：  验证结果和该论文做者说的是一致的，可是 好几处验证结果做者忽略没有写  ，在后面个人论文中会加入