// helios protocol with identities and mixnet - no privacy because of ballot replay attack

fun aenc/3.
fun pk/1.


reduc adec(aenc(x,r,pk(y)),y) -> x.

free c.
free a.
free b.
free e.
free yes.
free no.

(* voter process casting v, using private channel bb and election pk pkE
let V(id, v, pkE, bb) = 
(* complete *)
0.


(* Bulletin Board *)
let BB(bb, mn) =
    ( in(bb, b1); (* check ballot and send encrypted vote to mix-net *) |
    ( in(bb, b2); (* check ballot and send encrypted vote to mix-net *) |
    ( in(c,  b3); (* check ballot and send encrypted vote to mix-net *) ).



(* Tally through mix *)
let T(skT,mn) =
    in(mn,x1);
    in(mn,x2);
    in(mn,x3);
    ( out(c, adec(x1,skT)) | out(c, adec(x2,skT)) | out(c, adec(x3,skT)) ).


let AyBn = new skE; let pkE = pk(skE) in
       new bb; new mn; out(c, pkE);
       (* 2 honest voters: A votes yes, B votes no *)	
     (V(a,yes,pkE,bb) | V(b,no,pkE,bb) | BB(bb,mn) | T(skT,mn) ).

let AnBy = (* complete here *}


query trace_equiv(AyBn,AnBy).

// privacy cannot be proven because of vote replay attack