(* ROGUE VOTING SERVER NO ROGUE REGISTRAR------------------------------------ *)
let Rogue_Voting_Server(server_channel:key,public_channel:key) =
new ack:rand;
out (public,server_channel);
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
(* Since the Bulletin Board can be audited by anyone, we made the assump
tion that at least all displayed ballots are correctly signed. Also, sin
ce the registrar is honest in this case scenario, the voting server also
make sure taht the credential used with the ballot is a valid one. Other
wise ProVerif can not run the proof---------------------------------- *)
if (
verify(ballot,signature,spk_n) = true
&& is_valid(val_n,spk_n)=true
)
then (
event GOING_TO_TALLY(n,spk_n,ballot,adec(ballot,sk_e));
(* The rogue voting server does not proceed to any verification
other than the signature and its certificate and publish all bal
lots it gets------------------------------------------------------ *)
insert BULLETIN_BOARD(n,spk_n,ballot,signature);
out (public,enc((n,pwd_n,spk_n,ack),public_channel));
out (public,(spk_n,ballot,signature))
)
else
(
0
)
.
