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);
}
}