Formal analysis of the Belenios VS protocol – Verifiability – 05_HONEST_VOTING_DEVICE

(* HONEST VOTING DEVICE------------------------------------------------------ *)
let Honest_Voting_Device(voting_device_channel:key,server_channel:key) =
 new rv:rand;
 new sv:rand;
 in (public,message:bitstring);
 let (
 n:name,pwd_n:bitstring,
 spk_n:spkey,val_n:bitstring,
 vote_v:bitstring,sign_v:bitstring
 )
 = dec(message,voting_device_channel) in
 if (verify(vote_v,sign_v,spk_n) = true)
 then (
 out (public, enc((

(n,pwd_n,spk_n,val_n),
 randomize(vote_v,sign_v,pk_e,spk_n,rv,sv)),

server_channel));
 
 (* The voting device randomize the ballot and sends it to the server- *)
 out (public,randomize(vote_v,sign_v,pk_e,spk_n,rv,sv))
 )
 .