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


deffun sign/2;
defreduc sigcheck(sign(x,y),pk(y)) = x;

deffun pair/2;
defreduc px(pair(x,y)) = x;
defreduc py(pair(x,y)) = y;


defproc Alice(pubServer,secretA) = 
			   c?(host).
			   servchan!(a,host). 
			   servchan?(x).
			   let pubh = px(sigcheck(x,pubServer)) in
		           new nonceA in 
			   c!(enc(pair(nonceA,a),pubh)).
			   c?(y).
			   let nA = px(dec(y,secretA)) in
			   let nX = py(dec(y,secretA)) in
			   [nonceA = nA].
			   c!(enc(nX,pubh)).
			   okAlice!();
			   



defproc Bob(pubServer,secretB) = c?(x).
			 let nY = px(dec(x,secretB)) in
			 let host = py(dec(x,secretB)) in
			 servchan!(b,host).
			 servchan?(y).
			 let pubh = px(sigcheck(y,pubServer)) in
			 new nonceB in
			 c!(enc(pair(nY,nonceB),pubh)).
			 c?(z).
			 let nB = dec(z,secretB) in
			 [nonceB = nB].
			 okBob!();




defproc Server(pubK_A,pubK_B,pubK_T,secretK) = servchan?(x,y).
					select{[y=b].servchan!(sign(pair(pubK_B,y),secretK)).Server(pubK_A,pubK_B,pubK_T,secretK);
					       [y=a].servchan!(sign(pair(pubK_A,y),secretK)).Server(pubK_A,pubK_B,pubK_T,secretK);
					       [y=t].servchan!(sign(pair(pubK_T,y),secretK)).Server(pubK_A,pubK_B,pubK_T,secretK)};
					  
defproc Attacker(secretT) = c?(pkK,pkA,pkB).
		   	    c!(t).
			    c?(m).
			    c!(*/1).
			    c?(nounces).
			    c!(*/1).
			    c?(n).
			    c!(*/1).
			    okTrudy!(secretT,pkB,m,nounces,n);


defproc Sys = new secretA,secretB,secretT,secretK in 
	      (c!(pk(secretK),pk(secretA),pk(secretB)).
	      (Bob(pk(secretK),secretB) | Alice(pk(secretK),secretA) | Server(pk(secretA),pk(secretB),pk(secretT),secretK)) | Attacker(secretT));



check Sys |= eventually (<okBob!> true | <okAlice!> true | <okTrudy!> true);