deffun h/1;

deffun enc/2;
defreduc dec(enc(x,y),y) = x;



parameter attacker_depth = 2;

defproc A(k) = new n in c!(enc(n,k)).c?(x).[dec(x,k)=h(n)].end!(h(n));
defproc B(k) = c?(x).(begin!(dec(x,k)) | c!(enc(h(dec(x,k)),k)));
defproc Sys = new k in (A(k) | B(k));
defproc Attacker = c?(v).c!(*).s!(v);
defproc World = (Sys | Attacker);

defprop begin = <begin!> true;
defprop end = <end!> true;
defprop corrsp = always (end => begin);


check World |= corrsp;