首页 > TAG信息列表 > Scyther
协议形式化分析资料整理
1、接近尾声把协议形式化分析的资料整理一遍 形式化分析工具 Scyther 软件资料以及 tool manual 在官网上可查 https://people.cispa.io/cas.cremers/scyther/\ scyther 形式化分析的协议 发布在作者 GitHub https://github.com/cascremers/scyther 另协议形式化安全分析 Scyther 并非所有协议可以照抄就搬
1、Scyther 形式化分析工具可以对协议进行形式化描述，验证协议的机密性和可认证性是否存在安全威胁。在攻击时支持会话轮数无限次执行，同时支持在强安全模型和Delov-Yao模型。在对要形式化分析的协议算法方面并不支持含有 “”XOR“” 运算代数性质和 “”DH“” 代数运算性质以及Scyther 形式化分析工具资料整理（三）
1、作者Cas Cremers在做TLS1.3的时候我么发现并没有使用Scyther 形式化丰分析工具对其进行分析，而是使用了 The Tamarin 。作者建立了TLS.13的模型。 那么我的目标是 使用Scyther工具对TLS1.2协议的握手协议和TLS1.3版本的握手协议分别进行形式化的分析。通过对比TLS1.3较之前的TLS1Scyther-Semantics and verification of Security Protocol（整理）
1 、本书前一节主要是介作者自己的生平经历（读完感觉作者是个神童），目标明确作者13岁代码已经写的很溜了。自己也开了网络公司，但是后面又专注于自己的计算机基础理论，修了哲学的博士学位（不得不说很多专业的交叉真的可以创造新的起点），但是任何领域的开辟都是来自自己不辞辛苦的决心和坚韧