scyther/testing/samasc-broken.spdl

35 lines
467 B
Plaintext

/*
Samasc broken
*/
usertype Key;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol samascbroken(I,R)
{
role R
{
fresh nr: Nonce;
var kir: Key;
recv_!1a (I,R, { kir,I }pk(R) );
send_!1b (R,I, {nr,R}pk(I) );
/* Commenting out these two lines yields an attack: */
recv_!2a (I,R, { nr }kir );
send_!2b (R,I, { I,R,nr }kir );
recv_!3 (I,R, { I,R }kir );
claim_4 (R, Secret, kir );
}
}
untrusted e;
compromised sk(e);