Scyther-Semantics and verification of Security Protocol（整理）
1 、本书前一节主要是介作者自己的生平经历（读完感觉作者是个神童），目标明确作者13岁代码已经写的很溜了。自己也开了网络公司，但是后面又专注于自己的计算机基础理论，修了哲学的博士学位（不得不说很多专业的交叉真的可以创造新的起点），但是任何领域的开辟都是来自自己不辞辛苦的决心和坚韧不拔的毅力。
本来之前一直是在看渗透测试的方面资料，但是后面加上实习的事，论文View“”被“”选择成工业网络协议的形式化分析，没有人指导该怎么去做，迷茫应该往哪个方向上分析，先是对EtherNet/IP 协议ODVA发布的规范文档的阅读，（刚开始看的的时候感觉看不到头，没有自己期望的相关资料或者越看越复杂）就好像一棵藤，自己独自摸索着向前，每一个枝节会有新的问题或者概念蹦出，然后在返回去找相关的资料。（这种情况像是叠罗汉），但是这中间我感觉自己走了很多弯路（磕磕碰碰），因为急切的想要找到期望的，切中要点的idea ，这样我就很多时候半途而废（太摧残），就像漫画上一个人挖井，挖到一般看不到希望就放弃另寻锚点挖。有个之前寻求帮助的博士说“你四处询问的所需要的东西往往就在你眼前”所以真的要静下心来，坚持下去。就是觉得自己在计算机方面的能力真的有待提高，所以尴尬的近况就是真的害怕自己做不出来，现在还有论文方面还存在两个困难。
SRE实战 互联网时代守护先锋，助力企业售后服务体系运筹帷幄！一键直达领取阿里云限量特价优惠。一是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（整理）
内容：
第一节：Dolev-Yao模型 （假设基础， 要分析的密码算法是完美的，消息是抽象的术语，网络完全可由入侵者控制）
安全模型的术语定义： 首先安全协议区分了很多行为，每个这样的协议行为成为角色，
协议规范描述了协议中的每个角色的行为，将协议规范视为语义的参数，定义抽象的语法制定安全协议，将安全协议中的角色指定为一系列的事件，挑战响应机制（通常成为Nonce 随机数）或者会话秘钥，在整个协议中有重要的作用，按照协议提出一个抽象的语法和静态要求，代理模型：代理执行协议的角色，可以并行执行多次，是封闭的假设（诚实的代理不会对外泄露分类消息），代理模型描述了如何解释角色的运行，代理按照顺序执行角色的描述，等待读取时间，
通信模型：通信模型描述了消息之间的关系代理商的交换，我们选择异步模型通讯。使用缓冲区（暂）
威胁模型： 参见 Dolev-Yao
密码 原语： 密码原语是理想化的数学结构，例如加密，在对加密原语的处理中，使用了所谓黑盒测试，只是知道密码算法的相关属性，只考虑非对称和对称算法，并且假设要分析的协议使完美的。
