Scyther工具形式化分析Woo-Lam协议

Scyther

Scyther形式化分析工具可以对协议进行形式化描述，验证协议的机密性和可认证性是否存在安全威胁。在攻击时支持会话轮数无限次执行，同时支持在强安全模型和Delov-Yao模型。在对要形式化分析的协议算法方面并不支持含有 “”XOR“” 运算代数性质和 “”DH“” 代数运算性质以及含有双线性对代数性质的协议。类似的协议形式化分析工具还有SPIN，CPN Tools，Tamarin等。

一. Scyther

Scyther下载地址

Scyther-Compromise使用的状态空间显示和搜索算法相似，Scyther-Compromise在Scyther的基础上添加了强安全模的选项，从而增加了搜索的时间，而Tamarin是在Scyther基础上涉及的，使用Scyther的逆向算法。另外要说的是Scyther-Compromise和Tamarin工具不仅支持Dolev-Yao模型，还支持eCK等强安全模型。

二. Woo-Lam协议

上图所示为Woo-Lam协议消息流图。

三. 形式化建模分析

protocol Woo-Lam(A,B,S)
{
role A{
var Nb:Nonce;
send_1(A,B,A);
recv_2(B,A,Nb);
send_3(A,B,{Nb}k(A,S));
claim(A,Secret,Nb);
claim(A,Alive);
claim(A,Weakagree);
claim(A,Niagree);
claim(A,Nisynch);
}role B{
fresh Nb:Nonce;
recv_1(A,B,A);
send_2(B,A,Nb);
recv_3(A,B,{Nb}k(A,S));
send_4(B,S,{B,{Nb}k(A,S)}k(B,S));
recv_5(S,B,{A,Nb}k(B,S));
claim(B,Secret,Nb);
claim(B,Alive);
claim(B,Weakagree);
claim(B,Niagree);
claim(B,Nisynch);
}role S{
var Nb:Nonce;
recv_4(B,S,{B,{Nb}k(A,S)}k(B,S));
send_5(S,B,{A,Nb}k(B,S));
claim(S,Secret,Nb);
claim(S,Alive);
claim(S,Weakagree);
claim(S,Niagree);
claim(S,Nisynch);
}
}

Scyther工具形式化分析Woo-Lam协议相关推荐

Scyther tools 协议形式化分析帮助文档翻译
1.Scyther软件作者网站的整理 Scyther工具的网站主页:https://people.cispa.io/cas.cremers/index.html 首先对Scyther软件的资料进行整 ...
TLS1.3TLS1.2形式化分析
本博客是对下面博客连接上的原文进行梳理+自己在其他方面资料做个整理 https://blog.csdn.net/andylau00j/article/details/79269499 https:// ...
使用Wireshark分析工控协议
在工控系统中通信协议存在众多标准,也存在众多私有协议,如果你有过使用组态软件的经历,你便会发现,在第一步连接设备时除连接设备的方式有以太网/串行等方式外,各家基本上都存在自己的私有通信协议. 上图为, ...
【计算机网络】利用WireShark分析TCP/UDP协议
前期准备: IntelliJ IDEA 2021.1.3 (Ultimate Edition) Build #IU-211.7628.21, built on June 30, 2021 JDK 1. ...
Wireshark抓包分析之ICMP协议包
Wireshark抓包分析之ICMP协议包一. Wireshark简介:(前身为Ethereal,2006年改名为wireshark) Wireshark 是一个网络封包分析软件.网络封包分析软件的 ...
实验十四：Wireshark数据抓包分析之ARP协议
实验十四:Wireshark数据抓包分析之ARP协议目录一.实验目的及要求二.实验原理 1.什么是ARP 2.ARP工作流程 3.ARP缓存表三.实验环境四.实验步骤及内容实验步骤一 1. ...
dns隧道攻击原理及常用工具流量分析
今天看到一个关于Lyceum组织的文章,这个组织擅长使用dns隧道攻击,这种攻击方式还是头一次听说,于是搜集了一些文章来看看. 原文https://www.cnblogs.com/HighnessDr ...
协议分析---TCP/IP协议和邮件协议
协议分析-TCP/IP协议和邮件协议一.TCP/IP 1.TCP/IP参考模型概述 1.1 常见不同层使用的协议应用层:Telnet.FTP.TFTP.SNMP.HTTP.SMTP.NFS.D ...
利用java虚拟机的工具jmap分析java内存情况
2019独角兽企业重金招聘Python工程师标准>>> 有时候碰到性能问题,比如一个java application出现out of memory,出现内存泄漏的情况,再去修改bug ...

Scyther工具形式化分析Woo-Lam协议

Scyther

一. Scyther

二. Woo-Lam协议

三. 形式化建模分析

Scyther工具形式化分析Woo-Lam协议相关推荐

最新文章

热门文章