(* Receipt-freeness for BeleniosVS *)

(* Trust assumptions:
 - dishonest registrar (thus leaked voting sheet, regardless of whether the voter loses it or not)
 - honest audit device, voting device, voting server
 - private channel (authentic + secret) between voting device and server
   (stronger than no leaked password)
*)


(* -- Types -- *)
(* Asymmetric keys encryption types *)
type skey.
type pkey.

(* Signature keys *)
type sskey.
type spkey.

(* Other types *)
type rand.
type name.
type vote.

(* -- Equational theory -- *)
(* Randomized asymmetric encryption *)
fun pk(skey):pkey.
fun aenc(bitstring,pkey,spkey,rand,rand):bitstring.

reduc forall message:bitstring, sk:skey, xspk:spkey, r:rand, t:rand;
  adec(aenc(message,pk(sk),xspk,r,t), sk) = message.


(* Randomized signature *)
fun spk(sskey):spkey.
fun sign(bitstring, pkey, sskey, rand, rand):bitstring.

reduc forall message:bitstring, xpk:pkey, xssk:sskey, r:rand, t:rand, s:rand, u:rand;
  verify(aenc(message,xpk,spk(xssk),r,t), sign(aenc(message,xpk,spk(xssk),r,t),xpk,xssk,s,u),spk(xssk)) = true.


(* Randomization *)
reduc forall message:bitstring, xpk:pkey, xssk:sskey, r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
  randomize_aenc(
    aenc(message,xpk,spk(xssk),r,v),
    sign(aenc(message,xpk,spk(xssk),r,v),xpk,xssk,s,w),
    xpk, spk(xssk),t,u) =
  aenc(message,xpk,spk(xssk),r,t).

reduc forall message:bitstring, xpk:pkey, xssk:sskey, r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
  randomize_sign(
    aenc(message,xpk,spk(xssk),r,v),
    sign(aenc(message,xpk,spk(xssk),r,v),xpk,xssk,s,w),
    xpk,spk(xssk),t,u) =
  sign(aenc(message,xpk,spk(xssk),r,t),xpk,xssk,s,u).

letfun randomize(ballot:bitstring,signature:bitstring,pke:pkey,xspk:spkey,r:rand,s:rand) =
  (randomize_aenc(ballot,signature,pke,xspk,r,s),
   randomize_sign(ballot,signature,pke,xspk,r,s)).


(* Left randomization - private operation used to model correct randomization by a honest device *)
reduc forall message:bitstring, xpk:pkey, xssk:sskey, r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
  randomize_aenc_left(
    aenc(message,xpk,spk(xssk),r,v),
    sign(aenc(message,xpk,spk(xssk),r,v),xpk,xssk,s,w),
    xpk, spk(xssk),t,u) =
  aenc(message,xpk,spk(xssk),t,v) [private].

reduc forall message:bitstring, xpk:pkey, xssk:sskey, r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
  randomize_sign_left(
    aenc(message,xpk,spk(xssk),r,v),
    sign(aenc(message,xpk,spk(xssk),r,v),xpk,xssk,s,w),
    xpk,spk(xssk),t,u) =
  sign(aenc(message,xpk,spk(xssk),t,v),xpk,xssk,u,w) [private].

letfun randomize_left(ballot:bitstring,signature:bitstring,pke:pkey,xspk:spkey,r:rand,s:rand) =
  (randomize_aenc_left(ballot,signature,pke,xspk,r,s),
   randomize_sign_left(ballot,signature,pke,xspk,r,s)).



(* -- Election setup -- *) 
(* Election key *)
free sk_e:skey [private].
letfun pk_e = pk(sk_e).


(* Voter registration *)
fun voter_registration(name):bitstring [private].
reduc forall n:name;
  is_registered(n,voter_registration(n)) = true.

(* Valid verification keys (declared by the registrar) *)
fun valid(name,spkey):bitstring [private].
reduc forall n:name, xspk:spkey;
  is_valid(n,xspk,valid(n,xspk)) = true.

 
(* -- Registrar functions -- *)
(* Type conversion *)
fun bitstring_of_vote(vote):bitstring [data, typeConverter].

(* Voting sheet generation *)
(*letfun voting_sheet(v:vote,ssk:sskey) =
  new r:rand;
  new s:rand;
  (aenc(bitstring_of_vote(v),pk_e,spk(ssk),r,r),
   sign(aenc(bitstring_of_vote(v),pk_e,spk(ssk),r,r),pk_e,ssk,s,s),
   r,s).
*)

(* -- Names -- *)
(* Channels *)
free public:channel.
free rfch:channel.

(* Possible votes *)
free A:vote.
free B:vote.

(* Honest voters *)
free Alice:name.
free Bob:name.

free ssk_Alice:sskey.
free ssk_Bob:sskey.
(*with the same key letfun ssk_Bob = ssk_Alice. (also works)*)

letfun spk_Alice = spk(ssk_Alice).
letfun spk_Bob = spk(ssk_Bob).

letfun vreg_Alice = voter_registration(Alice).
letfun vreg_Bob = voter_registration(Bob).

(* Server acknowledgement *)
free ack:bitstring.

(* Private channels between the voters and the voting server *)
free chan_Alice:channel [private].
free chan_Bob:channel [private].


(* -- Tables -- *)
(* Public Bulletin Board *)
table BULLETIN_BOARD(spkey,bitstring,bitstring).



(* -- Processes -- *)

(* Registrar is dishonest: no process *)

(* Honest voter, with honest voting device, performing audit with honest auditing device *)
(* receives the voting sheet on a public channel (dishonest registrar) *)
(* votes for choice[A,B] *)
(* receipt-freeness encoding: output all nonces and all received messages *)
let Honest_Voter_audit_AB(n:name,reg_n:bitstring,server_channel:channel) =
  (* nonces for randomization -- generated in the beginning, as Proverif prefers *)
  new rv:rand; out(rfch,rv);
  new sv:rand; out(rfch,sv);

  (* receiving the voting sheet from the dishonest registrar *)
  in (public,message:bitstring); out(rfch,message);

  let (=spk_Alice, val_spk:bitstring,
    =A,(vote_a:bitstring,sign_a:bitstring,ra:rand,sa:rand),
    =B,(vote_b:bitstring,sign_b:bitstring,rb:rand,sb:rand)) = message in
 
  (* auditing the voting sheet (honest auditing device) *)
  if (aenc(bitstring_of_vote(A),pk_e,spk_Alice,ra,ra) = vote_a
    && aenc(bitstring_of_vote(B),pk_e,spk_Alice,rb,rb) = vote_b
    && verify(vote_a,sign_a,spk_Alice) = true
    && verify(vote_b,sign_b,spk_Alice) = true)
  then (
    let vote_v = choice[vote_a,vote_b] in
    let sign_v = choice[sign_a,sign_b] in
  
    (* the honest voting device randomizes the ballot *)
    (* here we do not use randomize_left, as the attacker does know rv,sv
       and can thus recover the original ballot)*)
    let (b_v1:bitstring,s_v1:bitstring) = randomize(vote_v,sign_v,pk_e,spk_Alice,rv,sv) in

    (* the voting device sends the ballot on an authenticated channel *)
    (* for receipt-freeness we need to assume this channel is actually private *)
    out(server_channel,(n,reg_n,spk_Alice,val_spk,(b_v1,s_v1)));
    
    (* getting confirmation from the server through the voting device *)
    in(server_channel,=ack);

    (* verifying that the vote appears on the board *)
    get BULLETIN_BOARD(=spk_Alice,rand_ballot,sign_rand_ballot) in
    out(rfch,(spk_Alice,rand_ballot,sign_rand_ballot));
    out(public,n)).


(* Honest voter, with honest voting device, performing audit with honest auditing device *)
(* receives the voting sheet on a public channel (dishonest registrar) *)
(* votes for choice[B,A] *)
let Honest_Voter_audit_BA(n:name,reg_n:bitstring,server_channel:channel) =

  (* nonces for randomization -- generated in the beginning, as Proverif prefers *)
  new rv:rand;
  new sv:rand;

  (* receiving the voting sheet from the dishonest registrar *)
  in (public, message:bitstring);
 
  (* receiving the voting sheet from the dishonest registrar *)
  let (=spk_Bob, val_spk:bitstring,
    =A,(vote_a:bitstring,sign_a:bitstring,ra:rand,sa:rand),
    =B,(vote_b:bitstring,sign_b:bitstring,rb:rand,sb:rand)) = message in
 
  (* auditing the voting sheet (honest auditing device) *)
  if (aenc(bitstring_of_vote(A),pk_e,spk_Bob,ra,ra) = vote_a
    && aenc(bitstring_of_vote(B),pk_e,spk_Bob,rb,rb) = vote_b
    && verify(vote_a,sign_a,spk_Bob) = true
    && verify(vote_b,sign_b,spk_Bob) = true)
  then (
    let vote_v = choice[vote_b,vote_a] in
    let sign_v = choice[sign_b,sign_a] in
    (* the honest voting device randomizes the ballot *)
    (* to follow the same assumptions as for Alice, we only use randomize here *)
    (* and we consider a private channel to the voting server *)
    let (b_v1:bitstring,s_v1:bitstring) = randomize(vote_v,sign_v,pk_e,spk_Bob,rv,sv) in
 
    out(server_channel,(n,reg_n,spk_Bob,val_spk,(b_v1,s_v1)));

    (* getting confirmation from the server through the voting device *)
    in(server_channel,=ack);

    (* verifying that the vote appears on the board *)
    get BULLETIN_BOARD(=spk_Bob,rand_ballot,sign_rand_ballot) in
    out(public,n)).
 

(* Honest voting server *)
let Honest_Voting_Server(server_channel:channel) =

  (* nonces for randomization -- generated in the beginning, as Proverif prefers *)
  new rv:rand;
  new sv:rand;
  new tv:rand;
  new uv:rand;
  
  (* receiving the ballot *)
  in(server_channel,message:bitstring);

  let(n:name,reg_n:bitstring,spk_n:spkey,val_spk_n:bitstring,(ballot:bitstring,signature:bitstring)) =
    message in

  (* verifications on the ballot *)
  if (
   (* the voter is eligible *)
   is_registered(n,reg_n)=true
   (* the key (allegedly) signing the ballot is eligible (ie declared valid by the registrar) *)
   && is_valid(n,spk_n,val_spk_n)=true
   (* authentication (modelled only for the honest voters): accept votes from
      Alice (resp. Bob) only on chan_Alice (resp. chan_Bob) *) 
   && (n <> Alice || server_channel = chan_Alice)
   && (n <> Bob || server_channel = chan_Bob)
   (* accepting a ballot signed by Alice's key only if Alice is authenticated *)
   (* (part of the modelling of privacy: we ensure that Alice and Bob's ballots are received,
       and the server would then reject other ballots signed with the same key) *)
   && (n = Alice || spk_n<>spk_Alice)
   && (n = Bob || spk_n<>spk_Bob)
   (* verifying the signature *)
   && verify(ballot,signature,spk_n) = true)
  then (

    (* randomizing and publishing the ballot *)
    (* here we may use randomize_left, as the randomization by the honest voting server
       is correct, with secret nonces *)
    (* (we actually need to, otherwise the attacker could reconstruct the initial ballots) *)
    let (rand_ballot1:bitstring,rand_sign1:bitstring) = randomize(ballot,signature,pk_e,spk_n,rv,sv) in
    let (rand_ballot:bitstring,rand_sign:bitstring) = randomize_left(rand_ballot1,rand_sign1,pk_e,spk_n,tv,uv) in
    insert BULLETIN_BOARD(spk_n,rand_ballot,rand_sign);
    (* also output the ballot on a public channel (as the attacker cannot read directly from the table) *)
    out(public,(n,spk_n,rand_ballot,rand_sign));

    (* sending confirmation to the voter (through the voting device) *)
    out(server_channel,ack)
    )
  else 0.


(* Tally *)
let Tally() =
  (* first retrieve the ballots signed by the honest voters *)
  (* (we know these are the keys they actually used, by construction) *)
  get BULLETIN_BOARD(=spk_Alice,rand_ballot_Alice,sign_rand_ballot_Alice) in
  get BULLETIN_BOARD(=spk_Bob,rand_ballot_Bob,sign_rand_ballot_Bob) in

  (* check that the signature key written on the board indeed signs the ballots*)
  if (verify(rand_ballot_Alice,sign_rand_ballot_Alice,spk_Alice)=true
  && verify(rand_ballot_Bob,sign_rand_ballot_Bob,spk_Bob)=true) then (

    (* mixnet *)
    new mixnet:channel;
    ( out(mixnet,choice[rand_ballot_Alice,rand_ballot_Bob])
    | out(mixnet,choice[rand_ballot_Bob,rand_ballot_Alice])
    |(
      in(mixnet,b1:bitstring);
      in(mixnet,b2:bitstring);
      (* decrypt and output the mixed ballots *)
      out(public,(adec(b1,sk_e),adec(b2,sk_e)));

      (* decrypt and output the ballots signed with any other key *)
      !(
        in(public,spk_n:spkey);
        if (spk_n <> spk_Alice && spk_n <> spk_Bob) then
          (get BULLETIN_BOARD(=spk_n,b_n,sign_n) in
          if (verify(b_n,sign_n,spk_n) = true) then
            out(public, adec(b_n,sk_e)))
       )
     )
    )
  ).



(* Main process *)
process
  (* setup: output the election public key, register Alice and Bob *)
  (out(public,pk_e);
   out(public,(voter_registration(Alice)));
   out(public,(voter_registration(Bob))))
 |
  (* register any number of dishonest agents *)
  !(in(public,n:name); out(public,(n,voter_registration(n))))
 |
  (* as the registrar is dishonest, any key may be marked as valid *)
  !(in(public,(n:name,spk_n:spkey)); out(public,valid(n,spk_n)))
 |
  (* Alice, Bob vote *)
   Honest_Voter_audit_AB(Alice,voter_registration(Alice),chan_Alice)
 |
   Honest_Voter_audit_BA(Bob,voter_registration(Bob),chan_Bob)
 |
  (* Voting server for Alice, Bob *)
   Honest_Voting_Server(chan_Alice)
 |
   Honest_Voting_Server(chan_Bob)
  (* Voting server for dishonest voters *)
 |
   ! Honest_Voting_Server(public)   
 |
   (* Tally *)
   Tally()