(* HONEST VOTING SERVER------------------------------------------------------ *)
let Honest_Voting_Server(server_channel:key,public_channel:key) =
new rv:rand;
new sv:rand;
new ack:rand;
in (public,message:bitstring);
let (
(n:name,pwd_n:bitstring,spk_n:spkey,val_n:bitstring),
(ballot:bitstring,signature:bitstring)
)
= dec(message,server_channel) in
(* The voting server makes some verification------------------------- *)
if (
(* Is the voter an elegible one ?---------------------------- *)
is_registered(n)=true
(* Did they correctly authenticate themself ?---------------- *)
&& pwd_n=password(n)
(* Is the credential used one generated by the registrar ?--- *)
&& is_valid(val_n,spk_n)=true
(* Is the ballot correctly signed ?-------------------------- *)
&& verify(ballot,signature,spk_n) = true
)
then (
(* The voting server then randomizes the ballot and displays it
on the Public Bulletin Board--------------------------------- *)
let (rand_ballot:bitstring,rand_sign:bitstring)
= randomize(ballot,signature,pk_e,spk_n,rv,sv) in
event GOING_TO_TALLY(n,spk_n,rand_ballot,adec(rand_ballot,sk_e));
insert BULLETIN_BOARD(n,spk_n,rand_ballot,rand_sign);
(* End of the session for the voter-------------------------- *)
out (public,enc((n,pwd_n,spk_n,ack),public_channel));
(* The ballot is made public because tables cannot be read by th
e attacker in ProVerif--------------------------------------- *)
out (public,(spk_n,val_n,rand_ballot,rand_sign))
)
else 0
.
