Formal analysis of Woo Lam protocol with scyther tool

Scyther Tools for formal analysis Woo-Lam agreement

Scyther

Scyther Formal analysis tools can formally describe the protocol , Verify whether there is a security threat to the confidentiality and authentication of the protocol . During the attack, it supports unlimited number of sessions , It supports both strong security model and Delov-Yao Model . In terms of protocol algorithms to be formally analyzed, it does not support the inclusion of “”XOR“” Properties of operational algebra and “”DH“” The properties of algebraic operations and the protocols of algebraic properties containing bilinear pairs . Similar formal protocol analysis tools include SPIN,CPN Tools,Tamarin etc. .

One . Scyther

Scyther Download address

Scyther-Compromise The state space display used is similar to the search algorithm ,Scyther-Compromise stay Scyther Add the option of strong security module on the basis of , This increases the search time , and Tamarin Is in Scyther Based on , Use Scyther Inverse algorithm of . The other thing is Scyther-Compromise and Tamarin Tools not only support Dolev-Yao Model , And support eCK Equal strength security model .

Two . Woo-Lam agreement

 The figure above shows Woo-Lam Protocol message flow diagram .

3、 ... and . Formal modeling analysis

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

You can try it if you like
This is the official account of Xiaobian. , Please move your lovely little hand , Pay attention to it.