fun true/0.

fun pk/1.
fun commit/2.
fun open/2.
fun sign/2.
fun checksign/3.
fun blind/2.
fun unblind/2.

equation checksign(sign(x,y),x,pk(y)) = true.
equation unblind(sign(blind(x,y),z),y) = sign(x,z).
equation unblind(blind(x,y),y) = x.
equation open(commit(x,y),y) = x.


free c.
free skr.

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

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

	in(b,v);

	(* START FOO *)
	new r; let x_r = r in
	new r'; let x_r' = r' in
	in(c,x); (* input secret key *)	
	let m' = commit(v,r) in
	let m'' = blind(m',r') in 
	out(c,(pk(x),m'',sign(m'',x)));
	in(c,bsb);
	if checksign(bsb,m'',pk(skr)) = true then 
	let m = unblind(bsb,r') in
	out(c,(m',m));	
	in(c,(bbe1,bbe2,bbe3));
	if (m',m)=(bbe2,bbe3) then
	out(c,(bbe1,r));	
	(* END FOO *)

	in(c,z);
	let (z1,z2,z3,z4,z5) = z in	
	in(b',y); 
	((
		if (z1,z2,z3,z4,z5, checksign(z3,z2,pk(skr))) 
				= (bbe1,commit(v,x_r),unblind(bsb,x_r'),x_r,v,true)  (*Riv *) 
		then event pass(true); out(cpass,(true,z,i))
	 )|(
		if (z1,z2,z3,z4,z5, checksign(z3,z2,pk(skr))) 
				= (bbe1,commit(v,x_r),unblind(bsb,x_r'),x_r,v,true) then (* Riv *)
		if (z2,checksign(z3,z2,pk(skr)),z5)  <> (commit(z5,z4),true,v) (* not Ruv *)
		then event fail(true)
	)).

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

let Q = in(c,x); ( out(a,x) | out(b',pk(x)) | out(cred,pk(x)) | out(c,pk(x))).

let R' = in(b,v1);in(b,v2);in(c,(bbe1_1,(*bbe2_1,bbe3_1,*)bsb_1,x_r_1,x_r'_1));in(c,(bbe1_2,(*bbe2_2,bbe3_2,*)bsb_2,x_r_2,x_r'_2));in(c,z);
    let (z1,z2,z3,z4,z5) = z in
	((
		if (z1,z2,z3,z4,z5,checksign(z3,z2,pk(skr))) 
				= (bbe1_1,commit(v1,x_r_1),unblind(bsb_1,x_r'_1),x_r_1,v1,true) (* Riv1 *)
		then if (z1,z2,z3,z4,z5,checksign(z3,z2,pk(skr))) 
				= (bbe1_2,commit(v2,x_r_2),unblind(bsb_2,x_r'_2),x_r_2,v2,true) (* Riv2 *)
		then if v1 <> v2 then event fail(true)
	 )|(
		if (z2,checksign(z3,z2,pk(skr)),z5) = (commit(z5,z4),true,v1) (* Ruv1 *)
		then if (z2,checksign(z3,z2,pk(skr)),z5) = (commit(z5,z4),true,v2) (* Ruv2 *)
		then if v1 <> v2 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).

process new cred; new cpass; ((new b;((!new a;new b'; (P|Q))|R|R'))|R'')

