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 的，所以必须先吃透这本书的内容。
现在第一个问题具体部署完成，预计周末完成比较和分析的梳理。现在对第二个问题进行分篇章的整理。
2、Scyther-Semantics and verification of Security Protocol（整理）
内容：
标签：分析,协议,Protocol,Scyther,CIP,verification,IP,EtherNet 来源： https://www.cnblogs.com/xinxianquan/p/10741759.html