scyther/testing/simplest.spdl

17 lines
167 B
Plaintext

secret k: Nonce;
protocol simplest(I)
{
role I
{
var x: Nonce;
fresh n: Nonce;
recv_!1(I,I, x);
send_!2(I,I, n, {n, x}k );
claim_3(I, Secret, n);
}
}