search

cascremers / scyther

The Scyther Tool for the symbolic analysis of security protocols
https://cispa.saarland/group/cremers/scyther/index.html
96 stars 38 forks source link

Scyther cannot find attack #27

Open gilcu3 opened 3 years ago

gilcu3 commented 3 years ago

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".

cascremers commented 3 years ago

Thanks for the report, we'll look into it.

cascremers commented 3 years ago

P.s. could you please add information on the version of Scyther you used (detailed version number, github commit if possible, and details of the operating system you are using).

gilcu3 commented 3 years ago

OS: Archlinux Scyther : v1.1.3 (installed from http://www.cs.ox.ac.uk/people/cas.cremers/downloads/scyther/scyther-linux-v1.1.3.tgz)

GOKULKUMAR-2004 commented 2 months ago

please tell me the is there any syntax error in sycther tool ????