Scyther-Semantics and verification of Security Protocol

 1 、本书前一节主要是介做者本身的平生经历（读完感受做者是个神童），目标明确做者13岁代码已经写的很溜了。本身也开了网络公司，可是后面又专一于本身的计算机基础理论，修了哲学的博士学位（不得不说不少专业的交叉真的能够创造新的起点），可是任何领域的开辟都是来自本身任劳任怨的决心和坚韧不拔的毅力。

   原本以前一直是在看渗透测试的方面资料，可是后面加上实习的事，论文View“”被“”选择成工业网络协议的形式化分析，没有人指导该怎么去作，迷茫应该往哪一个方向上分析，先是对EtherNet/IP 协议ODVA发布的规范文档的阅读，（刚开始看的的时候感受看不到头，没有本身指望的相关资料或者越看越复杂）就好像一棵藤，本身独自摸索着向前，每个枝节会有新的问题或者概念蹦出，而后在返回去找相关的资料。（这种状况像是叠罗汉），可是这中间我感受本身走了不少弯路（磕磕碰碰），由于急切的想要找到指望的，切中要点的idea ，这样我就不少时候半途而废（太摧残），就像漫画上一我的挖井，挖到通常看不到但愿就放弃另寻锚点挖。有个以前寻求帮助的博士说“你四处询问的所须要的东西每每就在你眼前”因此真的要静下心来，坚持下去。就是以为本身在计算机方面的能力真的有待提升，因此尴尬的近况就是真的惧怕本身作不出来，如今还有论文方面还存在两个困难。

        一是EtherNet/IP协议中应用层CIP协议中使用的安全传输机制TLS协议和DTLS协议自身的问题（TLS1.3版本已经更新，可是ODVA中的支持的芯片将来3-6年才能更新支持），若是对EtherNet/IP协议形式化分析，拿现有的TLS1.2做为分析，仍是使用TLS1.3,1.3的版本在协议内容上存在较大的改变。可是若是使用TLS1.3作形式化分析，自己CIP中的全部密码套件不支持，在回溯到EtherNet/IP 协议的自身安全的时候就会没法进行下去。考虑到此因此对CIP协议分析的采用目前使用的TLS1.2版本，分析完以后对其中的漏洞和安全问题以及攻击路径作整理回溯到CIP安全，在回溯到EtherNet/IP协议的安全，这里加上比较TLS1.2和TLS1.3存在的差别，（后面扩展视时间而定）。

      二是Scyther 形式化分析工具的手册和语义分析的资料书目前仍是没有看懂，Scyther user manual 已经看完，可是因为里面的内容是基于Scyther-Semantics and verification of Security Protocol 的，因此必须先吃透这本书的内容。

     如今第一个问题具体部署完成，预计周末完成比较和分析的梳理。如今对第二个问题进行分篇章的整理。

二、Scyther-Semantics and verification of Security Protocol（整理）

     内容：

  第一节：Dolev-Yao模型 （假设基础， 要分析的密码算法是完美的，消息是抽象的术语，网络彻底可由入侵者控制）

   安全模型的术语定义： 首先安全协议区分了不少行为，每一个这样的协议行为成为角色，

   协议规范描述了协议中的每一个角色的行为，将协议规范视为语义的参数，定义抽象的语法制定安全协议，将安全协议中的角色指定为一系列的事件，挑战响应机制（一般成为Nonce 随机数）或者会话秘钥，在整个协议中有重要的做用，按照协议提出一个抽象的语法和静态要求，代理模型：代理执行协议的角色，能够并行执行屡次，是封闭的假设（诚实的代理不会对外泄露分类消息），代理模型描述了如何解释角色的运行，代理按照顺序执行角色的描述，等待读取时间，

通讯模型：通讯模型描述了消息之间的关系代理商的交换，咱们选择异步模型通信。使用缓冲区（暂）

威胁模型： 参见 Dolev-Yao

密码 原语： 密码原语是理想化的数学结构，例如加密，在对加密原语的处理中，使用了所谓黑盒测试，只是知道密码算法的相关属性，只考虑非对称和对称算法，而且假设要分析的协议使完美的。

 本章使用NS协议（Needham-Scroeder）,使用消息序列图（MSC）来讲明安全协议的攻击：   首先 发起者 i  拥有公钥pk(r)和私钥sk(i) ,同时接受者也一样拥有公钥pk(i)和私钥sk(r) ,发起者向接受者发送个个随机变量 ni 同时加上本身的身份 i ，使用 公钥 pk(r)进行加密，接受者 r 接收到消息以后向发送者发送一个随机变量 nr 加上以前的随机变量 ni 使用本身的公钥 pk(i)进行加密。接受者收到消息以后，解密出nr 发送给 接受者，并使用本身的公钥进pk(r)行加密,这样发送者和接受者都声称本身有安全认证的属性 ni-synch 的拥有者。

   

 角色术语： 定义基本的角色术语

    Var : 表示用于存储接受消息的变量     、    Const  :表示角色的每一个实例化新生成的常量，被认为是局部常量。  、  Role ：定义角色   、   Func :表示函数的名字

   咱们将角色术语集定义为基本术语套，使用构造函数进行扩展以进行配对和加密，而且假设配对是右关联的。

  

  当咱们想要使用个函数的 f 的时候，其定义域是 X，能够这样标记  ：------->  {f(x)| x ∈X}

这里咱们定义一个术语的逆 使用函数：

         咱们规定 — ^-1是本身的逆， （rt ^-1）^-1=rt  

   在整片论文中咱们假设公钥pk 和私钥映射到非对称秘钥的元素函数中，咱们使用pk 表示i代理的公钥，使用sk表示代理的私钥

    （补充数学量词   ∀R∈Role ：pk(R)^-1=sk(R)^sk(R)-1=pk(R) 表示 对任意的R 属于 Role均成立右面的等式。）

例子： 咱们创建角色R的私钥模型 sk(R)和对应公钥的逆 pk(R),使用公钥模型加密消息 m 表示模型为  ： {/m/}pk(R) ,  对消息进行签名，并非直接使用秘钥进行加密，而是被称为：消息摘要”加密，

为了使私钥正确的签名消息 m 模型，咱们须要一个函数  h , 签署消息 m 以后的的术语是  （m, {/h(m)/}sk(R)）

定义：描述角色，（协议是由角色组成的，而角色又是由角色事件组成的）。

    咱们定义一组事件集，RoleEvent 使用两个新的组，标签 Labe 和安全声称 Claims

  

      上面的事件集解释以下： 事件 表示发送的消息 rt  绑定到代理 R上 ，打算用于绑定代理 R' ,一样的 指明消息  rt 被代理 R ’ 绑定，显然是由代理 R发送过来的，事假声明表达，执行此事件时 R 指望安全目标  c 与可选参数  rt 保持一致。声称事件仅仅表示涉及本地代理R 并非其余任何人的指望的代理。标签标记事件来消除协议规范中相同事件的相似避免发生歧义，第二层含义是表达发送事件和接受事件的之间的关系，

      定义次运算符：  定义子术语，其中包括用于加密的秘钥，注意术语形如 f(rt)的术语没有子句，由于被认为是非组合型术语。除了发送和接受术语以外，角色规范还定义了执行角色的初始知识，也是一组术语。

    定义以下：

   定义 角色知识： 咱们定义角色知识，将角色知识集RoleKnow定义为不包含变量做为子项的全部角色术语的集合。

       做为结果，咱们有这样的表达式 由于角色事件彻底描述角色的行为。    没有必要声明局部常量和变量，协议的执行不须要角色知识，这里引入角色知识有两个缘由，首先他容许静态角色的一致性测试，在给定初始知识集的状况下查看角色是否能够执行，第二，他将使咱们可以系统的推导出文章末尾的初始入侵者。

   定义角色规范： 角色规范包含一系列的事件，一些事初步知识，所以咱们定义了角色规范集合 像  ： RoleSpec=RoleKnow×RoleEvent*

 咱们写成[ε1,ε2]指定 两个事件列表，ε1和ε2 ，咱们写 [ε1,ε2]^.[ε3] 去指定两个列表的级联，  常常在书写单个事假的时候咱们会省略括号直接写成,ε1^.ε2 表示 [ε1,ε2]。

  咱们书写  A B指定一个局部函数，他将A的元素映射到元素B上，  

 定义2.8  一个协议规范角色行为经过设置协议的部分功能，如此咱们有这样的表达式  ： Protocol=RoleRoleSpec 

    咱们使用 MR^P(R)做为协议规范 P中角色 R的初始知识简写。在不少状况下咱们省略 参数 P 在协议上下文很清楚的状况之下。符号  MR是M的缩写，以后咱们将用做表示知识，R 用做表示角色。

      角色事件在协议中的描述必须是惟一的，能够经过标签事件进行强制执行，者容许咱们定义一个角色函数:   RoleEvent ------> Role ,鉴于角色事件，角色函数也是事件中的一个。咱们将协议做为一个隐式的参数，当协议上下文清楚的时候。

定义 2.9  下面的角色描述模拟了NeedHam-Schroeder 协议的发起者角色，没有任何的安全要求。

 

 2.2.2 事件顺序

      事件的每一个角色对应于事件列表，换句话说， 一个结构顺序加到属于角色R的协议事件中，这个总数的排序指定 ，如此 对于任何角色R∈Role 和 ε1，ε2 ∈RoleEvent ,这样 role(ε1)=R 和role(ε2)=R 我么有这样的表达式 ： 我么认为有个抽象的安全协议 P做为通讯序列结合，每个顺序组件由特定的角色承担。通讯由装饰事件的标签管理，标签直接定义沟通（通讯）关系：

 定义2.10  通讯关联

    对于全部的 ∈ Label  以及 m1 ,m2 ∈ Role ×Role ×RoleTerm ,通讯关系定义为： 这个关系规范了发送事假和接受事件如何对应。

 Example 2.11  事假顺序和通讯关系：  对于示例协议 NS  角色排序 和关于角色 i 和 r ,分别表示以下：

  

    通讯关系表示以下：

  

2.2.3 静态要求

      在上一节中咱们已经解释了协议规范的抽象的语法，适当的协议规范还应当知足不少无缺性的要求，并非任何有发送、接受、和声明的事件被认为是安全的协议，列如，咱们要求代理可以构建出他发送的条款，而且他不能检查条款的内容和加密的秘钥。

    良好的角色，  对于每个角色，咱们要求有本身肯定的标准，这些标注的范围是至关明确的，列如，协议角色定义中的每一个时间都是具备执行它的相同的角色（事件参与者和执行者），对于消息，咱们要求发送者可以实际构造这些消息，对于变量应该首先出如今接受事件中，在实例化以前能够出如今发送时间中。对于接受事件，从上的协议的列子中能够看出， 在咱们描述Needham-Schroeder protocol

    咱们定义一个 预测 WF 表达一个角色定能够的一致性要求，  使用辅助定义RD （可读性）和一个推理知识的关系，

             角色能够撰写和分解术语对，若是代理指导加密秘钥，则能够加密术语，若是代理知道响应的解密秘钥，则能够解密加密的术语。

定义 2.12 推理运算法

     使用M做为 一个角色知识集，  知识推理关系 概括以下： 全部的角色术语 rt ,rt1 ,rt2  ,k :

       

Example 2.13 推理和加密  从术语集 组成 术语 term{/m/}k ，可是不是  k ^-1 没法推断 是m 或者 k  i e

         给定 和 k ^-1 咱们可以推断出 m , 若是 k 是非对称秘钥 （如此 k k ^-1 ），而且给定{/m/}k 和k ^-1   没法推断 K

   

Example 2,1,4 推断和子句 

     给定术语  m1 和m2 以及 通常状况之下，m2 不是 ，一个反例给出 m1=(rt1, rt2) 和 m2=(rt2 ,rt 1) 当 rt 1不等于rt2 ，反之则否则。好比，由于给定术语 k 和 m 以及 咱们有 k 可是

Example 2.1.5 推断和函数