deffun pair/2;
deffun enc/2;

defreduc dec(enc(x,y),y) = x ;
defreduc fst(pair(x,y)) = x;
defreduc snd(pair(x,y)) = y;

defproc P(k) = new n in c!(n).c?(x).
			   let y = dec(x,k) in
			   [n = y].
			   c!(enc(pair(v,n),k));
				
defproc Q(k) = c?(x).
			   c!(enc(x,k)).
			   c?(y).
			   let m = dec(y,k) in
			   let v = fst(m) in
			   let n = snd(m) in
			   [n = x].
			   ok!();

defproc Sys = new k in (P(k) | Q(k));

defproc Attacker = c?(x).c!(*/1).c?(y).c!(*/1).c?(z).c!(*/1).mem!(x,y,z);

defproc World = Sys | Attacker;


defprop attackerK = not eventually inside (2 | (1 and @mem and knows v)); 

defprop pqK = eventually inside ((2 and knows v) | (1 and @mem and not (knows v))); 


check World |= attackerK;

check World |= pqK;