fun true/0.

fun pk/1.
fun sign/2.
fun checksign/3.

equation checksign(sign(x,y),x,pk(y)) = true.

query ev:fail(true).
query ev:pass(true).

query ev:fail2(true).

free c.

(* ProVerif modelling *)
   
let P =	
	(* adding new i avoids ProVerif being unable to 
	   complete the proof because of over-approximations *)
	new i;

	(*in(b,v);*) (* input vote *)

	(* START PROTOCOL *)
	(*in(a,x);*) (* input secret key *)
	out(c,(v,sign(v,x)));
	(* END PROTOCOL *)

	in(c,z);
	let (z1,z2,z3)=z in
	in(b',y); 

	((
		if z = (sign(v,x),v,pk(x)) (*Riv *) 
			then event pass(true); out(cpass,(true,z,i))
	 )|(
		if z = (sign(v,x),v,pk(x)) then (* Riv *)
			if (checksign(z1,z2,z3), v) <> (true, z2) (* not Ruv *)
				then event fail(true)
	 )|(
		if z = (sign(v,x),v,pk(x)) then (* Riv *)
			if (checksign(z1,z2,z3), y) <> (true, z3) (* not Rev *)
				then event fail(true)
	 )|(
		if z <> (sign(v,x),v,pk(x)) then (* not Riv *)
			if (checksign(z1,z2,z3), y) = (true, z3) (* Rev *)
				then event fail2(true)
	)).

(* let Q = new skv; (out(a,skv) | out(b',pk(skv)) | out(cred,pk(skv)) | out(c,pk(skv))). *)

(* adding new i avoids ProVerif being unable to complete the proof because of over-approximations *)
let Q = new i; (*new skv; (out(a,skv) |*) (out(b',pk(skv)) | out(cred,(pk(skv),i)) | out(c,pk(skv))).

let R = !new s;((!out(b,s))|out(c,s)).

let R' = in(b,v1);in(b,v2);in(c,x1);in(c,x2);in(c,y1);in(c,y2);in(c,(z1,z2,z3));
	((
		if (z1,z2,z3) = (sign(v1,x1),v1,pk(x1)) (* Riv1 *)
			then if (z1,z2,z3) = (sign(v2,x2),v2,pk(x2)) (* Riv2 *)
				then if v1 <> v2 then event fail(true)
	  )|(
		if (checksign(z1,z2,z3), v1) = (true, z2) (* Ruv1 *)
			then if  (checksign(z1,z2,z3), v2) = (true, z2) (* Ruv2 *)
				then if v1 <> v2 then event fail(true)
      )|(
		if (checksign(z1,z2,z3), y1) = (true, z3) (* Rev 1 *)
			then if (checksign(z1,z2,z3), y2) = (true, z3) (* Rev 2 *)
				then if y1 <> y2 then event fail(true)
     )).		 


let R'' = in(cpass,(e1,e2,i)); in(cpass,(e'1,e'2,i'));
    	  if e1 = true then if e'1 = true then if e2 = e'2 then
		  if i <> i' then (* should always be true; eliminates overapproximation *)
		  event fail(true).

let R''' = in(cred,(e,i)); in(cred,(e',i'));
    	   if i <> i' then (* should always be true; eliminates overapproximation *) 
    	   if e = e' then event fail(true).


process new cred; new cpass; ((new b;((!(*new a;*)in(b,v);new b';new skv; ( (let x = skv in P)|Q))|R|R'))|R''|R''')


