Scyther cannot find attack #27
Description
The following protocol msc.pdf is insecure. Its corresponding Scyther model is shown below:
protocol DY2(I, R) {
role I {
fresh ni: Nonce;
send_1(I, R, {I, {ni}pk(R)}pk(R) );
recv_2(R, I, {R, {ni}pk(I)}pk(I) );
claim_3(I, Secret, ni);
}
role R {
var ni: Nonce;
recv_1(I, R, {I, {ni}pk(R)}pk(R) );
send_2(R, I, {R, {ni}pk(I)}pk(I) );
}
}
The attack is attack.pdf. It is a type flaw attack, but no matter how I set the options in Scyther, it says the protocol is "Ok".