fun true/0.

fun eq/2.
fun land/2.

equation eq(x,x) = true.
equation land(true,true) = true.

fun pk/1.
fun commit/2.
fun open/2.
fun penc/3.
(* fun renc/2. *)
fun dec/2.
fun f/2.

equation dec(penc(x,y,pk(z)),z) = x.
(* equation renc(penc(x,y,pk(z)),y') = penc(x,f(y,y'),pk(z)). *)
equation dec(penc(x,y,pk(z)),commit(penc(x,y,pk(z)),z)) = x.
equation open(commit(x,y),y) = x.

fun dk/3.
fun pet/3.

equation pet(penc(x,y,pk(z)),penc(x,y',pk(z)),dk(penc(x,y,pk(z)),penc(x,y',pk(z)),z)) = true.

(*
       Signature proof of knowledge zk1 has been taken from http://infsec.cs.uni-sb.de/~maffei/ev.zip

       The proof shows that

               beta1 = penc(alpha1,alpha2,beta3) /\ beta2 = penc(alpha3,alpha4,beta3) /\
                       (alpha1 = beta4 \/ alpha1 = beta5 \/ alpha1 = beta6)

       we will use

               alpha1 = v, alpha2 = r1, alpha3 = k, alpha4 = r2

               beta3 = pk(skT), beta4 = n1, beta5 = n2, beta6 = n3,


       Signature proof of knowledge zk2 is new, it shows

               beta1 = commit(penc(m,r,pk(alpha1)),alpha1) /\ beta2 = penc(m,r,pk(alpha1))

       if follows that beta1 is a decryption key
*)

fun public/1.
fun formula/1.
fun zk1/2.
fun zk2/2.
fun zkver1/1.
fun zkver2/1.

equation public(zk1(x,y)) = y.
equation public(zk2(x,y)) = y.
equation formula(zk1(x,y)) = true.
equation formula(zk2(x,y)) = true.

equation zkver1(zk1((v,r1,k,r2),(penc(v,r1,pky),penc(k,r2,pky),pky,v,z1,z2))) = true.
equation zkver1(zk1((v,r1,k,r2),(penc(v,r1,pky),penc(k,r2,pky),pky,z1,v,z2))) = true.
equation zkver1(zk1((v,r1,k,r2),(penc(v,r1,pky),penc(k,r2,pky),pky,z1,z2,v))) = true.
equation zkver2(zk2((sk),(commit(penc(v,r,pk(sk)),sk),penc(v,r,pk(sk))))) = true.

fun fakezk'/3.

equation public(fakezk'(x,y,z)) = y.
equation formula(fakezk'(x,y,z)) = z.

fun fakezk1/2.
fun fakezk2/2.

equation formula(fakezk1(x,y)) = y.
equation formula(fakezk2(x,y)) = y.

fun fakever/3.
fun fakepublic/2.


free c.

free n1,n2,n3.

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

let V =
       (* START JCJ *)
       new r1;
       new r2;
       in(a,k);
       out(c,zk1((v,r1,k,r2),(penc(v,r1,pk(skT)),penc(k,r2,pk(skT)),pk(skT),n1,n2,n3)));
       (* END JCJ *)


       in(b',y);
       in(c,z);
       let (z1,z2,z3) = z in
       let (z1_1,z1_2,z1_3,z1_4,z1_5,z1_6) = public(z1) in
       let (z2_1,z2_2) = public(z2) in

       ((
               if (zkver2(z2),z1_1,z1,pet(y,z1_2,z3)) = (true,z2_2,zk1((v,r1,k,r2),(penc(v,r1,pk(skT)),penc(k,r2,pk(skT)),pk(skT),n1,n2,n3)),true) (* IV *)
                  then event pass(true); out(cpass,(true,z,i))
        )|(
               if (zkver2(z2),z1_1,z1,pet(y,z1_2,z3)) = (true,z2_2,zk1((v,r1,k,r2),(penc(v,r1,pk(skT)),penc(k,r2,pk(skT)),pk(skT),n1,n2,n3)),true) (* IV *)
                  then if (zkver2(z2),z1_1,dec(z2_2,z2_1)) <> (true,z2_2,v)  (* not UV *)
                     then event fail(true)
        )|(
               if (zkver2(z2),z1_1,z1,pet(y,z1_2,z3)) = (true,z2_2,zk1((v,r1,k,r2),(penc(v,r1,pk(skT)),penc(k,r2,pk(skT)),pk(skT),n1,n2,n3)),true) (* IV *)
                  then if (zkver2(z2),z1_1,zkver1(z1),pet(y,z1_2,z3)) <> (true,z2_2,true,true) (* not EV *)
                     then  event fail(true)
        )|(
               if (zkver2(z2),z1_1,z1,pet(y,z1_2,z3)) <> (true,z2_2,zk1((v,r1,k,r2),(penc(v,r1,pk(skT)),penc(k,r2,pk(skT)),pk(skT),n1,n2,n3)),true) (* not IV *)
                  then if (zkver2(z2),z1_1,zkver1(z1),pet(y,z1_2,z3)) = (true,z2_2,true,true) (* EV *)
                     then event fail(true)
       )).

let K =
       new k; (* generate fresh credentails *)
       new r''; let y = penc(k,r'',pk(skT)) in (* provide encrypted credentials *)
       (out(a,k) | out(c,y) | out(b',y) | out(cred,(y,i))).


let G = (!out(b,n1)) | (!out(b,n2)) | (!out(b,n3)).

let A = in(c,z);                               (* read ballot from BB *)
       if zkver1(z) = true then                (* if valid ballot *)
       let (z1,z2,z3,z4,z5,z6) = public(z) in

       (* new r1; new r2; *)
       (* out(c,(renc(z1,r1),renc(z2,r2))); *) (* re-encryption of the Mix-Net (assumed to be verifiable) *)

       in(c,z');                               (* read encrypted credentials from BB *)

       if pet(z',z2,dk(z',z2,skT)) = true then (* if pet succeeds then *)
       out(c,dk(z',z2,skT));                   (* output pet proof *)

       out(c,zk2((skT),(commit(z1,skT),z1))). (* output decryption proof *)


let P =
       in(b,v1);in(b,v2);in(c,x1);in(c,x2);in(c,y1);in(c,y2);in(c,z);

       let (z1,z2,z3) = z in
       let (z1_1,z1_2,z1_3,z1_4,z1_5,z1_6) = public(z1) in
       let (z2_1,z2_2) = public(z2) in

       ((
               let (r1,k,r2,pkT) = x1 in
               let (r1_,k_,r2_,pkT_) = x2 in

               if (zkver2(z2),z1_1,z1,pet(y1,z1_2,z3)) = (true,z2_2,zk1((v1,r1,k,r2),(penc(v1,r1,pkT),penc(k,r2,pkT),pkT,n1,n2,n3)),true) (* IV1 *)
                  then if (zkver2(z2),z1_1,z1,pet(y2,z1_2,z3)) = (true,z2_2,zk1((v2,r1_,k_,r2_),(penc(v2,r1_,pkT_),penc(k_,r2_,pkT_),pkT_,n1,n2,n3)),true) (* IV2 *)
                       then if v1 <> v2 then event fail(true)
       )|(
               if (zkver2(z2),z1_1,dec(z2_2,z2_1)) = (true,z2_2,v1) (* UV1 *)
                  then if (zkver2(z2),z1_1,dec(z2_2,z2_1)) = (true,z2_2,v2) (* UV2 *)
                       then if v1 <> v2 then event fail(true)

       )|(
               if (zkver2(z2),z1_1,zkver1(z1),pet(y1,z1_2,z3)) = (true,z2_2,true,true) (* EV1 *)
                  then if (zkver2(z2),z1_1,zkver1(z1),pet(y2,z1_2,z3)) = (true,z2_2,true,true) (* EV2 *)
                       then if y1 <> y2 then event fail(true)
       )).


let Q = 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 cpass;new cred;((new b;((new skT;out(c,pk(skT)); (!new i;in(b,v);new b';new a;(V|K)) |(!A))|G|P))|Q|R)
